2011-08-04 Eric Botcazou <ebotcazou@adacore.com>

	* bindgen.adb: Add comments.

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

	* einfo.adb, einfo.ads: Free Flag254 and make Formal_Proof_On a
	synthesized flag.
	* sem_prag.adb (Analyze_Pragma): record the pragma Annotate
	(Formal_Proof, On/Off) in the Rep_Item list of the current subprogram.

2011-08-04  Robert Dewar  <dewar@adacore.com>

	* exp_ch7.adb, exp_ch6.adb, sem_ch3.adb, layout.adb, sem_ch5.adb,
	osint-c.ads, sem_util.ads, gnat1drv.adb, targparm.ads, sem_ch6.adb,
	sem_ch13.adb, s-pooloc.adb: Minor reformatting.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177334 138bc75d-0d04-0410-961f-82ee72b054a4

17 files changed, 186 insertions, 125 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5fe886421a3..179b12e61c4 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,20 @@
+2011-08-04  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* bindgen.adb: Add comments.
+
+2011-08-04  Yannick Moy  <moy@adacore.com>
+
+	* einfo.adb, einfo.ads: Free Flag254 and make Formal_Proof_On a
+	synthesized flag.
+	* sem_prag.adb (Analyze_Pragma): record the pragma Annotate
+	(Formal_Proof, On/Off) in the Rep_Item list of the current subprogram.
+
+2011-08-04  Robert Dewar  <dewar@adacore.com>
+
+	* exp_ch7.adb, exp_ch6.adb, sem_ch3.adb, layout.adb, sem_ch5.adb,
+	osint-c.ads, sem_util.ads, gnat1drv.adb, targparm.ads, sem_ch6.adb,
+	sem_ch13.adb, s-pooloc.adb: Minor reformatting.
+
 2011-08-04  Thomas Quinot  <quinot@adacore.com>
 
 	* s-pooloc.ads, s-pooglo.ads: Minor reformatting
diff --git a/gcc/ada/bindgen.adb b/gcc/ada/bindgen.adb
index 353e91da584..a4e7ccae87e 100644
--- a/gcc/ada/bindgen.adb
+++ b/gcc/ada/bindgen.adb
@@ -3097,6 +3097,9 @@ package body Bindgen is
          WBI ("");
       end if;
 
+      --  The B.1 (39) implementation advice says that the adainit/adafinal
+      --  routines should be idempotent. Generate a flag to ensure that.
+
       WBI ("   Is_Elaborated : Boolean := False;");
       WBI ("");
 
@@ -3323,6 +3326,9 @@ package body Bindgen is
          WBI ("");
       end if;
 
+      --  The B.1 (39) implementation advice says that the adainit/adafinal
+      --  routines should be idempotent. Generate a flag to ensure that.
+
       WBI ("static char is_elaborated = 0;");
       WBI ("");
 
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index be0081684dc..84163c67c8d 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -522,7 +522,7 @@ package body Einfo is
    --    Body_Is_In_ALFA                 Flag251
    --    Is_Processed_Transient          Flag252
    --    Is_Postcondition_Proc           Flag253
-   --    Formal_Proof_On                 Flag254
+   --    (unused)                        Flag254
 
    -----------------------
    -- Local subprograms --
@@ -1126,12 +1126,6 @@ package body Einfo is
       return Node6 (Id);
    end First_Rep_Item;
 
-   function Formal_Proof_On (Id : E) return B is
-   begin
-      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
-      return Flag254 (Id);
-   end Formal_Proof_On;
-
    function Freeze_Node (Id : E) return N is
    begin
       return Node7 (Id);
