[multiple changes]

2011-08-29  Yannick Moy  <moy@adacore.com>

	* sem_prag.adb (Check_Precondition_Postcondition): In formal
	verification mode, analyze pragma expression for correctness, for
	pre/post on library-level subprogram, as it is not expanded later.

2011-08-29  Yannick Moy  <moy@adacore.com>

	* exp_aggr.adb (Expand_Array_Aggregate): Do not expand array aggregates
	in formal verification.

2011-08-29  Thomas Quinot  <quinot@adacore.com>

	* sem_util.adb: Minor reformatting.
	* freeze.adb, sem_ch13.adb: Fix comment: Bit_Order is an attribute,
	there's no pragma.
	* par_sco.ads, par_sco.adb: Update comments.

2011-08-29  Yannick Moy  <moy@adacore.com>

	* einfo.adb, einfo.ads: Remove flag Is_Postcondition_Proc and
	associated getter/setter.
	* sem_ch6.adb: Remove reference to Is_Postcondition_Proc.

2011-08-29  Vincent Celier  <celier@adacore.com>

	* prj-attr.adb: New Compiler attribute Dependency_Kind and Language_Kind
	* prj-conf.adb: Add_Default_GNAT_Naming_Scheme: Add a package Compiler
	with declarations for Language_Kind and Dependency_Kind for Ada.
	* prj-nmsc.adb (Check_Unit_Name): New name of procedure Check_Ada_Name
	(Process_Compiler): Take into account the new attributes Dependency_Kind
	and Language_Kind.
	(Check_Configuration): Check if language kind is unit based, not if the
	language name is Ada.
	(Process_Exceptions_Unit_Based): Ditto
	(Add_Language): Remove default additions of language and dependency kind
	* prj.ads: Minor comment change
	* snames.ads-tmpl: New standard names Dependency_Kind and Language_Kind

2011-08-29  Johannes Kanig  <kanig@adacore.com>

	* debug.adb: Update comments.

From-SVN: r178156

17 files changed, 165 insertions, 81 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3554868..6261f1a 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,46 @@
+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* sem_prag.adb (Check_Precondition_Postcondition): In formal
+	verification mode, analyze pragma expression for correctness, for
+	pre/post on library-level subprogram, as it is not expanded later.
+
+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* exp_aggr.adb (Expand_Array_Aggregate): Do not expand array aggregates
+	in formal verification.
+
+2011-08-29  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_util.adb: Minor reformatting.
+	* freeze.adb, sem_ch13.adb: Fix comment: Bit_Order is an attribute,
+	there's no pragma.
+	* par_sco.ads, par_sco.adb: Update comments.
+
+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* einfo.adb, einfo.ads: Remove flag Is_Postcondition_Proc and
+	associated getter/setter.
+	* sem_ch6.adb: Remove reference to Is_Postcondition_Proc.
+
+2011-08-29  Vincent Celier  <celier@adacore.com>
+
+	* prj-attr.adb: New Compiler attribute Dependency_Kind and Language_Kind
+	* prj-conf.adb: Add_Default_GNAT_Naming_Scheme: Add a package Compiler
+	with declarations for Language_Kind and Dependency_Kind for Ada.
+	* prj-nmsc.adb (Check_Unit_Name): New name of procedure Check_Ada_Name
+	(Process_Compiler): Take into account the new attributes Dependency_Kind
+	and Language_Kind.
+	(Check_Configuration): Check if language kind is unit based, not if the
+	language name is Ada.
+	(Process_Exceptions_Unit_Based): Ditto
+	(Add_Language): Remove default additions of language and dependency kind
+	* prj.ads: Minor comment change
+	* snames.ads-tmpl: New standard names Dependency_Kind and Language_Kind
+
+2011-08-29  Johannes Kanig  <kanig@adacore.com>
+
+	* debug.adb: Update comments.
+
 2011-08-24  Joseph Myers  <joseph@codesourcery.com>
 
 	* gcc-interface/Make-lang.in (CFLAGS-ada/tracebak.o)
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index af6200d..da34d8a 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -125,7 +125,7 @@ package body Debug is
    --  d.E
    --  d.F  ALFA mode
    --  d.G  Precondition only mode for gnat2why
