[multiple changes]

2017-04-27  Bob Duff  <duff@adacore.com>

	* g-dyntab.ads, g-dyntab.adb: Add assertions to subprograms that
	can reallocate.
	* atree.adb, elists.adb, fname-uf.adb, ghost.adb, inline.adb,
	* lib.adb, namet.adb, nlists.adb, sem.adb, sinput.adb, stringt.adb:
	Reorder code so that above assertions do not fail.
	* table.ads: Remove obsolete comment on Locked.

2017-04-27  Claire Dross  <dross@adacore.com>

	* a-cfdlli.ads: Code cleanup.

2017-04-27  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK_Freeze_Type): Build a DIC procedure
	when needed for proof.	(Expand_SPARK): Call the new procedure.
	* exp_util.ads Fix typo.

2017-04-27  Gary Dismukes  <dismukes@adacore.com>

	* a-cofuma.ads, a-cfhama.ads: Minor reformatting, grammar, and typo
	fixes.

From-SVN: r247323

gcc/ada/ChangeLog

+2017-04-27  Bob Duff  <duff@adacore.com>
+
+	* g-dyntab.ads, g-dyntab.adb: Add assertions to subprograms that
+	can reallocate.
+	* atree.adb, elists.adb, fname-uf.adb, ghost.adb, inline.adb,
+	* lib.adb, namet.adb, nlists.adb, sem.adb, sinput.adb, stringt.adb:
+	Reorder code so that above assertions do not fail.
+	* table.ads: Remove obsolete comment on Locked.
+
+2017-04-27  Claire Dross  <dross@adacore.com>
+
+	* a-cfdlli.ads: Code cleanup.
+
+2017-04-27  Yannick Moy  <moy@adacore.com>
+
+	* exp_spark.adb (Expand_SPARK_Freeze_Type): Build a DIC procedure
+	when needed for proof.	(Expand_SPARK): Call the new procedure.
+	* exp_util.ads Fix typo.
+
+2017-04-27  Gary Dismukes  <dismukes@adacore.com>
+
+	* a-cofuma.ads, a-cfhama.ads: Minor reformatting, grammar, and typo
+	fixes.
+
 2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_elab.adb Add new type Visited_Element

gcc/ada/a-cfdlli.ads

@@ -175,7 +175,7 @@ is
 
             --  Big contains all cursors of Small
 
-            P.Keys_Included (Small, Big)
+            (P.Keys_Included (Small, Big)
 
               --  Cursors located before Cut are not moved, cursors located
               --  after are shifted by Count.
@@ -191,7 +191,7 @@ is
 
               and (for all I of Big =>
                     P.Has_Key (Small, I)
-                      or P.Get (Big, I) - Count in Cut - Count  .. Cut - 1);
+                      or P.Get (Big, I) - Count in Cut - Count  .. Cut - 1));
 
       function P_Positions_Swapped
         (Left  : P.Map;

gcc/ada/a-cfhama.ads

@@ -44,8 +44,8 @@
 --    and its previous version C'Old) for expressing properties, which is not
 --    possible if cursors encapsulate an access to the underlying container.
 
---  Iteration over maps is done using the Iterable aspect which is SPARK
---  compatible. For of iteration ranges over keys instead of elements.
+--  Iteration over maps is done using the Iterable aspect, which is SPARK
+--  compatible. "For of" iteration ranges over keys instead of elements.
 
 with Ada.Containers.Functional_Vectors;
 with Ada.Containers.Functional_Maps;
@@ -153,7 +153,7 @@ is
                      K.Get (K_Right, P.Get (P_Right, C))));
 
       function Model (Container : Map) return M.Map with
-      --  The highlevel model of a map is a map from keys to elements. Neither
+      --  The high-level model of a map is a map from keys to elements. Neither
       --  cursors nor order of elements are represented in this model. Keys are
       --  modeled up to equivalence.
 
@@ -193,14 +193,14 @@ is
 
       function Positions (Container : Map) return P.Map with
       --  The Positions map is used to model cursors. It only contains valid