@@ -3612,12 +3606,6 @@ package body Einfo is
       Set_Uint10 (Id, UI_From_Int (F'Pos (V)));
    end Set_Float_Rep;
 
-   procedure Set_Formal_Proof_On (Id : E; V : B := True) is
-   begin
-      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
-      Set_Flag254 (Id, V);
-   end Set_Formal_Proof_On;
-
    procedure Set_Freeze_Node (Id : E; V : N) is
    begin
       Set_Node7 (Id, V);
@@ -5911,6 +5899,41 @@ package body Einfo is
       end if;
    end First_Formal_With_Extras;
 
+   ---------------------
+   -- Formal_Proof_On --
+   ---------------------
+
+   function Formal_Proof_On (Id : E) return B is
+      N    : Node_Id;
+      Arg1 : Node_Id;
+      Arg2 : Node_Id;
+
+   begin
+      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+
+      N := First_Rep_Item (Id);
+      while Present (N) loop
+         if Nkind (N) = N_Pragma
+           and then Get_Pragma_Id (Pragma_Name (N)) = Pragma_Annotate
+           and then Present (Pragma_Argument_Associations (N))
+           and then List_Length (Pragma_Argument_Associations (N)) = 2
+         then
+            Arg1 := First (Pragma_Argument_Associations (N));
+            Arg2 := Next (Arg1);
+
+            if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof
+              and then Chars (Get_Pragma_Arg (Arg2)) = Name_On
+            then
+               return True;
+            end if;
+         end if;
+
+         Next_Rep_Item (N);
+      end loop;
+
+      return False;
+   end Formal_Proof_On;
+
    -------------------------------------
    -- Get_Attribute_Definition_Clause --
    -------------------------------------
@@ -7442,7 +7465,6 @@ package body Einfo is
       W ("Entry_Accepted",                  Flag152 (Id));
       W ("Can_Use_Internal_Rep",            Flag229 (Id));
       W ("Finalize_Storage_Only",           Flag158 (Id));
-      W ("Formal_Proof_On",                 Flag254 (Id));
       W ("From_With_Type",                  Flag159 (Id));
       W ("Has_Aliased_Components",          Flag135 (Id));
       W ("Has_Alignment_Clause",            Flag46  (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 84fd79d3657..49e22fb01f9 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -1272,10 +1272,10 @@ package Einfo is
 --       Float_Rep_Kind. Together with the Digits_Value uniquely defines
 --       the floating-point representation to be used.
 
---    Formal_Proof_On (Flag254)
---       Present in subprogram and generic subprogram entities. Set on for
---       subprograms whose body contains an Annotate pragma which forces formal
---       proof on this body.
+--    Formal_Proof_On (synthesized)
+--       Applies to subprogram and generic subprogram entities. Returns True if
+--       the Rep_Item chain for the subprogram has a pragma Annotate which
+--       forces formal proof on the subprogram's body.
 
 --    Freeze_Node (Node7)
 --       Present in all entities. If there is an associated freeze node for
@@ -5250,7 +5250,6 @@ package Einfo is
    --    Delay_Cleanups                      (Flag114)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Discard_Names                       (Flag88)
-   --    Formal_Proof_On                     (Flag254)
    --    Has_Completion                      (Flag26)
    --    Has_Controlling_Result              (Flag98)
    --    Has_Invariants                      (Flag232)
@@ -5397,7 +5396,6 @@ package Einfo is
    --    Is_Primitive                        (Flag218)
    --    Is_Thunk                            (Flag225)
    --    Default_Expressions_Processed       (Flag108)
-   --    Formal_Proof_On                     (Flag254)
    --    Aren't there more flags and fields? seems like this list should be
    --    more similar to the E_Function list, which is much longer ???
 
@@ -5518,7 +5516,6 @@ package Einfo is
    --    Delay_Cleanups                      (Flag114)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Discard_Names                       (Flag88)
-   --    Formal_Proof_On                     (Flag254)
    --    Has_Completion                      (Flag26)
    --    Has_Invariants                      (Flag232)
    --    Has_Master_Entity                   (Flag21)
@@ -6076,7 +6073,6 @@ package Einfo is
    function First_Private_Entity                (Id : E) return E;
    function First_Rep_Item                      (Id : E) return N;
    function Float_Rep                           (Id : E) return F;
-   function Formal_Proof_On                     (Id : E) return B;
    function Freeze_Node                         (Id : E) return N;
    function From_With_Type                      (Id : E) return B;
    function Full_View                           (Id : E) return E;
@@ -6453,6 +6449,7 @@ package Einfo is
    function First_Component_Or_Discriminant     (Id : E) return E;
    function First_Formal                        (Id : E) return E;
    function First_Formal_With_Extras            (Id : E) return E;
+   function Formal_Proof_On                     (Id : E) return B;
    function Has_Attach_Handler                  (Id : E) return B;
    function Has_Entries                         (Id : E) return B;
    function Has_Foreign_Convention              (Id : E) return B;
@@ -6666,7 +6663,6 @@ package Einfo is
    procedure Set_First_Private_Entity            (Id : E; V : E);
    procedure Set_First_Rep_Item                  (Id : E; V : N);
    procedure Set_Float_Rep                       (Id : E; V : F);
-   procedure Set_Formal_Proof_On                 (Id : E; V : B := True);
    procedure Set_Freeze_Node                     (Id : E; V : N);
    procedure Set_From_With_Type                  (Id : E; V : B := True);
    procedure Set_Full_View                       (Id : E; V : E);
@@ -7364,7 +7360,6 @@ package Einfo is
    pragma Inline (First_Optional_Parameter);
    pragma Inline (First_Private_Entity);
    pragma Inline (First_Rep_Item);
-   pragma Inline (Formal_Proof_On);
    pragma Inline (Freeze_Node);
    pragma Inline (From_With_Type);
    pragma Inline (Full_View);
@@ -7809,7 +7804,6 @@ package Einfo is
    pragma Inline (Set_First_Optional_Parameter);
    pragma Inline (Set_First_Private_Entity);
    pragma Inline (Set_First_Rep_Item);
-   pragma Inline (Set_Formal_Proof_On);
    pragma Inline (Set_Freeze_Node);
    pragma Inline (Set_From_With_Type);
    pragma Inline (Set_Full_View);
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 1d9544dd9f3..ca449fae78b 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -7188,7 +7188,7 @@ package body Exp_Ch6 is
             null;
 
          --  Do not generate the call to Make_Set_Finalize_Address_Ptr for
-         --  CodePeer compilations becase Finalize_Address is never built.
+         --  CodePeer compilations because Finalize_Address is never built.
 
          elsif not CodePeer_Mode then
             Insert_Action (Allocator,
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 21a1ffea63a..abe960b3a06 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -2817,6 +2817,10 @@ package body Exp_Ch7 is
       --  order to detect this scenario, save the state of entry into the
       --  finalization code.
 
+      --  No need to do this for VM case, since VM version of Ada.Exceptions
+      --  does not include routine Raise_From_Controlled_Operation which is the
+      --  the sole user of flag Abort.
+
       if Abort_Allowed
         and then VM_Target = No_VM
       then
@@ -2871,9 +2875,7 @@ package body Exp_Ch7 is
                         Attribute_Name => Name_Identity)));
          end;
 
-      --  No abort or .NET/JVM. The VM version of Ada.Exceptions does not
-      --  include routine Raise_From_Controlled_Operation which is the sole
-      --  user of flag Abort.
+      --  No abort or .NET/JVM
 
       else
          A_Expr := New_Reference_To (Standard_False, Loc);
@@ -7131,8 +7133,9 @@ package body Exp_Ch7 is
          Utyp := Underlying_Type (Root_Type (Base_Type (Typ)));
          Ref  := Unchecked_Convert_To (Utyp, Ref);
 
+         --  The following is to prevent problems with UC see 1.156 RH ???
+
          Set_Assignment_OK (Ref);
-         --  To prevent problems with UC see 1.156 RH ???
       end if;
 
       --  If the underlying_type is a subtype, then we are dealing with the
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index dcff866229b..eabf1123d4a 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -1048,15 +1048,17 @@ begin
       Write_ALI (Object => (Back_End_Mode = Generate_Object));
 
       if not Compilation_Errors then
+
          --  In case of ada backends, we need to make sure that the generated
-         --  object file has a timestamp greater than the ALI file.
-         --  We do this to make gnatmake happy when checking the ALI and obj
-         --  timestamps, where it expects the object file being written after
-         --  the ali file.
+         --  object file has a timestamp greater than the ALI file. We do this
+         --  to make gnatmake happy when checking the ALI and obj timestamps,
+         --  where it expects the object file being written after the ali file.
+
          --  Gnatmake's assumption is true for gcc platforms where the gcc
          --  wrapper needs to call the assembler after calling gnat1, but is
          --  not true for ada backends, where the object files are created
          --  directly by gnat1 (so are created before the ali file).
+
          Back_End.Gen_Or_Update_Object_File;
       end if;
 
diff --git a/gcc/ada/layout.adb b/gcc/ada/layout.adb
index 7ae89b53f27..09d3ce1ac8d 100644
--- a/gcc/ada/layout.adb
+++ b/gcc/ada/layout.adb
@@ -1280,8 +1280,8 @@ package body Layout is
             end;
          end if;
 
-         --  Now set the dynamic size (the Value_Size is always the same
-         --  as the Object_Size for arrays whose length is dynamic).
+         --  Now set the dynamic size (the Value_Size is always the same as the
+         --  Object_Size for arrays whose length is dynamic).
 
          --  ??? If Size.Status = Dynamic, Vtyp will not have been set.
          --  The added initialization sets it to Empty now, but is this
@@ -1305,6 +1305,7 @@ package body Layout is
       Lo   : Node_Id;
       Hi   : Node_Id;
       Res  : Boolean := False;
+
    begin
       --  Loop to process array indexes
 
@@ -1323,9 +1324,10 @@ package body Layout is
          Hi := Type_High_Bound (Ityp);
 
          if (Nkind (Lo) = N_Identifier
-               and then Ekind (Entity (Lo)) = E_Discriminant)
-           or else (Nkind (Hi) = N_Identifier
-                      and then Ekind (Entity (Hi)) = E_Discriminant)
+              and then Ekind (Entity (Lo)) = E_Discriminant)
+           or else
+            (Nkind (Hi) = N_Identifier
+              and then Ekind (Entity (Hi)) = E_Discriminant)
          then
             Res := True;
          end if;
diff --git a/gcc/ada/osint-c.ads b/gcc/ada/osint-c.ads
index e8bc57a8ad1..2faef5ed787 100644
--- a/gcc/ada/osint-c.ads
+++ b/gcc/ada/osint-c.ads
@@ -117,10 +117,10 @@ package Osint.C is
    --  above for a discussion of how library information files are stored.
 
    procedure Set_Library_Info_Name;
-   --  Sets a default ALI file name from the main compiler source name.
-   --  This is used by Create_Output_Library_Info, and by the version of
-   --  Read_Library_Info that takes a default file name. The name is in
-   --  Name_Buffer (with length in Name_Len) on return from the call.
+   --  Sets a default ALI file name from the main compiler source name. Used by
+   --  Create_Output_Library_Info, and by the version of Read_Library_Info that
+   --  takes a default file name. The name is in Name_Buffer (with length in
+   --  Name_Len) on return from the call.
 
    procedure Create_Output_Library_Info;
    --  Creates the output library information file for the source file which
diff --git a/gcc/ada/s-pooloc.adb b/gcc/ada/s-pooloc.adb
index 2a161f49de3..ebada306114 100644
--- a/gcc/ada/s-pooloc.adb
+++ b/gcc/ada/s-pooloc.adb
@@ -112,6 +112,8 @@ package body System.Pool_Local is
       if Prev (Allocated).all = Null_Address then
          Pool.First := Next (Allocated).all;
 
+         --  Comment needed
+
          if Pool.First /= Null_Address then
             Prev (Pool.First).all := Null_Address;
          end if;
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 3bb1d524996..c9f78fae525 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -440,14 +440,14 @@ package body Sem_Ch13 is
                               Error_Msg_Uint_1 := SSU;
                               Error_Msg_F
                                 ("\and is not a multiple of Storage_Unit (^) "
-                                 & "('R'M 13.4.1(10))",
+                                 & "(RM 13.4.1(10))",
                                  First_Bit (CC));
 
                            else
                               Error_Msg_Uint_1 := Fbit;
                               Error_Msg_F
                                 ("\and first bit (^) is non-zero "
-                                 & "('R'M 13.4.1(10))",
+                                 & "(RM 13.4.1(10))",
                                  First_Bit (CC));
                            end if;
                         end if;
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 401436db2b8..4cf4c0b6b10 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -15302,7 +15302,7 @@ package body Sem_Ch3 is
             elsif No (Real_Range_Specification (Def)) then
                Error_Msg_Uint_1 := Max_Digs_Val;
                Error_Msg_N ("types with more than ^ digits need range spec "
-                 & "('R'M 3.5.7(6))", Digs);
+                 & "(RM 3.5.7(6))", Digs);
             end if;
          end;
       end if;
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index b9c03c02932..8936daa531f 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2098,8 +2098,9 @@ package body Sem_Ch5 is
                --  elements of a container using the OF syntax.
 
                if Is_In_ALFA (Etype (Id))