-   --  d.H
+   --  d.H  Standard package only mode for gnat2why
    --  d.I  SCIL generation mode
    --  d.J  Disable parallel SCIL generation mode
    --  d.K
@@ -588,6 +588,10 @@ package body Debug is
    --       only generate Why code that checks for the well-guardedness of
    --       preconditions.
 
+   --  d.H  Standard package only mode for gnat2why. In this mode, gnat2why
+   --       will only generate Why code for package Standard. Any given input
+   --       file will be ignored.
+
    --  d.I  Generate SCIL mode. Generate intermediate code for the sake of
    --       of static analysis tools, and ensure additional tree consistency
    --       between different compilations of specs.
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index db0fcb1..ffe4349 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -519,10 +519,10 @@ package body Einfo is
    --    Is_Safe_To_Reevaluate           Flag249
    --    Has_Predicates                  Flag250
 
-   --    (Has_Implicit_Dereference)      Flag251
+   --    Has_Implicit_Dereference        Flag251
    --    Is_Processed_Transient          Flag252
-   --    Is_Postcondition_Proc           Flag253
 
+   --    (unused)                        Flag253
    --    (unused)                        Flag254
 
    -----------------------
@@ -1987,12 +1987,6 @@ package body Einfo is
       return Flag138 (Id);
    end Is_Packed_Array_Type;
 
-   function Is_Postcondition_Proc (Id : E) return B is
-   begin
-      pragma Assert (Ekind (Id) = E_Procedure);
-      return Flag253 (Id);
-   end Is_Postcondition_Proc;
-
    function Is_Potentially_Use_Visible (Id : E) return B is
    begin
       pragma Assert (Nkind (Id) in N_Entity);
@@ -4511,12 +4505,6 @@ package body Einfo is
       Set_Flag138 (Id, V);
    end Set_Is_Packed_Array_Type;
 
-   procedure Set_Is_Postcondition_Proc (Id : E; V : B := True) is
-   begin
-      pragma Assert (Ekind (Id) = E_Procedure);
-      Set_Flag253 (Id, V);
-   end Set_Is_Postcondition_Proc;
-
    procedure Set_Is_Potentially_Use_Visible (Id : E; V : B := True) is
    begin
       pragma Assert (Nkind (Id) in N_Entity);
@@ -7558,7 +7546,6 @@ package body Einfo is
       W ("Is_Package_Body_Entity",          Flag160 (Id));
       W ("Is_Packed",                       Flag51  (Id));
       W ("Is_Packed_Array_Type",            Flag138 (Id));