-      --  cursors and map them to their position in the container.
+      --  cursors and maps them to their position in the container.
 
         Ghost,
         Global => null,
         Post   =>
           not P.Has_Key (Positions'Result, No_Element)
 
-            --  Positions of cursors are smaller than the container's length.
+            --  Positions of cursors are smaller than the container's length
 
             and then
               (for all I of Positions'Result =>
@@ -217,11 +217,11 @@ is
 
       procedure Lift_Abstraction_Level (Container : Map) with
         --  Lift_Abstraction_Level is a ghost procedure that does nothing but
-        --  assume that we can access to the same elements by iterating over
+        --  assume that we can access the same elements by iterating over
         --  positions or cursors.
         --  This information is not generally useful except when switching from
-        --  a lowlevel, cursor aware view of a container, to a highlevel
-        --  position based view.
+        --  a low-level, cursor-aware view of a container, to a high-level,
+        --  position-based view.
 
         Ghost,
         Global => null,
@@ -328,17 +328,17 @@ is
      Pre    => Has_Element (Container, Position),
      Post   =>
 
-       --  Order of keys and cursors are preserved
+       --  Order of keys and cursors is preserved
 
        Keys (Container) = Keys (Container)'Old
          and Positions (Container) = Positions (Container)'Old
 
-         --  New_Item is now associated to the key at position Position in
+         --  New_Item is now associated with the key at position Position in
          --  Container.
 
          and Element (Container, Position) = New_Item
 
-         --  Elements associated to other keys are preserved
+         --  Elements associated with other keys are preserved
 
          and M.Same_Keys (Model (Container), Model (Container)'Old)
          and M.Elements_Equal_Except
@@ -405,7 +405,7 @@ is
                    Model (Container)'Old,
                    Key)
 
-            --  Mapping from cursors to keys are preserved
+            --  Mapping from cursors to keys is preserved
 
             and Mapping_Preserved
                   (K_Left  => Keys (Container)'Old,
@@ -443,7 +443,7 @@ is
                 Model (Container)'Old,
                 Key)
 
-         --  Mapping from cursors to keys are preserved
+         --  Mapping from cursors to keys is preserved
 
          and Mapping_Preserved
                (K_Left  => Keys (Container)'Old,
@@ -485,7 +485,7 @@ is
                    Keys (Container),
                    P.Get (Positions (Container), Find (Container, Key)))
 
-            --  Elements associated to other keys are preserved
+            --  Elements associated with other keys are preserved
 
             and M.Same_Keys (Model (Container), Model (Container)'Old)
             and M.Elements_Equal_Except
@@ -506,7 +506,7 @@ is
                    Model (Container)'Old,
                    Key)
 
-            --  Mapping from cursors to keys are preserved
+            --  Mapping from cursors to keys is preserved
 
             and Mapping_Preserved
                   (K_Left  => Keys (Container)'Old,
@@ -540,11 +540,11 @@ is
                Keys (Container),
                P.Get (Positions (Container), Find (Container, Key)))
 
-         --  New_Item is now associated to the Key in Container
+         --  New_Item is now associated with the Key in Container
 
          and Element (Model (Container), Key) = New_Item
 
-         --  Elements associated to other keys are preserved
+         --  Elements associated with other keys are preserved
 
          and M.Same_Keys (Model (Container), Model (Container)'Old)
          and M.Elements_Equal_Except
@@ -577,7 +577,7 @@ is
                    Model (Container),
                    Key)
 
-            --  Mapping from cursors to keys are preserved
+            --  Mapping from cursors to keys is preserved
 
             and Mapping_Preserved
                   (K_Left  => Keys (Container),
@@ -607,7 +607,7 @@ is
                 Model (Container),
                 Key)
 
-         --  Mapping from cursors to keys are preserved
+         --  Mapping from cursors to keys is preserved
 
          and Mapping_Preserved
                (K_Left  => Keys (Container),
@@ -639,7 +639,7 @@ is
                 Model (Container),
                 Key (Container, Position)'Old)
 
-         --  Mapping from cursors to keys are preserved
+         --  Mapping from cursors to keys is preserved
 
          and Mapping_Preserved
                (K_Left  => Keys (Container),
@@ -700,7 +700,7 @@ is
        (not Contains (Model (Container), Key) =>
           Find'Result = No_Element,
 
-        --  Otherwise, Find returns a valid cusror in Container
+        --  Otherwise, Find returns a valid cursor in Container
 
         others =>
           P.Has_Key (Positions (Container), Find'Result)

gcc/ada/a-cofuma.ads

@@ -48,7 +48,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
    --  Maps are empty when default initialized.
    --  "For in" quantification over maps should not be used.
    --  "For of" quantification over maps iterates over keys.
-   --  Note that, for proof, for of quantification is understood modulo
+   --  Note that, for proof, "for of" quantification is understood modulo
    --  equivalence (quantification includes keys equivalent to keys of the
    --  map).
 

gcc/ada/atree.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -1579,12 +1579,12 @@ package body Atree is
 
    procedure Lock is
    begin
-      Nodes.Locked := True;
-      Flags.Locked := True;
-      Orig_Nodes.Locked := True;
       Nodes.Release;
+      Nodes.Locked := True;
       Flags.Release;
+      Flags.Locked := True;
       Orig_Nodes.Release;
+      Orig_Nodes.Locked := True;
    end Lock;
 
    ----------------

gcc/ada/elists.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -320,10 +320,10 @@ package body Elists is
 
    procedure Lock is
    begin
-      Elists.Locked := True;
-      Elmts.Locked := True;
       Elists.Release;
+      Elists.Locked := True;
       Elmts.Release;
+      Elmts.Locked := True;
    end Lock;
 
    --------------------

gcc/ada/exp_spark.adb

@@ -53,6 +53,9 @@ package body Exp_SPARK is
    --  Replace occurrences of System'To_Address by calls to
    --  System.Storage_Elements.To_Address
 
+   procedure Expand_SPARK_Freeze_Type (E : Entity_Id);
+   --  Build the DIC procedure of a type when needed, if not already done
+
    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
    --  Perform object-declaration-specific expansion
 
@@ -122,6 +125,11 @@ package body Exp_SPARK is
          when N_Object_Renaming_Declaration =>
             Expand_SPARK_N_Object_Renaming_Declaration (N);
 
+         when N_Freeze_Entity =>
+            if Is_Type (Entity (N)) then
+               Expand_SPARK_Freeze_Type (Entity (N));
+            end if;
+
          --  In SPARK mode, no other constructs require expansion
 
          when others =>
@@ -233,6 +241,23 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_N_Attribute_Reference;
 
+   ------------------------------
+   -- Expand_SPARK_Freeze_Type --
+   ------------------------------
+
+   procedure Expand_SPARK_Freeze_Type (E : Entity_Id) is
+   begin
+      --  When a DIC is inherited by a tagged type, it may need to be
+      --  specialized to the descendant type, hence build a separate DIC
+      --  procedure for it as done during regular expansion for compilation.
+
+      if Has_DIC (E)
+        and then Is_Tagged_Type (E)
+      then
+         Build_DIC_Procedure_Body (E, For_Freeze => True);
+      end if;
+   end Expand_SPARK_Freeze_Type;
+
    ---------------------------------------
    -- Expand_SPARK_N_Object_Declaration --
    ---------------------------------------

gcc/ada/exp_util.ads

@@ -283,7 +283,7 @@ package Exp_Util is
       For_Freeze : Boolean := False);
    --  Create the body of the procedure which verifies the assertion expression
    --  of pragma Default_Initial_Condition at run time. Flag For_Freeze should
-   --  be set when the body is construction as part of the freezing actions for
+   --  be set when the body is constructed as part of the freezing actions for
    --  Typ.
 
    procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id);

gcc/ada/fname-uf.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -549,8 +549,8 @@ package body Fname.UF is
 
    procedure Lock is
    begin
-      SFN_Table.Locked := True;
       SFN_Table.Release;
+      SFN_Table.Locked := True;
    end Lock;
 
    -------------------

gcc/ada/g-dyntab.adb

@@ -59,6 +59,7 @@ package body GNAT.Dynamic_Tables is
    begin
       --  Note that Num can be negative
 
+      pragma Assert (not T.Locked);
       Set_Last (T, T.P.Last + Table_Index_Type'Base (Num));
    end Allocate;
 
@@ -68,6 +69,7 @@ package body GNAT.Dynamic_Tables is
 
    procedure Append (T : in out Instance; New_Val : Table_Component_Type) is
    begin
+      pragma Assert (not T.Locked);
       Set_Item (T, T.P.Last + 1, New_Val);
    end Append;
 
@@ -88,6 +90,7 @@ package body GNAT.Dynamic_Tables is
 
    procedure Decrement_Last (T : in out Instance) is
    begin
+      pragma Assert (not T.Locked);
       Allocate (T, -1);
    end Decrement_Last;
 
@@ -118,6 +121,7 @@ package body GNAT.Dynamic_Tables is
    ----------
 
    procedure Free (T : in out Instance) is
+      pragma Assert (not T.Locked);
       subtype Alloc_Type is Table_Type (First .. T.P.Last_Allocated);
       type Alloc_Ptr is access all Alloc_Type;
 
@@ -228,6 +232,7 @@ package body GNAT.Dynamic_Tables is
 
    procedure Increment_Last (T : in out Instance) is
    begin
+      pragma Assert (not T.Locked);
       Allocate (T, 1);
    end Increment_Last;
 
@@ -237,6 +242,7 @@ package body GNAT.Dynamic_Tables is
 
    procedure Init (T : in out Instance) is
    begin
+      pragma Assert (not T.Locked);
       Free (T);
    end Init;
 
@@ -266,6 +272,8 @@ package body GNAT.Dynamic_Tables is
 
    procedure Move (From, To : in out Instance) is
    begin
+      pragma Assert (not From.Locked);
+      pragma Assert (not To.Locked);
       pragma Assert (Is_Empty (To));
       To := From;
 
@@ -281,6 +289,7 @@ package body GNAT.Dynamic_Tables is
    -------------
 
    procedure Release (T : in out Instance) is
+      pragma Assert (not T.Locked);
       Old_Last_Allocated : constant Table_Last_Type := T.P.Last_Allocated;
 
       function New_Last_Allocated return Table_Last_Type;
@@ -355,6 +364,7 @@ package body GNAT.Dynamic_Tables is
       Index : Valid_Table_Index_Type;
       Item  : Table_Component_Type)
    is
+      pragma Assert (not T.Locked);
       Item_Copy : constant Table_Component_Type := Item;
    begin
       --  If Set_Last is going to reallocate the table, we make a copy of Item,
@@ -386,6 +396,7 @@ package body GNAT.Dynamic_Tables is
 
    procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type) is
    begin
+      pragma Assert (not T.Locked);
       if New_Val > T.P.Last_Allocated then
          Grow (T, New_Val);
       end if;

gcc/ada/g-dyntab.ads

@@ -173,10 +173,10 @@ package GNAT.Dynamic_Tables is
       --  SCO_Unit_Table and SCO_Table in scos.h.
 
       Locked : Boolean := False;
-      --  Table expansion is permitted only if this is False. A client may set
-      --  Locked to True, in which case any attempt to expand the table will
-      --  cause an assertion failure. Note that while a table is locked, its
-      --  address in memory remains fixed and unchanging.
+      --  Table reallocation is permitted only if this is False. A client may
+      --  set Locked to True, in which case any operation that might expand or
+      --  shrink the table will cause an assertion failure. While a table is
+      --  locked, its address in memory remains fixed and unchanging.
 
       P : Table_Private;
    end record;

gcc/ada/ghost.adb

@@ -1091,8 +1091,8 @@ package body Ghost is
 
    procedure Lock is
    begin
-      Ignored_Ghost_Units.Locked := True;
       Ignored_Ghost_Units.Release;
+      Ignored_Ghost_Units.Locked := True;
    end Lock;
 
    -----------------------------------

gcc/ada/inline.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -4184,14 +4184,14 @@ package body Inline is
 
    procedure Lock is
    begin
-      Pending_Instantiations.Locked := True;
-      Inlined_Bodies.Locked := True;
-      Successors.Locked := True;
-      Inlined.Locked := True;
       Pending_Instantiations.Release;
+      Pending_Instantiations.Locked := True;
       Inlined_Bodies.Release;
+      Inlined_Bodies.Locked := True;
       Successors.Release;
+      Successors.Locked := True;
       Inlined.Release;
+      Inlined.Locked := True;
    end Lock;
 
    --------------------------------

gcc/ada/lib.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -1046,12 +1046,12 @@ package body Lib is
 
    procedure Lock is
    begin
-      Linker_Option_Lines.Locked := True;
-      Load_Stack.Locked := True;
-      Units.Locked := True;
       Linker_Option_Lines.Release;
+      Linker_Option_Lines.Locked := True;
       Load_Stack.Release;
+      Load_Stack.Locked := True;
       Units.Release;
+      Units.Locked := True;
    end Lock;
 
    ---------------

gcc/ada/namet.adb

@@ -1088,10 +1088,10 @@ package body Namet is
    begin
       Name_Chars.Set_Last (Name_Chars.Last + Name_Chars_Reserve);
       Name_Entries.Set_Last (Name_Entries.Last + Name_Entries_Reserve);
-      Name_Chars.Locked := True;
-      Name_Entries.Locked := True;
       Name_Chars.Release;
+      Name_Chars.Locked := True;
       Name_Entries.Release;
+      Name_Entries.Locked := True;
    end Lock;
 
    ----------------
@@ -1708,11 +1708,11 @@ package body Namet is
 
    procedure Unlock is
    begin
-      Name_Chars.Set_Last (Name_Chars.Last - Name_Chars_Reserve);
-      Name_Entries.Set_Last (Name_Entries.Last - Name_Entries_Reserve);
       Name_Chars.Locked := False;
-      Name_Entries.Locked := False;
+      Name_Chars.Set_Last (Name_Chars.Last - Name_Chars_Reserve);
       Name_Chars.Release;
+      Name_Entries.Locked := False;
+      Name_Entries.Set_Last (Name_Entries.Last - Name_Entries_Reserve);
       Name_Entries.Release;
    end Unlock;
 

gcc/ada/nlists.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -721,14 +721,12 @@ package body Nlists is
 
    procedure Lock is
    begin
-      Lists.Locked := True;
       Lists.Release;
-
-      Prev_Node.Locked := True;
-      Next_Node.Locked := True;
-
+      Lists.Locked := True;
       Prev_Node.Release;
+      Prev_Node.Locked := True;
       Next_Node.Release;
+      Next_Node.Locked := True;
    end Lock;
 
    ----------------

gcc/ada/sem.adb

@@ -1227,8 +1227,8 @@ package body Sem is
 
    procedure Lock is
    begin
-      Scope_Stack.Locked := True;
       Scope_Stack.Release;
+      Scope_Stack.Locked := True;
    end Lock;
 
    ----------------

gcc/ada/sinput.adb

@@ -678,8 +678,8 @@ package body Sinput is
 
    procedure Lock is
    begin
-      Source_File.Locked := True;
       Source_File.Release;
+      Source_File.Locked := True;
    end Lock;
 
    ----------------------

gcc/ada/stringt.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -128,10 +128,10 @@ package body Stringt is
 
    procedure Lock is
    begin
-      String_Chars.Locked := True;
-      Strings.Locked := True;
       String_Chars.Release;
+      String_Chars.Locked := True;
       Strings.Release;
+      Strings.Locked := True;
    end Lock;
 
    ----------

gcc/ada/table.ads

@@ -78,14 +78,6 @@ package Table is
       Table : Table_Ptr renames Tab.Table;
 
       Locked : Boolean renames Tab.Locked;
-      --  Table expansion is permitted only if this switch is set to False. A
-      --  client may set Locked to True, in which case any attempt to expand
-      --  the table will cause an assertion failure. Note that while a table
-      --  is locked, its address in memory remains fixed and unchanging. This
-      --  feature is used to control table expansion during Gigi processing.
-      --  Gigi assumes that tables other than the Uint and Ureal tables do
-      --  not move during processing, which means that they cannot be expanded.
-      --  The Locked flag is used to enforce this restriction.
 
       function Is_Empty return Boolean renames Tab.Is_Empty;