-                 and then (No (Iterator_Specification (N))
-                           or else not Of_Present (Iterator_Specification (N)))
+                 and then
+                   (No (Iterator_Specification (N))
+                     or else not Of_Present (Iterator_Specification (N)))
                then
                   Set_Is_In_ALFA (Id);
                end if;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 4eaaaa6ab9b..64a7eac5e6e 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -6273,7 +6273,7 @@ package body Sem_Ch6 is
                         Obj_Decl, Typ);
                      Error_Msg_N
                        ("\an equality operator cannot be declared after this "
-                         & "point ('R'M 4.5.2 (9.8)) (Ada 2012))?", Obj_Decl);
+                         & "point (RM 4.5.2 (9.8)) (Ada 2012))?", Obj_Decl);
                      exit;
                   end if;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index e9923157b14..dac7df81461 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -6091,103 +6091,118 @@ package body Sem_Prag is
          --  external tool and a tool-specific function. These arguments are
          --  not analyzed.
 
-         when Pragma_Annotate => Annotate : begin
+         --  The following is a special form used in conjunction with the
+         --  ALFA subset of Ada:
+
+         --    pragma Annotate (Formal_Proof, MODE);
+         --    MODE ::= On | Off
+
+         --    This pragma either forces (mode On) or disables (mode Off)
+         --    formal verification of the subprogram in which it is added. When
+         --    formal verification is forced, all violations of the the ALFA
+         --    subset of Ada present in the subprogram are reported as errors
+         --    to the user.
+
+         when Pragma_Annotate => Annotate : declare
+            Arg : Node_Id;
+            Exp : Node_Id;
+
+         begin
             GNAT_Pragma;
             Check_At_Least_N_Arguments (1);
             Check_Arg_Is_Identifier (Arg1);
             Check_No_Identifiers;
             Store_Note (N);
 