-      W ("Is_Postcondition_Proc",           Flag253 (Id));
       W ("Is_Potentially_Use_Visible",      Flag9   (Id));
       W ("Is_Preelaborated",                Flag59  (Id));
       W ("Is_Primitive",                    Flag218 (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 35fce3a..b1b1b90 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -2566,10 +2566,6 @@ package Einfo is
 --       an entity, then the Original_Array_Type field of this entity points
 --       to the original array type for which this is the packed array type.
 
---    Is_Postcondition_Proc (Flag253)
---       Present in procedures. Set if entity is a procedure generated by the
---       compiler for a postcondition.
-
 --    Is_Potentially_Use_Visible (Flag9)
 --       Present in all entities. Set if entity is potentially use visible,
 --       i.e. it is defined in a package that appears in a currently active
@@ -5522,7 +5518,6 @@ package Einfo is
    --    Is_Intrinsic_Subprogram             (Flag64)
    --    Is_Machine_Code_Subprogram          (Flag137)  (non-generic case only)
    --    Is_Null_Init_Proc                   (Flag178)
-   --    Is_Postcondition_Proc               (Flag253)  (non-generic case only)
    --    Is_Primitive                        (Flag218)
    --    Is_Primitive_Wrapper                (Flag195)  (non-generic case only)
    --    Is_Private_Descendant               (Flag53)
@@ -6218,7 +6213,6 @@ package Einfo is
    function Is_Package_Body_Entity              (Id : E) return B;
    function Is_Packed                           (Id : E) return B;
    function Is_Packed_Array_Type                (Id : E) return B;
-   function Is_Postcondition_Proc               (Id : E) return B;
    function Is_Potentially_Use_Visible          (Id : E) return B;
    function Is_Preelaborated                    (Id : E) return B;
    function Is_Primitive                        (Id : E) return B;
@@ -6812,7 +6806,6 @@ package Einfo is
    procedure Set_Is_Package_Body_Entity          (Id : E; V : B := True);
    procedure Set_Is_Packed                       (Id : E; V : B := True);
    procedure Set_Is_Packed_Array_Type            (Id : E; V : B := True);
-   procedure Set_Is_Postcondition_Proc           (Id : E; V : B := True);
    procedure Set_Is_Potentially_Use_Visible      (Id : E; V : B := True);
    procedure Set_Is_Preelaborated                (Id : E; V : B := True);
    procedure Set_Is_Primitive                    (Id : E; V : B := True);
@@ -7541,7 +7534,6 @@ package Einfo is
    pragma Inline (Is_Overloadable);
    pragma Inline (Is_Packed);
    pragma Inline (Is_Packed_Array_Type);
-   pragma Inline (Is_Postcondition_Proc);
    pragma Inline (Is_Potentially_Use_Visible);
    pragma Inline (Is_Preelaborated);
    pragma Inline (Is_Primitive);
@@ -7953,7 +7945,6 @@ package Einfo is
    pragma Inline (Set_Is_Package_Body_Entity);
    pragma Inline (Set_Is_Packed);
    pragma Inline (Set_Is_Packed_Array_Type);
-   pragma Inline (Set_Is_Postcondition_Proc);
    pragma Inline (Set_Is_Potentially_Use_Visible);
    pragma Inline (Set_Is_Preelaborated);
    pragma Inline (Set_Is_Primitive);
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index d6b53d4..2240b2f 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -4664,6 +4664,12 @@ package body Exp_Aggr is
          Check_Same_Aggr_Bounds (N, 1);
       end if;
 
+      --  In formal verification mode, leave the aggregate non-expanded
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  STEP 2
 
       --  Here we test for is packed array aggregate that we can handle at
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 9bd0e9c..099f9eb 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -2029,7 +2029,8 @@ package body Freeze is
             Next_Entity (Comp);
          end loop;
 
-         --  Deal with pragma Bit_Order setting non-standard bit order
+         --  Deal with Bit_Order attribute definition specifying a non-default
+         --  bit order.
 
          if Reverse_Bit_Order (Rec) and then Base_Type (Rec) = Rec then
             if not Placed_Component then
diff --git a/gcc/ada/par_sco.adb b/gcc/ada/par_sco.adb
index 5a8a695..d3e6046 100644
--- a/gcc/ada/par_sco.adb
+++ b/gcc/ada/par_sco.adb
@@ -1082,7 +1082,7 @@ package body Par_SCO is
                Pragma_Sloc : Source_Ptr := No_Location;
             begin
                --  For the case of a statement SCO for a pragma controlled by
-               --  Set_SCO_Pragma_Enable, set Pragma_Sloc so that the SCO (and
+               --  Set_SCO_Pragma_Enabled, set Pragma_Sloc so that the SCO (and
                --  those of any nested decision) is emitted only if the pragma
                --  is enabled.
 
diff --git a/gcc/ada/par_sco.ads b/gcc/ada/par_sco.ads
index 5bcad0c..450d769 100644
--- a/gcc/ada/par_sco.ads
+++ b/gcc/ada/par_sco.ads
@@ -50,9 +50,9 @@ package Par_SCO is
    --  original tree associated with Cond.
 
    procedure Set_SCO_Pragma_Enabled (Loc : Source_Ptr);
-   --  This procedure is called from Sem_Prag when a pragma is disabled (i.e.
-   --  when the Pragma_Enabled flag is unset). Loc is the Sloc of the N_Pragma
-   --  node. This is used to disable the corresponding SCO table entry. Note
+   --  This procedure is called from Sem_Prag when a pragma is enabled (i.e.
+   --  when the Pragma_Enabled flag is set). Loc is the Sloc of the N_Pragma
+   --  node. This is used to enable the corresponding statement SCO entry. Note
    --  that we use the Sloc as the key here, since in the generic case, the
    --  analysis is on a copy of the node, which is different from the node
    --  seen by Par_SCO in the parse tree (but the Sloc values are the same).
diff --git a/gcc/ada/prj-attr.adb b/gcc/ada/prj-attr.adb
index d584f6c..0f8608b 100644
--- a/gcc/ada/prj-attr.adb
+++ b/gcc/ada/prj-attr.adb
@@ -183,6 +183,8 @@ package body Prj.Attr is
    --  Configuration - Compiling
 
    "Sadriver#" &
+   "Salanguage_kind#" &
+   "Sadependency_kind#" &
    "Larequired_switches#" &
    "Laleading_required_switches#" &
    "Latrailing_required_switches#" &
diff --git a/gcc/ada/prj-conf.adb b/gcc/ada/prj-conf.adb
index db8312a..a1d9fe9 100644
--- a/gcc/ada/prj-conf.adb
+++ b/gcc/ada/prj-conf.adb
@@ -382,8 +382,9 @@ package body Prj.Conf is
 
       --  Local variables
 
-      Name   : Name_Id;
-      Naming : Project_Node_Id;
+      Name     : Name_Id;
+      Naming   : Project_Node_Id;
+      Compiler : Project_Node_Id;
 
    --  Start of processing for Add_Default_GNAT_Naming_Scheme
 
@@ -433,6 +434,12 @@ package body Prj.Conf is
 
          Create_Attribute (Name_Default_Language, "ada");
 
+         Compiler := Create_Package (Project_Tree, Config_File, "compiler");
+         Create_Attribute
+           (Name_Language_Kind, "unit_based", "ada", Pkg => Compiler);
+         Create_Attribute
+           (Name_Dependency_Kind, "ALI_File", "ada", Pkg => Compiler);
+
          Naming := Create_Package (Project_Tree, Config_File, "naming");
          Create_Attribute (Name_Spec_Suffix, ".ads", "ada",     Pkg => Naming);
          Create_Attribute (Name_Separate_Suffix, ".adb", "ada", Pkg => Naming);
diff --git a/gcc/ada/prj-nmsc.adb b/gcc/ada/prj-nmsc.adb
index 52cbdac..7f36ded 100644
--- a/gcc/ada/prj-nmsc.adb
+++ b/gcc/ada/prj-nmsc.adb
@@ -281,8 +281,8 @@ package body Prj.Nmsc is
    --  Copy Str into Name_Buffer, replacing Pattern with Replacement. Str is
    --  converted to lower-case at the same time.
 
-   procedure Check_Ada_Name (Name : String; Unit : out Name_Id);
-   --  Check that a name is a valid Ada unit name
+   procedure Check_Unit_Name (Name : String; Unit : out Name_Id);
+   --  Check that a name is a valid unit name
 
    procedure Check_Package_Naming
      (Project : Project_Id;
@@ -1112,11 +1112,11 @@ package body Prj.Nmsc is
       Debug_Decrease_Indent ("done check");
    end Check;
 
-   --------------------
-   -- Check_Ada_Name --
-   --------------------
+   ---------------------
+   -- Check_Unit_Name --
+   ---------------------
 
-   procedure Check_Ada_Name (Name : String; Unit : out Name_Id) is
+   procedure Check_Unit_Name (Name : String; Unit : out Name_Id) is
       The_Name        : String := Name;
       Real_Name       : Name_Id;
       Need_Letter     : Boolean := True;
@@ -1164,7 +1164,7 @@ package body Prj.Nmsc is
          end if;
       end Is_Reserved;
 
-   --  Start of processing for Check_Ada_Name
+   --  Start of processing for Check_Unit_Name
 
    begin
       To_Lower (The_Name);
@@ -1293,7 +1293,7 @@ package body Prj.Nmsc is
 
          Unit := No_Name;
       end if;
-   end Check_Ada_Name;
+   end Check_Unit_Name;
 
    -------------------------
    -- Check_Configuration --
@@ -1492,6 +1492,26 @@ package body Prj.Nmsc is
 
                      if Lang_Index /= No_Language_Index then
                         case Current_Array.Name is
+                        when Name_Dependency_Kind =>
+
+                           --  Attribute Dependency_Kind (<language>)
+
+                           Get_Name_String (Element.Value.Value);
+
+                           begin
+                              Lang_Index.Config.Dependency_Kind :=
+                                Dependency_File_Kind'Value
+                                  (Name_Buffer (1 .. Name_Len));
+
+                           exception
+                              when Constraint_Error =>
+                                 Error_Msg
+                                   (Data.Flags,
+                                    "illegal value for Dependency_Kind",
+                                    Element.Value.Location,
+                                    Project);
+                           end;
+
                         when Name_Dependency_Switches =>
 
                            --  Attribute Dependency_Switches (<language>)
@@ -1526,6 +1546,25 @@ package body Prj.Nmsc is
                                    In_Tree   => Data.Tree);
                            end if;
 
+                        when Name_Language_Kind =>
+                           --  Attribute Language_Kind (<language>)
+
+                           Get_Name_String (Element.Value.Value);
+
+                           begin
+                              Lang_Index.Config.Kind :=
+                                Language_Kind'Value
+                                  (Name_Buffer (1 .. Name_Len));
+
+                           exception
+                              when Constraint_Error =>
+                                 Error_Msg
+                                   (Data.Flags,
+                                    "illegal value for Language_Kind",
+                                    Element.Value.Location,
+                                    Project);
+                           end;
+
                         when Name_Include_Switches =>
 
                            --  Attribute Include_Switches (<language>)
@@ -1554,7 +1593,7 @@ package body Prj.Nmsc is
                            --  Attribute Include_Path_File (<language>)
 
                            Lang_Index.Config.Include_Path_File :=
-                               Element.Value.Value;
+                             Element.Value.Value;
 
                         when Name_Driver =>
 
@@ -1566,15 +1605,15 @@ package body Prj.Nmsc is
                         when Name_Required_Switches |
                              Name_Leading_Required_Switches =>
                            Put (Into_List =>
-                                  Lang_Index.Config.
-                                    Compiler_Leading_Required_Switches,
+                                Lang_Index.Config.
+                                  Compiler_Leading_Required_Switches,
                                 From_List => Element.Value.Values,
                                 In_Tree   => Data.Tree);
 
                         when Name_Trailing_Required_Switches =>
                            Put (Into_List =>
-                                  Lang_Index.Config.
-                                    Compiler_Trailing_Required_Switches,
+                                Lang_Index.Config.
+                                  Compiler_Trailing_Required_Switches,
                                 From_List => Element.Value.Values,
                                 In_Tree   => Data.Tree);
 
@@ -2575,7 +2614,7 @@ package body Prj.Nmsc is
 
       Lang_Index := Project.Languages;
       while Lang_Index /= No_Language_Index loop
-         if Lang_Index.Name = Name_Ada then
+         if Lang_Index.Config.Kind = Unit_Based then
             Lang_Index.Config.Naming_Data.Casing := Casing;
             Lang_Index.Config.Naming_Data.Dot_Replacement := Dot_Replacement;
 
@@ -2627,7 +2666,7 @@ package body Prj.Nmsc is
                Prev_Index.Next := Lang_Index.Next;
             end if;
 
-         elsif Lang_Index.Name = Name_Ada then
+         elsif Lang_Index.Config.Kind = Unit_Based then
             Prev_Index := Lang_Index;
 
             --  For unit based languages, Dot_Replacement, Spec_Suffix and
@@ -2636,21 +2675,24 @@ package body Prj.Nmsc is
             if Lang_Index.Config.Naming_Data.Dot_Replacement = No_File then
                Error_Msg
                  (Data.Flags,
-                  "Dot_Replacement not specified for Ada",
+                  "Dot_Replacement not specified for " &
+                  Get_Name_String (Lang_Index.Name),
                   No_Location, Project);
             end if;
 
             if Lang_Index.Config.Naming_Data.Spec_Suffix = No_File then
                Error_Msg
                  (Data.Flags,
-                  "Spec_Suffix not specified for Ada",
+                  "Spec_Suffix not specified for " &
+                  Get_Name_String (Lang_Index.Name),
                   No_Location, Project);
             end if;
 
             if Lang_Index.Config.Naming_Data.Body_Suffix = No_File then
                Error_Msg
                  (Data.Flags,
-                  "Body_Suffix not specified for Ada",
+                  "Body_Suffix not specified for " &
+                  Get_Name_String (Lang_Index.Name),
                   No_Location, Project);
             end if;
 
@@ -3189,7 +3231,6 @@ package body Prj.Nmsc is
         (Lang_Id : Language_Ptr;
          Kind    : Source_Kind)
       is
-         Lang       : constant Name_Id := Lang_Id.Name;
          Exceptions : Array_Element_Id;
          Element    : Array_Element;
          Unit       : Name_Id;
@@ -3236,22 +3277,19 @@ package body Prj.Nmsc is
 
             Get_Name_String (Element.Index);
             To_Lower (Name_Buffer (1 .. Name_Len));
-            Unit  := Name_Find;
             Index := Element.Value.Index;
 
-            --  For Ada, check if it is a valid unit name
+            --  Check if it is a valid unit name
 
-            if Lang = Name_Ada then
-               Get_Name_String (Element.Index);
-               Check_Ada_Name (Name_Buffer (1 .. Name_Len), Unit);
+            Get_Name_String (Element.Index);
+            Check_Unit_Name (Name_Buffer (1 .. Name_Len), Unit);
 
-               if Unit = No_Name then
-                  Err_Vars.Error_Msg_Name_1 := Element.Index;
-                  Error_Msg
-                    (Data.Flags,
-                     "%% is not a valid unit name.",
-                     Element.Value.Location, Project);
-               end if;
+            if Unit = No_Name then
+               Err_Vars.Error_Msg_Name_1 := Element.Index;
+               Error_Msg
+                 (Data.Flags,
+                  "%% is not a valid unit name.",
+                  Element.Value.Location, Project);
             end if;
 
             if Unit /= No_Name then
@@ -4344,13 +4382,6 @@ package body Prj.Nmsc is
          Project.Languages := Lang;
          Lang.Name         := Name;
          Lang.Display_Name := Display_Name;
-
-         if Name = Name_Ada then
-            Lang.Config.Kind            := Unit_Based;
-            Lang.Config.Dependency_Kind := ALI_File;
-         else
-            Lang.Config.Kind := File_Based;
-         end if;
       end Add_Language;
 
    --  Start of processing for Check_Programming_Languages
@@ -5690,7 +5721,7 @@ package body Prj.Nmsc is
       --  Name_Buffer contains the name of the unit in lower-cases. Check
       --  that this is a valid unit name
 
-      Check_Ada_Name (Name_Buffer (1 .. Name_Len), Unit);
+      Check_Unit_Name (Name_Buffer (1 .. Name_Len), Unit);
 
       --  If there is a naming exception for the same unit, the file is not
       --  a source for the unit.
diff --git a/gcc/ada/prj.ads b/gcc/ada/prj.ads
index 7102757..b075235 100644
--- a/gcc/ada/prj.ads
+++ b/gcc/ada/prj.ads
@@ -410,8 +410,8 @@ package Prj is
 
    type Language_Config is record
       Kind : Language_Kind := File_Based;
-      --  Kind of language. All languages are file based, except Ada which is
-      --  unit based.
+      --  Kind of language. Most languages are file based. A few, such as Ada,
+      --  are unit based.
 
       Naming_Data : Lang_Naming_Data;
       --  The naming data for the languages (prefixes, etc.)
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index f2075d0..3fa3a73 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -235,8 +235,8 @@ package body Sem_Ch13 is
       --  Processing depends on version of Ada
 
       --  For Ada 95, we just renumber bits within a storage unit. We do the
-      --  same for Ada 83 mode, since we recognize pragma Bit_Order in Ada 83,
-      --  and are free to add this extension.
+      --  same for Ada 83 mode, since we recognize attribute Bit_Order in
+      --  Ada 83, and are free to add this extension.
 
       if Ada_Version < Ada_2005 then
          Comp := First_Component_Or_Discriminant (R);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 5f7b1a7..55566fb 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -9557,7 +9557,6 @@ package body Sem_Ch6 is
                     Statements => Plist)));
 
             Set_Ekind (Post_Proc, E_Procedure);
