diff --git a/Vagrantfile b/Vagrantfile index ca5ea92..f0b8f45 100644 --- a/Vagrantfile +++ b/Vagrantfile @@ -3,6 +3,47 @@ # See README.md, in the same directory as this Vagrantfile. +# This block is loaded into the shell before any other commands. +# +# This defines the logfile to which we write +VAGRANT_LOGFILE = "/home/vagrant/vagrant-provisioning-log.txt" + +# Here's the logging function; the constant above is embedded directly. +LOG_REPORT_FUNCTION = <<-SHELL + touch #{VAGRANT_LOGFILE} + chown vagrant:vagrant #{VAGRANT_LOGFILE} + + log_report() { + if [ $1 != "echo" ]; then + echo $@ >> #{VAGRANT_LOGFILE} + fi + + $@ >> #{VAGRANT_LOGFILE} 2>&1 + + RET=$? + + if [ $RET -ne 0 ]; then + echo "[Error] $@" + else + case $1 in + echo|cd) ;; + *) echo "[Success] $@" ;; + esac + fi + + return $RET + } + + export DEBIAN_FRONTEND=noninteractive +SHELL + +# Write an entry for the log that indicates the date. +PROVISIONING_DATE = <<-SHELL + echo "# ------------------------------------------------------ #" + echo "# Starting provisioning at `date`" + echo "# ------------------------------------------------------ #" +SHELL + # Basic software install via apt (and pip) PROVISIONING_APT = <<-SHELL # --------- @@ -10,8 +51,8 @@ PROVISIONING_APT = <<-SHELL echo " " echo "# ------------------------------------------------------ #" echo "# Apt Update & Upgrade " - DEBIAN_FRONTEND=noninteractive apt-get update - DEBIAN_FRONTEND=noninteractive apt-get -y upgrade + apt-get update + apt-get -y upgrade echo " " echo "# End Apt Update & Upgrade" echo "# ------------------------------------------------------ #" @@ -23,7 +64,7 @@ PROVISIONING_APT = <<-SHELL echo "# python3 python3-dev " echo "# python3-distutils python3-venv " echo "# python3-pip" - DEBIAN_FRONTEND=noninteractive apt-get install -y make cmake pkg-config uuid-dev libyaml-dev fontconfig libx11-xcb1 libx11-6 python3 python3-dev python3-distutils python3-venv python3-pip + apt-get install -y make cmake pkg-config uuid-dev libyaml-dev fontconfig libx11-xcb1 libx11-6 python3 python3-dev python3-distutils python3-venv python3-pip echo " " echo "# end apt install" @@ -122,45 +163,21 @@ PROVISIONING_ENV = <<-SHELL echo "# ------------------------------------------------------ #" SHELL -# Set some symlinks to make it easier to get to the UxAS-related repos -PROVISIONING_LINKS = <<-SHELL - echo " " - echo "# ------------------------------------------------------ #" - echo "# creating links" - cd /home/vagrant - - sudo -u vagrant mkdir -p uxas - - cd uxas - - # run as vagrant - sudo -u vagrant ln -fs ~vagrant/bootstrap/sbx/vcs/openuxas OpenUxAS - sudo -u vagrant ln -fs ~vagrant/bootstrap/sbx/vcs/amase OpenAMASE - sudo -u vagrant ln -fs ~vagrant/bootstrap/sbx/vcs/lmcpgen LmcpGen - - echo " " - echo "# end creating links" - echo "# ------------------------------------------------------ #" -SHELL - MOTD_MESSAGE = <<-SHELL + ------------------------------------------------------------------------------- -Ubuntu 18.04 OpenUxAS Development Vagrant Box +Ubuntu 20.04 OpenUxAS Development Vagrant Box ------------------------------------------------------------------------------- This machine has been preconfigured with all dependencies required to build and run OpenUxAS. To get started, run the following command: - cd ~vagrant/bootstrap && ./anod-build uxas + cd ~/bootstrap && ./anod-build uxas That will build the C++ version of OpenUxAS. Additional instructions can be -found in the README in ~vagrant/bootstrap/README.md (or more easily read on +found in the README in ~/bootstrap/README.md (or more easily read on github at https://github.com/AdaCore/OpenUxAS-bootstrap). -After uxas is built for the first time, the links under ~vagrant/uxas can be -used to quickly navigate to the OpenUxAS, OpenAMASE, or LMCPgen repositories. - - SHELL # Set the above MOTD so that the user can have some guidance upon login. @@ -172,7 +189,7 @@ PROVISIONING_GUI = <<-SHELL echo " " echo "# ------------------------------------------------------ #" echo "# apt-get install ubuntu-desktop " - DEBIAN_FRONTEND=noninteractive apt-get install -y ubuntu-desktop libncurses5 virtualbox-guest-dkms + apt-get install -y ubuntu-desktop libncurses5 virtualbox-guest-dkms echo "# end apt-get install ubuntu-desktop " echo "# ------------------------------------------------------ #" @@ -184,13 +201,49 @@ PROVISIONING_GUI = <<-SHELL echo "# ------------------------------------------------------ #" SHELL + +# This function will take our provisioning fragments and turn them into a +# sequence of commands run through `log_report`. +# +# Each command must be on a single line, or this will not work. Comment and +# blank lines are skipped. +# +# Simple if statements are also skipped, but this is brittle and should be +# treated with caution. +# +# Commands that redirect their output to files are also skipped. +def build_logged_commands(commands) + script = LOG_REPORT_FUNCTION + script += "\n" + + script += commands.split("\n"). + reject { |line| line if line.match(/^\s*#/) }. + reject { |line| line if line.match(/^\s*$/) }. + collect { |line| + if line.include?('>>') or + line.match(/^\s*if/) or + line.match(/^\s*fi/) + then + line + else + 'log_report ' + line.strip + end + }.join("\n") +end + +# Initial provisioning +INIT_PROVISIONING = build_logged_commands(PROVISIONING_DATE + + PROVISIONING_APT) + # All machines need this provisioning -COMMON_PROVISIONING = PROVISIONING_REPOS + - PROVISIONING_GNAT_DOWNLOAD + - PROVISIONING_DEPENDENCIES + - PROVISIONING_ENV + - PROVISIONING_LINKS + - PROVISIONING_MOTD +COMMON_PROVISIONING = build_logged_commands(PROVISIONING_REPOS + + PROVISIONING_GNAT_DOWNLOAD + + PROVISIONING_DEPENDENCIES + + PROVISIONING_ENV) + "\n" + + PROVISIONING_MOTD + +# GUI machines need this provisioning +GUI_PROVISIONING = build_logged_commands(PROVISIONING_GUI) # All Vagrant configuration is done below. The "2" in Vagrant.configure # configures the configuration version (Vagrant supports older styles for @@ -232,8 +285,8 @@ Vagrant.configure("2") do |config| config.vm.synced_folder COMMUNITY_FOLDER, "/home/vagrant/software/gnat_community" end - # Common provisioning - config.vm.provision "shell", inline: PROVISIONING_APT + # Initial provisioning + config.vm.provision "shell", inline: INIT_PROVISIONING # This defines the non-graphical VM. Does not depend on plugins, to keep the # VM build as fast as possible. @@ -267,6 +320,6 @@ Vagrant.configure("2") do |config| end uxas_gui.vm.provision "shell", inline: COMMON_PROVISIONING - uxas_gui.vm.provision "shell", inline: PROVISIONING_GUI + uxas_gui.vm.provision "shell", inline: GUI_PROVISIONING end end diff --git a/build-vagrant-gui b/build-vagrant-gui deleted file mode 100755 index 116d758..0000000 --- a/build-vagrant-gui +++ /dev/null @@ -1,12 +0,0 @@ -#! /bin/bash - -# This script will build the Vagrant GUI machine and then run the three -# relevant builds for UXAS: the C++ version, the Ada version, and Amase. - -MACHINE=uxas-gui - -vagrant up $MACHINE &&\ -vagrant reload $MACHINE &&\ -vagrant ssh $MACHINE -c "cd bootstrap && python3 anod-build uxas" &&\ -vagrant ssh $MACHINE -c "cd bootstrap && python3 anod-build amase" &&\ -vagrant ssh $MACHINE -c "cd bootstrap && python3 anod-build uxas-ada" \ No newline at end of file diff --git a/community.patch b/community.patch deleted file mode 100644 index 97f0199..0000000 --- a/community.patch +++ /dev/null @@ -1,731 +0,0 @@ -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfdlli.adb lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfdlli.adb -index 19aa83f..1f23f4b 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfdlli.adb -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfdlli.adb -@@ -15,9 +15,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfdlli.ads lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfdlli.ads -index 0f19707..b8df023 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfdlli.ads -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfdlli.ads -@@ -19,9 +19,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -@@ -34,6 +34,7 @@ with Ada.Containers.Functional_Maps; - - generic - type Element_Type is private; -+ with function "=" (Left, Right : Element_Type) return Boolean is <>; - - package Ada.Containers.Formal_Doubly_Linked_Lists with - SPARK_Mode -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhama.adb lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhama.adb -index 8e14832..580ca12 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhama.adb -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhama.adb -@@ -15,9 +15,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhama.ads lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhama.ads -index 4ba1e83..c4e8221 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhama.ads -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhama.ads -@@ -19,9 +19,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -@@ -59,6 +59,7 @@ generic - with function Equivalent_Keys - (Left : Key_Type; - Right : Key_Type) return Boolean is "="; -+ with function "=" (Left, Right : Element_Type) return Boolean is <>; - - package Ada.Containers.Formal_Hashed_Maps with - SPARK_Mode -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhase.adb lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhase.adb -index fb2872c..8cc220c 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhase.adb -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhase.adb -@@ -15,9 +15,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhase.ads lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhase.ads -index ea53a9d..3e72aef 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhase.ads -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfhase.ads -@@ -19,9 +19,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -@@ -355,10 +355,24 @@ is - "="'Result = - (E_Elements_Included (Elements (Left), Elements (Right)) - and E_Elements_Included (Elements (Right), Elements (Left))); -+ -- For each element in Left, set equality attempts to find the equal -+ -- element in Right; if a search fails, then set equality immediately -+ -- returns False. The search works by calling Hash to find the bucket in -+ -- the Right set that corresponds to the Left element. If the bucket is -+ -- non-empty, the search calls the generic formal element equality operator -+ -- to compare the element (in Left) to the element of each node in the -+ -- bucket (in Right); the search terminates when a matching node in the -+ -- bucket is found, or the nodes in the bucket are exhausted. (Note that -+ -- element equality is called here, not Equivalent_Elements. Set equality -+ -- is the only operation in which element equality is used. Compare set -+ -- equality to Equivalent_Sets, which does call Equivalent_Elements.) - - function Equivalent_Sets (Left, Right : Set) return Boolean with - Global => null, - Post => Equivalent_Sets'Result = (Model (Left) = Model (Right)); -+ -- Similar to set equality, with the difference that the element in Left is -+ -- compared to the elements in Right using the generic formal -+ -- Equivalent_Elements operation instead of element equality. - - function To_Set (New_Item : Element_Type) return Set with - Global => null, -@@ -366,10 +380,14 @@ is - M.Is_Singleton (Model (To_Set'Result), New_Item) - and Length (To_Set'Result) = 1 - and E.Get (Elements (To_Set'Result), 1) = New_Item; -+ -- Constructs a singleton set comprising New_Element. To_Set calls Hash to -+ -- determine the bucket for New_Item. - - function Capacity (Container : Set) return Count_Type with - Global => null, - Post => Capacity'Result = Container.Capacity; -+ -- Returns the current capacity of the set. Capacity is the maximum length -+ -- before which rehashing in guaranteed not to occur. - - procedure Reserve_Capacity - (Container : in out Set; -@@ -387,14 +405,21 @@ is - (Elements (Container), Elements (Container)'Old) - and E_Elements_Included - (Elements (Container)'Old, Elements (Container)); -+ -- If the value of the Capacity actual parameter is less or equal to -+ -- Container.Capacity, then the operation has no effect. Otherwise it -+ -- raises Capacity_Error (as no expansion of capacity is possible for a -+ -- bounded form). - - function Is_Empty (Container : Set) return Boolean with - Global => null, - Post => Is_Empty'Result = (Length (Container) = 0); -+ -- Equivalent to Length (Container) = 0 - - procedure Clear (Container : in out Set) with - Global => null, - Post => Length (Container) = 0 and M.Is_Empty (Model (Container)); -+ -- Removes all of the items from the set. This will deallocate all memory -+ -- associated with this set. - - procedure Assign (Target : in out Set; Source : Set) with - Global => null, -@@ -407,6 +432,10 @@ is - - and E_Elements_Included (Elements (Target), Elements (Source)) - and E_Elements_Included (Elements (Source), Elements (Target)); -+ -- If Target denotes the same object as Source, then the operation has no -+ -- effect. If the Target capacity is less than the Source length, then -+ -- Assign raises Capacity_Error. Otherwise, Assign clears Target and then -+ -- copies the (active) elements from Source to Target. - - function Copy - (Source : Set; -@@ -422,6 +451,14 @@ is - Copy'Result.Capacity = Source.Capacity - else - Copy'Result.Capacity = Capacity); -+ -- Constructs a new set object whose elements correspond to Source. If the -+ -- Capacity parameter is 0, then the capacity of the result is the same as -+ -- the length of Source. If the Capacity parameter is equal or greater than -+ -- the length of Source, then the capacity of the result is the specified -+ -- value. Otherwise, Copy raises Capacity_Error. If the Modulus parameter -+ -- is 0, then the modulus of the result is the value returned by a call to -+ -- Default_Modulus with the capacity parameter determined as above; -+ -- otherwise the modulus of the result is the specified value. - - function Element - (Container : Set; -@@ -485,6 +522,8 @@ is - - and E_Elements_Included (Elements (Target), Elements (Source)'Old) - and E_Elements_Included (Elements (Source)'Old, Elements (Target)); -+ -- Clears Target (if it's not empty), and then moves (not copies) the -+ -- buckets array and nodes from Source to Target. - - procedure Insert - (Container : in out Set; -@@ -541,6 +580,18 @@ is - (Positions (Container), - Positions (Container)'Old, - Position)); -+ -- Conditionally inserts New_Item into the set. If New_Item is already in -+ -- the set, then Inserted returns False and Position designates the node -+ -- containing the existing element (which is not modified). If New_Item is -+ -- not already in the set, then Inserted returns True and Position -+ -- designates the newly-inserted node containing New_Item. The search for -+ -- an existing element works as follows. Hash is called to determine -+ -- New_Item's bucket; if the bucket is non-empty, then Equivalent_Elements -+ -- is called to compare New_Item to the element of each node in that -+ -- bucket. If the bucket is empty, or there were no equivalent elements in -+ -- the bucket, the search "fails" and the New_Item is inserted in the set -+ -- (and Inserted returns True); otherwise, the search "succeeds" (and -+ -- Inserted returns False). - - procedure Insert (Container : in out Set; New_Item : Element_Type) with - Global => null, -@@ -570,6 +621,13 @@ is - (Positions (Container), - Positions (Container)'Old, - Find (Container, New_Item)); -+ -- Attempts to insert New_Item into the set, performing the usual insertion -+ -- search (which involves calling both Hash and Equivalent_Elements); if -+ -- the search succeeds (New_Item is equivalent to an element already in the -+ -- set, and so was not inserted), then this operation raises -+ -- Constraint_Error. (This version of Insert is similar to Replace, but -+ -- having the opposite exception behavior. It is intended for use when you -+ -- want to assert that the item is not already in the set.) - - procedure Include (Container : in out Set; New_Item : Element_Type) with - Global => null, -@@ -625,6 +683,13 @@ is - (Positions (Container), - Positions (Container)'Old, - Find (Container, New_Item))); -+ -- Attempts to insert New_Item into the set. If an element equivalent to -+ -- New_Item is already in the set (the insertion search succeeded, and -+ -- hence New_Item was not inserted), then the value of New_Item is assigned -+ -- to the existing element. (This insertion operation only raises an -+ -- exception if cursor tampering occurs. It is intended for use when you -+ -- want to insert the item in the set, and you don't care whether an -+ -- equivalent element is already present.) - - procedure Replace (Container : in out Set; New_Item : Element_Type) with - Global => null, -@@ -648,6 +713,12 @@ is - (Elements (Container)'Old, - Elements (Container), - P.Get (Positions (Container), Find (Container, New_Item))); -+ -- Searches for New_Item in the set; if the search fails (because an -+ -- equivalent element was not in the set), then it raises -+ -- Constraint_Error. Otherwise, the existing element is assigned the value -+ -- New_Item. (This is similar to Insert, but with the opposite exception -+ -- behavior. It is intended for use when you want to assert that the item -+ -- is already in the set.) - - procedure Exclude (Container : in out Set; Item : Element_Type) with - Global => null, -@@ -685,6 +756,13 @@ is - (Positions (Container)'Old, - Positions (Container), - Find (Container, Item)'Old)); -+ -- Searches for Item in the set, and if found, removes its node from the -+ -- set and then deallocates it. The search works as follows. The operation -+ -- calls Hash to determine the item's bucket; if the bucket is not empty, -+ -- it calls Equivalent_Elements to compare Item to the element of each node -+ -- in the bucket. (This is the deletion analog of Include. It is intended -+ -- for use when you want to remove the item from the set, but don't care -+ -- whether the item is already in the set.) - - procedure Delete (Container : in out Set; Item : Element_Type) with - Global => null, -@@ -715,6 +793,12 @@ is - (Positions (Container)'Old, - Positions (Container), - Find (Container, Item)'Old); -+ -- Searches for Item in the set (which involves calling both Hash and -+ -- Equivalent_Elements). If the search fails, then the operation raises -+ -- Constraint_Error. Otherwise it removes the node from the set and then -+ -- deallocates it. (This is the deletion analog of non-conditional -+ -- Insert. It is intended for use when you want to assert that the item is -+ -- already in the set.) - - procedure Delete (Container : in out Set; Position : in out Cursor) with - Global => null, -@@ -747,6 +831,10 @@ is - (Positions (Container)'Old, - Positions (Container), - Position'Old); -+ -- Removes the node designated by Position from the set, and then -+ -- deallocates the node. The operation calls Hash to determine the bucket, -+ -- and then compares Position to each node in the bucket until there's a -+ -- match (it does not call Equivalent_Elements). - - procedure Union (Target : in out Set; Source : Set) with - Global => null, -@@ -795,6 +883,8 @@ is - E_Right => Elements (Target), - P_Left => Positions (Target)'Old, - P_Right => Positions (Target)); -+ -- Iterates over the Source set, and conditionally inserts each element -+ -- into Target. - - function Union (Left, Right : Set) return Set with - Global => null, -@@ -831,6 +921,8 @@ is - Model (Left), - Elements (Right), - Elements (Union'Result)); -+ -- The operation first copies the Left set to the result, and then iterates -+ -- over the Right set to conditionally insert each element into the result. - - function "or" (Left, Right : Set) return Set renames Union; - -@@ -866,6 +958,9 @@ is - E_Right => Elements (Target)'Old, - P_Left => Positions (Target), - P_Right => Positions (Target)'Old); -+ -- Iterates over the Target set (calling First and Next), calling Find to -+ -- determine whether the element is in Source. If an equivalent element is -+ -- not found in Source, the element is deleted from Target. - - function Intersection (Left, Right : Set) return Set with - Global => null, -@@ -891,6 +986,9 @@ is - and E_Elements_Included - (Elements (Left), Model (Right), - Elements (Intersection'Result)); -+ -- Iterates over the Left set, calling Find to determine whether the -+ -- element is in Right. If an equivalent element is found, it is inserted -+ -- into the result set. - - function "and" (Left, Right : Set) return Set renames Intersection; - -@@ -926,6 +1024,9 @@ is - E_Right => Elements (Target)'Old, - P_Left => Positions (Target), - P_Right => Positions (Target)'Old); -+ -- Iterates over the Source (calling First and Next), calling Find to -+ -- determine whether the element is in Target. If an equivalent element is -+ -- found, it is deleted from Target. - - function Difference (Left, Right : Set) return Set with - Global => null, -@@ -955,6 +1056,9 @@ is - (Elements (Left), - Model (Difference'Result), - Elements (Difference'Result)); -+ -- Iterates over the Left set, calling Find to determine whether the -+ -- element is in the Right set. If an equivalent element is not found, the -+ -- element is inserted into the result set. - - function "-" (Left, Right : Set) return Set renames Difference; - -@@ -995,6 +1099,10 @@ is - - and E_Elements_Included - (Elements (Source), Model (Target), Elements (Target)); -+ -- The operation iterates over the Source set, searching for the element -+ -- in Target (calling Hash and Equivalent_Elements). If an equivalent -+ -- element is found, it is removed from Target; otherwise it is inserted -+ -- into Target. - - function Symmetric_Difference (Left, Right : Set) return Set with - Global => null, -@@ -1042,6 +1150,12 @@ is - (Elements (Right), - Model (Symmetric_Difference'Result), - Elements (Symmetric_Difference'Result)); -+ -- The operation first iterates over the Left set. It calls Find to -+ -- determine whether the element is in the Right set. If no equivalent -+ -- element is found, the element from Left is inserted into the result. The -+ -- operation then iterates over the Right set, to determine whether the -+ -- element is in the Left set. If no equivalent element is found, the Right -+ -- element is inserted into the result. - - function "xor" (Left, Right : Set) return Set - renames Symmetric_Difference; -@@ -1050,10 +1164,21 @@ is - Global => null, - Post => - Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right))); -+ -- Iterates over the Left set (calling First and Next), calling Find to -+ -- determine whether the element is in the Right set. If an equivalent -+ -- element is found, the operation immediately returns True. The operation -+ -- returns False if the iteration over Left terminates without finding any -+ -- equivalent element in Right. - - function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with - Global => null, - Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set)); -+ -- Iterates over Subset (calling First and Next), calling Find to determine -+ -- whether the element is in Of_Set. If no equivalent element is found in -+ -- Of_Set, the operation immediately returns False. The operation returns -+ -- True if the iteration over Subset terminates without finding an element -+ -- not in Of_Set (that is, every element in Subset is equivalent to an -+ -- element in Of_Set). - - function First (Container : Set) return Cursor with - Global => null, -@@ -1064,6 +1189,8 @@ is - others => - Has_Element (Container, First'Result) - and P.Get (Positions (Container), First'Result) = 1); -+ -- Returns a cursor that designates the first non-empty bucket, by -+ -- searching from the beginning of the buckets array. - - function Next (Container : Set; Position : Cursor) return Cursor with - Global => null, -@@ -1079,6 +1206,12 @@ is - Has_Element (Container, Next'Result) - and then P.Get (Positions (Container), Next'Result) = - P.Get (Positions (Container), Position) + 1); -+ -- Returns a cursor that designates the node that follows the current one -+ -- designated by Position. If Position designates the last node in its -+ -- bucket, the operation calls Hash to compute the index of this bucket, -+ -- and searches the buckets array for the first non-empty bucket, starting -+ -- from that index; otherwise, it simply follows the link to the next node -+ -- in the same bucket. - - procedure Next (Container : Set; Position : in out Cursor) with - Global => null, -@@ -1094,6 +1227,7 @@ is - Has_Element (Container, Position) - and then P.Get (Positions (Container), Position) = - P.Get (Positions (Container), Position'Old) + 1); -+ -- Equivalent to Position := Next (Position) - - function Find - (Container : Set; -@@ -1118,6 +1252,11 @@ is - - and Equivalent_Elements - (Element (Container, Find'Result), Item)); -+ -- Searches for Item in the set. Find calls Hash to determine the item's -+ -- bucket; if the bucket is not empty, it calls Equivalent_Elements to -+ -- compare Item to each element in the bucket. If the search succeeds, Find -+ -- returns a cursor designating the node containing the equivalent element; -+ -- otherwise, it returns No_Element. - - function Contains (Container : Set; Item : Element_Type) return Boolean with - Global => null, -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfinve.adb lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfinve.adb -index 75a4268..a187128 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfinve.adb -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfinve.adb -@@ -15,9 +15,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -@@ -457,7 +457,7 @@ is - Item : Element_Type; - Index : Index_Type := Index_Type'First) return Extended_Index - is -- K : Capacity_Range; -+ K : Count_Type; - Last : constant Index_Type := Last_Index (Container); - - begin -@@ -1277,7 +1277,7 @@ is - Index : Index_Type := Index_Type'Last) return Extended_Index - is - Last : Index_Type'Base; -- K : Capacity_Range; -+ K : Count_Type'Base; - - begin - if Index > Last_Index (Container) then -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfinve.ads lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfinve.ads -index 29d8334..87940d2 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfinve.ads -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cfinve.ads -@@ -19,9 +19,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -@@ -38,6 +38,7 @@ with Ada.Containers.Functional_Vectors; - generic - type Index_Type is range <>; - type Element_Type (<>) is private; -+ with function "=" (Left, Right : Element_Type) return Boolean is <>; - Max_Size_In_Storage_Elements : Natural; - -- Maximum size of Vector elements in bytes. This has the same meaning as - -- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforma.adb lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforma.adb -index ffb5582..15d142d 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforma.adb -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforma.adb -@@ -15,9 +15,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforma.ads lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforma.ads -index a2d1819..a13bce4 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforma.ads -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforma.ads -@@ -19,9 +19,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -@@ -58,6 +58,7 @@ generic - type Element_Type is private; - - with function "<" (Left, Right : Key_Type) return Boolean is <>; -+ with function "=" (Left, Right : Element_Type) return Boolean is <>; - - package Ada.Containers.Formal_Ordered_Maps with - SPARK_Mode -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforse.adb lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforse.adb -index cdd99a8..71d9b47 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforse.adb -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforse.adb -@@ -15,9 +15,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforse.ads lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforse.ads -index b1f3762..3cd62af 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforse.ads -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cforse.ads -@@ -19,9 +19,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cofove.adb lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cofove.adb -index 5a3a62f..3a10d32 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cofove.adb -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cofove.adb -@@ -15,9 +15,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -@@ -378,7 +378,7 @@ is - Item : Element_Type; - Index : Index_Type := Index_Type'First) return Extended_Index - is -- K : Capacity_Range; -+ K : Count_Type; - Last : constant Index_Type := Last_Index (Container); - - begin -@@ -1147,7 +1147,7 @@ is - Index : Index_Type := Index_Type'Last) return Extended_Index - is - Last : Index_Type'Base; -- K : Capacity_Range; -+ K : Count_Type'Base; - - begin - if Index > Last_Index (Container) then -diff --git lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cofove.ads lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cofove.ads -index 4a39d83..5fb3bc9 100644 ---- lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cofove.ads -+++ lib/gcc/x86_64-pc-linux-gnu/8.3.1/rts-native/adainclude/a-cofove.ads -@@ -19,9 +19,9 @@ - -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- - -- or FITNESS FOR A PARTICULAR PURPOSE. -- - -- -- ---- -- ---- -- ---- -- -+-- As a special exception under Section 7 of GPL version 3, you are granted -- -+-- additional permissions described in the GCC Runtime Library Exception, -- -+-- version 3.1, as published by the Free Software Foundation. -- - -- -- - -- You should have received a copy of the GNU General Public License and -- - -- a copy of the GCC Runtime Library Exception along with this program; -- -@@ -40,6 +40,8 @@ with Ada.Containers.Functional_Vectors; - generic - type Index_Type is range <>; - type Element_Type is private; -+ with function "=" (Left, Right : Element_Type) return Boolean is <>; -+ - package Ada.Containers.Formal_Vectors with - SPARK_Mode - is -@@ -68,7 +70,11 @@ is - subtype Capacity_Range is Count_Type range 0 .. Last_Count; - - type Vector (Capacity : Capacity_Range) is private with -- Default_Initial_Condition => Is_Empty (Vector); -+ Default_Initial_Condition => Is_Empty (Vector), -+ Iterable => (First => Iter_First, -+ Has_Element => Iter_Has_Element, -+ Next => Iter_Next, -+ Element => Element); - - function Length (Container : Vector) return Capacity_Range with - Global => null, -@@ -171,6 +177,7 @@ is - Ghost, - Global => null, - Post => M.Length (Model'Result) = Length (Container); -+ pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Model); - - function Element - (S : M.Sequence; -@@ -857,6 +864,30 @@ is - Model (Target)'Old); - end Generic_Sorting; - -+ --------------------------- -+ -- Iteration Primitives -- -+ --------------------------- -+ -+ function Iter_First (Container : Vector) return Extended_Index with -+ Global => null; -+ -+ function Iter_Has_Element -+ (Container : Vector; -+ Position : Extended_Index) return Boolean -+ with -+ Global => null, -+ Post => -+ Iter_Has_Element'Result = -+ (Position in Index_Type'First .. Last_Index (Container)); -+ pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element); -+ -+ function Iter_Next -+ (Container : Vector; -+ Position : Extended_Index) return Extended_Index -+ with -+ Global => null, -+ Pre => Iter_Has_Element (Container, Position); -+ - private - pragma SPARK_Mode (Off); - -@@ -880,4 +911,22 @@ private - function Empty_Vector return Vector is - ((Capacity => 0, others => <>)); - -+ function Iter_First (Container : Vector) return Extended_Index is -+ (Index_Type'First); -+ -+ function Iter_Next -+ (Container : Vector; -+ Position : Extended_Index) return Extended_Index -+ is -+ (if Position = Extended_Index'Last then -+ Extended_Index'First -+ else -+ Extended_Index'Succ (Position)); -+ -+ function Iter_Has_Element -+ (Container : Vector; -+ Position : Extended_Index) return Boolean -+ is -+ (Position in Index_Type'First .. Container.Last); -+ - end Ada.Containers.Formal_Vectors;