-            declare
-               Arg : Node_Id;
-               Exp : Node_Id;
+            --  Special processing for Formal_Proof case
 
-            begin
-               if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then
-                  if No (Arg2) then
-                     Error_Pragma_Arg
-                       ("missing second argument for pragma%", Arg1);
-                  end if;
+            if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then
+               if No (Arg2) then
+                  Error_Pragma_Arg
+                    ("missing second argument for pragma%", Arg1);
+               end if;
 
-                  Check_Arg_Is_Identifier (Arg2);
-                  Check_Arg_Count (2);
+               Check_Arg_Count (2);
+               Check_Arg_Is_One_Of (Arg2, Name_On, Name_Off);
 
-                  if Chars (Get_Pragma_Arg (Arg2)) /= Name_On
-                    and then Chars (Get_Pragma_Arg (Arg2)) /= Name_Off
+               declare
+                  Cur_Subp : constant Entity_Id := Current_Subprogram;
+
+               begin
+                  if Present (Cur_Subp)
+                    and then (Is_Subprogram (Cur_Subp)
+                               or else Is_Generic_Subprogram (Cur_Subp))
                   then
-                     Error_Pragma_Arg
-                       ("wrong second argument for pragma%", Arg2);
-                  end if;
+                     --  Notify user if some ALFA violation occurred before
+                     --  this point in Cur_Subp. These violations are not
+                     --  precisly located, but this is better than ignoring
+                     --  these violations.
+
+                     if Chars (Get_Pragma_Arg (Arg2)) = Name_On
+                       and then (not Is_In_ALFA (Cur_Subp)
+                                  or else not Body_Is_In_ALFA (Cur_Subp))
+                     then
+                        Error_Pragma
+                          ("pragma% is placed after violation"
+                           & " of 'A'L'F'A");
+                     end if;
 