-            Set_Is_Postcondition_Proc (Post_Proc);
 
             --  If this is a procedure, set the Postcondition_Proc attribute on
             --  the proper defining entity for the subprogram.
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 419f6cf..f866cea 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -1884,6 +1884,15 @@ package body Sem_Prag is
          --  See if it is in the pragmas after a library level subprogram
 
          elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then
+
+            --  In formal verification mode, analyze pragma expression for
+            --  correctness, as it is not expanded later.
+
+            if ALFA_Mode then
+               Analyze_PPC_In_Decl_Part
+                 (N, Defining_Entity (Unit (Parent (Parent (N)))));
+            end if;
+
             Chain_PPC (Unit (Parent (Parent (N))));
             return;
          end if;
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index f97dbb4..6aaa3dc 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -1360,7 +1360,7 @@ package body Sem_Util is
          return;
       end if;
 
-      --  Ada 2012 AI04-0144-2: Dangerous order dependence. Actuals in nested
+      --  Ada 2012 AI05-0144-2: Dangerous order dependence. Actuals in nested
       --  calls within a construct have been collected. If one of them is
       --  writable and overlaps with another one, evaluation of the enclosing
       --  construct is nondeterministic. This is illegal in Ada 2012, but is
@@ -11677,10 +11677,10 @@ package body Sem_Util is
    -- Set_Current_Entity --
    ------------------------
 