-                  if Chars (Get_Pragma_Arg (Arg2)) = Name_On then
-                     declare
-                        Cur_Subp : constant Entity_Id := Current_Subprogram;
+                     --  We treat this as a Rep_Item to record it on the rep
+                     --  item chain for easy location later on.
 
-                     begin
-                        if Present (Cur_Subp)
-                          and then (Is_Subprogram (Cur_Subp)
-                                     or else Is_Generic_Subprogram (Cur_Subp))
-                        then
-                           --  Notify user if some ALFA violation occurred
-                           --  before this point in Cur_Subp. These violations
-                           --  are not precisly located, but this is better
-                           --  than ignoring them.
+                     Record_Rep_Item (Cur_Subp, N);
 
-                           if not Is_In_ALFA (Cur_Subp)
-                             or else not Body_Is_In_ALFA (Cur_Subp)
-                           then
-                              Error_Pragma
-                                ("pragma% is placed after violation"
-                                 & " of 'A'L'F'A");
-                           end if;
+                  else
+                     Error_Pragma ("wrong placement for pragma%");
+                  end if;
+               end;
 
-                           Set_Formal_Proof_On (Cur_Subp);
+            --  Second parameter is optional, it is never analyzed
 
-                        else
-                           Error_Pragma ("wrong placement for pragma%");
-                        end if;
-                     end;
-                  end if;
-               end if;
+            elsif No (Arg2) then
+               null;
 