-   --  The given entity is to be set as the currently visible definition
-   --  of its associated name (i.e. the Node_Id associated with its name).
-   --  All we have to do is to get the name from the identifier, and
-   --  then set the associated Node_Id to point to the given entity.
+   --  The given entity is to be set as the currently visible definition of its
+   --  associated name (i.e. the Node_Id associated with its name). All we have
+   --  to do is to get the name from the identifier, and then set the
+   --  associated Node_Id to point to the given entity.
 
    procedure Set_Current_Entity (E : Entity_Id) is
    begin
@@ -12378,6 +12378,8 @@ package body Sem_Util is
          end if;
       end Get_Scoped_Name;
 
+   --  Start of processing for Unique_Name
+
    begin
       if E = Standard_Standard then
          return Get_Name_String (Name_Standard);
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 252dbda..69e53db 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -1093,6 +1093,7 @@ package Snames is
    Name_Default_Language                 : constant Name_Id := N + $;
    Name_Default_Switches                 : constant Name_Id := N + $;
    Name_Dependency_Driver                : constant Name_Id := N + $;
+   Name_Dependency_Kind                  : constant Name_Id := N + $;
    Name_Dependency_Switches              : constant Name_Id := N + $;
    Name_Driver                           : constant Name_Id := N + $;
    Name_Excluded_Source_Dirs             : constant Name_Id := N + $;
@@ -1121,6 +1122,7 @@ package Snames is
    Name_Include_Path_File                : constant Name_Id := N + $;
    Name_Inherit_Source_Path              : constant Name_Id := N + $;
    Name_Languages                        : constant Name_Id := N + $;
+   Name_Language_Kind                    : constant Name_Id := N + $;
    Name_Leading_Library_Options          : constant Name_Id := N + $;
    Name_Leading_Required_Switches        : constant Name_Id := N + $;
    Name_Leading_Switches                 : constant Name_Id := N + $;