-               --  Second unanalyzed parameter is optional
+            --  Here if we have a second parameter
 
-               if No (Arg2) then
-                  null;
-               else
-                  Arg := Next (Arg2);
-                  while Present (Arg) loop
-                     Exp := Get_Pragma_Arg (Arg);
-                     Analyze (Exp);
+            else
+               --  Second parameter must be identifier
 
-                     if Is_Entity_Name (Exp) then
-                        null;
+               Check_Arg_Is_Identifier (Arg2);
 
-                     --  For string literals, we assume Standard_String as the
-                     --  type, unless the string contains wide or wide_wide
-                     --  characters.
+               --  Process remaining parameters if any
 
-                     elsif Nkind (Exp) = N_String_Literal then
-                        if Has_Wide_Wide_Character (Exp) then
-                           Resolve (Exp, Standard_Wide_Wide_String);
-                        elsif Has_Wide_Character (Exp) then
-                           Resolve (Exp, Standard_Wide_String);
-                        else
-                           Resolve (Exp, Standard_String);
-                        end if;
+               Arg := Next (Arg2);
+               while Present (Arg) loop
+                  Exp := Get_Pragma_Arg (Arg);
+                  Analyze (Exp);
 
-                     elsif Is_Overloaded (Exp) then
-                           Error_Pragma_Arg
-                             ("ambiguous argument for pragma%", Exp);
+                  if Is_Entity_Name (Exp) then
+                     null;
+
+                  --  For string literals, we assume Standard_String as the
+                  --  type, unless the string contains wide or wide_wide
+                  --  characters.
 
+                  elsif Nkind (Exp) = N_String_Literal then
+                     if Has_Wide_Wide_Character (Exp) then
+                        Resolve (Exp, Standard_Wide_Wide_String);
+                     elsif Has_Wide_Character (Exp) then
+                        Resolve (Exp, Standard_Wide_String);
                      else
-                        Resolve (Exp);
+                        Resolve (Exp, Standard_String);
                      end if;
 
-                     Next (Arg);
-                  end loop;
-               end if;
-            end;
+                  elsif Is_Overloaded (Exp) then
+                        Error_Pragma_Arg
+                          ("ambiguous argument for pragma%", Exp);
+
+                  else
+                     Resolve (Exp);
+                  end if;
+
+                  Next (Arg);
+               end loop;
+            end if;
          end Annotate;
 
          ------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index e8773a44a28..62b75670654 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -291,8 +291,7 @@ package Sem_Util is
    --  specification, and calls to the subprogram, from being in ALFA.
 
    --  If the subprogram being marked as not in ALFA is annotated with
-   --  Formal_Proof being On, then an error is issued with message Msg on node
-   --  N.
+   --  Formal_Proof On, then an error is issued with message Msg on node N.
 
    function Defining_Entity (N : Node_Id) return Entity_Id;
    --  Given a declaration N, returns the associated defining entity. If the
diff --git a/gcc/ada/targparm.ads b/gcc/ada/targparm.ads
index 7db350be24c..fa6e25ede9f 100644
--- a/gcc/ada/targparm.ads
+++ b/gcc/ada/targparm.ads
@@ -26,8 +26,6 @@
 --  This package obtains parameters from the target runtime version of System,
 --  to indicate parameters relevant to the target environment.
 
---  Is it right for this to be modified GPL???
-
 --  Conceptually, these parameters could be obtained using rtsfind, but
 --  we do not do this for four reasons: