[multiple changes]

2015-10-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch12.adb (Analyze_Package_Instantiation):
	Treat a missing SPARK_Mode annotation as having mode "Off".
	(Analyze_Subprogram_Instantiation): Treat a missing SPARK_Mode
	annotation as having mode "Off".
	(Instantiate_Package_Body): Code
	reformatting. Treat a missing SPARK_Mode annotation as having mode
	"Off".
	(Instantiate_Subprogram_Body): Code reformatting. Treat
	a missing SPARK_Mode annotation as having mode "Off".

2015-10-16  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch5.adb: Code clean up.
	* sem_ch13.adb: Minor fix in comment.

2015-10-16  Bob Duff  <duff@adacore.com>

	* a-exexda.adb: Change format of Exception_Information to be
	more like what we print for unhandled exceptions.
	* a-exstat.adb: Parse new format.
	* a-except-2005.adb, a-except.adb: Document new format.

From-SVN: r228907

8 files changed, 173 insertions, 112 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index d8f2b58..751cbf7 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,27 @@
+2015-10-16  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_ch12.adb (Analyze_Package_Instantiation):
+	Treat a missing SPARK_Mode annotation as having mode "Off".
+	(Analyze_Subprogram_Instantiation): Treat a missing SPARK_Mode
+	annotation as having mode "Off".
+	(Instantiate_Package_Body): Code
+	reformatting. Treat a missing SPARK_Mode annotation as having mode
+	"Off".
+	(Instantiate_Subprogram_Body): Code reformatting. Treat
+	a missing SPARK_Mode annotation as having mode "Off".
+
+2015-10-16  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch5.adb: Code clean up.
+	* sem_ch13.adb: Minor fix in comment.
+
+2015-10-16  Bob Duff  <duff@adacore.com>
+
+	* a-exexda.adb: Change format of Exception_Information to be
+	more like what we print for unhandled exceptions.
+	* a-exstat.adb: Parse new format.
+	* a-except-2005.adb, a-except.adb: Document new format.
+
 2015-10-16  Javier Miranda  <miranda@adacore.com>
 
 	* sem_ch5.adb (Analyze_Iterator_Specification): Associate a
diff --git a/gcc/ada/a-except-2005.adb b/gcc/ada/a-except-2005.adb
index 10f06bf..e792917 100644
--- a/gcc/ada/a-except-2005.adb
+++ b/gcc/ada/a-except-2005.adb
@@ -152,8 +152,8 @@ package body Ada.Exceptions is
       --
       --  The format of the string is as follows:
       --
-      --    Exception_Name: <exception name> (as in Exception_Name)
-      --    Message: <message> (only if Exception_Message is empty)
+      --    raised <exception name> : <message>
+      --    (" : <message>" is present only if Exception_Message is not empty)
       --    PID=nnnn (only if nonzero)
       --    Call stack traceback locations:  (only if at least one location)
       --    <0xyyyyyyyy 0xyyyyyyyy ...>      (is recorded)
diff --git a/gcc/ada/a-except.adb b/gcc/ada/a-except.adb
index 6760982..a228a83 100644
--- a/gcc/ada/a-except.adb
+++ b/gcc/ada/a-except.adb
@@ -117,8 +117,8 @@ package body Ada.Exceptions is
       --
       --  The format of the string is as follows:
       --
-      --    Exception_Name: <exception name> (as in Exception_Name)
-      --    Message: <message> (only if Exception_Message is empty)
+      --    raised <exception name> : <message>
+      --    (" : <message>" is present only if Exception_Message is not empty)
       --    PID=nnnn (only if nonzero)
       --    Call stack traceback locations:  (only if at least one location)
       --    <0xyyyyyyyy 0xyyyyyyyy ...>      (is recorded)
diff --git a/gcc/ada/a-exexda.adb b/gcc/ada/a-exexda.adb
index c3d1718..2a5ffbc 100644
--- a/gcc/ada/a-exexda.adb
+++ b/gcc/ada/a-exexda.adb
@@ -248,11 +248,11 @@ package body Exception_Data is
    -- Append_Info_Basic_Exception_Information --
    ---------------------------------------------
 
-   --  To ease the maximum length computation, we define and pull out a couple
-   --  of string constants:
+   --  To ease the maximum length computation, we define and pull out some
+   --  string constants:
 
-   BEI_Name_Header : constant String := "Exception name: ";
-   BEI_Msg_Header  : constant String := "Message: ";
+   BEI_Name_Header : constant String := "raised ";
+   BEI_Msg_Header  : constant String := " : ";
    BEI_PID_Header  : constant String := "PID: ";
 
    procedure Append_Info_Basic_Exception_Information
@@ -275,13 +275,13 @@ package body Exception_Data is
       if Name (Name'First) /= '_' then
          Append_Info_String (BEI_Name_Header, Info, Ptr);
          Append_Info_String (Name, Info, Ptr);
-         Append_Info_NL (Info, Ptr);
 
          if Exception_Message_Length (X) /= 0 then
             Append_Info_String (BEI_Msg_Header, Info, Ptr);
             Append_Info_Exception_Message  (X, Info, Ptr);
-            Append_Info_NL (Info, Ptr);
          end if;
+
+         Append_Info_NL (Info, Ptr);
       end if;
 
       --  Output PID line if nonzero
@@ -498,7 +498,7 @@ package body Exception_Data is
    is
    begin
       return
-        BEI_Name_Header'Length + Exception_Name_Length (X) + 1
+        BEI_Name_Header'Length + Exception_Name_Length (X)
         + BEI_Msg_Header'Length + Exception_Message_Length (X) + 1
         + BEI_PID_Header'Length + 15;
    end Basic_Exception_Info_Maxlength;
diff --git a/gcc/ada/a-exstat.adb b/gcc/ada/a-exstat.adb
index b1c6db3..1ff9481 100644
--- a/gcc/ada/a-exstat.adb
+++ b/gcc/ada/a-exstat.adb
@@ -142,117 +142,125 @@ package body Stream_Attributes is
    begin
       if S = "" then
          return Null_Occurrence;
+      end if;
 
-      else
-         To := S'First - 2;
-         Next_String;
+      To := S'First - 2;
+      Next_String;
 
-         if S (From .. From + 15) /= "Exception name: " then
-            Bad_EO;
-         end if;
-
-         X.Id := Exception_Id (Internal_Exception (S (From + 16 .. To)));
+      if S (From .. From + 6) /= "raised " then
+         Bad_EO;
+      end if;
 
-         Next_String;
+      declare
+         Name_Start : constant Positive := From + 7;
+      begin
+         From := Name_Start + 1;
 
-         if From <= To and then S (From) = 'M' then
-            if S (From .. From + 8) /= "Message: " then
-               Bad_EO;
-            end if;
+         while From < To and then S (From) /= ' ' loop
+            From := From + 1;
+         end loop;
 
-            X.Msg_Length := To - From - 8;
-            X.Msg (1 .. X.Msg_Length) := S (From + 9 .. To);
-            Next_String;
+         X.Id :=
+           Exception_Id (Internal_Exception (S (Name_Start .. From - 1)));
+      end;
 
-         else
-            X.Msg_Length := 0;
+      if From <= To then
+         if S (From .. From + 2) /= " : " then
+            Bad_EO;
          end if;
 
-         X.Pid := 0;
-
-         if From <= To and then S (From) = 'P' then
-            if S (From .. From + 3) /= "PID:" then
-               Bad_EO;
-            end if;
+         X.Msg_Length := To - From - 2;
+         X.Msg (1 .. X.Msg_Length) := S (From + 3 .. To);
 
-            From := From + 5; -- skip past PID: space
+      else
+         X.Msg_Length := 0;
+      end if;
 
-            while From <= To loop
-               X.Pid := X.Pid * 10 +
-                          (Character'Pos (S (From)) - Character'Pos ('0'));
-               From := From + 1;
-            end loop;
+      Next_String;
+      X.Pid := 0;
 
-            Next_String;
+      if From <= To and then S (From) = 'P' then
+         if S (From .. From + 3) /= "PID:" then
+            Bad_EO;
          end if;
 
-         X.Num_Tracebacks := 0;
-
-         if From <= To then
-            if S (From .. To) /= "Call stack traceback locations:" then
-               Bad_EO;
-            end if;
+         From := From + 5; -- skip past PID: space
 
-            Next_String;
-            loop
-               exit when From > To;
+         while From <= To loop
+            X.Pid := X.Pid * 10 +
+                       (Character'Pos (S (From)) - Character'Pos ('0'));
+            From := From + 1;
+         end loop;
 
-               declare
-                  Ch : Character;
-                  C  : Integer_Address;
-                  N  : Integer_Address;
-
-               begin
-                  if S (From) /= '0'
-                    or else S (From + 1) /= 'x'
-                  then
-                     Bad_EO;
-                  else
-                     From := From + 2;
-                  end if;
+         Next_String;
+      end if;
 
-                  C := 0;
-                  while From <= To loop
-                     Ch := S (From);
+      X.Num_Tracebacks := 0;
 
-                     if Ch in '0' .. '9' then
-                        N :=
-                          Character'Pos (S (From)) - Character'Pos ('0');
+      if From <= To then
+         if S (From .. To) /= "Call stack traceback locations:" then
+            Bad_EO;
+         end if;
 
-                     elsif Ch in 'a' .. 'f' then
-                        N :=
-                          Character'Pos (S (From)) - Character'Pos ('a') + 10;
+         Next_String;
+         loop
+            exit when From > To;
+
+            declare
+               Ch : Character;
+               C  : Integer_Address;
+               N  : Integer_Address;
+
+            begin
+               if S (From) /= '0'
+                 or else S (From + 1) /= 'x'
+               then
+                  Bad_EO;
+               else
+                  From := From + 2;
+               end if;
 
-                     elsif Ch = ' ' then
-                        From := From + 1;
-                        exit;
+               C := 0;
+               while From <= To loop
+                  Ch := S (From);
 
-                     else
-                        Bad_EO;
-                     end if;
+                  if Ch in '0' .. '9' then
+                     N :=
+                       Character'Pos (S (From)) - Character'Pos ('0');
 
-                     C := C * 16 + N;
+                  elsif Ch in 'a' .. 'f' then
+                     N :=
+                       Character'Pos (S (From)) - Character'Pos ('a') + 10;
 
+                  elsif Ch = ' ' then
                      From := From + 1;
-                  end loop;
+                     exit;
 
-                  if X.Num_Tracebacks = Max_Tracebacks then
+                  else
                      Bad_EO;
                   end if;
 
-                  X.Num_Tracebacks := X.Num_Tracebacks + 1;
-                  X.Tracebacks (X.Num_Tracebacks) :=
-                    TBE.TB_Entry_For (To_Address (C));
-               end;
-            end loop;
-         end if;
+                  C := C * 16 + N;
 
-         --  If an exception was converted to a string, it must have
-         --  already been raised, so flag it accordingly and we are done.
+                  From := From + 1;
+               end loop;
 
-         X.Exception_Raised := True;
-         return X;
+               if X.Num_Tracebacks = Max_Tracebacks then
+                  Bad_EO;
+               end if;
+
+               X.Num_Tracebacks := X.Num_Tracebacks + 1;
+               X.Tracebacks (X.Num_Tracebacks) :=
+                 TBE.TB_Entry_For (To_Address (C));
+            end;
+         end loop;
       end if;
+
+      --  If an exception was converted to a string, it must have
+      --  already been raised, so flag it accordingly and we are done.
+
+      X.Exception_Raised := True;
+      return X;
    end String_To_EO;
 
 end Stream_Attributes;
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index 29113e5..8a90b6c 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/gcc/ada/exp_ch5.adb
@@ -2956,6 +2956,10 @@ package body Exp_Ch5 is
 
          Prepend (Elmt_Ref, Stats);
 
+         --  The element is assignable in the expanded code.
+
+         Set_Assignment_OK (Name (Elmt_Ref));
+
          --  The loop is rewritten as a block, to hold the element declaration
 
          New_Loop :=
@@ -2981,7 +2985,6 @@ package body Exp_Ch5 is
 
       Analyze (Elmt_Decl);
       Set_Ekind (Defining_Identifier (Elmt_Decl), E_Loop_Parameter);
-      Set_Assignment_OK (Name (Elmt_Ref));
 
       Analyze (N);
    end Expand_Formal_Container_Element_Loop;
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 94b2a39..6bcecf4 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -3723,11 +3723,12 @@ package body Sem_Ch12 is
          goto Leave;
 
       else
-         --  If the context of the instance is subject to SPARK_Mode "off",
-         --  set the global flag which signals Analyze_Pragma to ignore all
-         --  SPARK_Mode pragmas within the instance.
+         --  If the context of the instance is subject to SPARK_Mode "off" or
+         --  the annotation is altogether missing, set the global flag which
+         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+         --  the instance.
 
-         if SPARK_Mode = Off then
+         if SPARK_Mode /= On then
             Ignore_Pragma_SPARK_Mode := True;
          end if;
 
@@ -5098,11 +5099,12 @@ package body Sem_Ch12 is
          Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
 
       else
-         --  If the context of the instance is subject to SPARK_Mode "off",
-         --  set the global flag which signals Analyze_Pragma to ignore all
-         --  SPARK_Mode pragmas within the instance.
+         --  If the context of the instance is subject to SPARK_Mode "off" or
+         --  the annotation is altogether missing, set the global flag which
+         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+         --  the instance.
 
-         if SPARK_Mode = Off then
+         if SPARK_Mode /= On then
             Ignore_Pragma_SPARK_Mode := True;
          end if;
 
@@ -10632,17 +10634,18 @@ package body Sem_Ch12 is
       Act_Spec    : constant Node_Id    := Specification (Act_Decl);
       Act_Decl_Id : constant Entity_Id  := Defining_Entity (Act_Spec);
 
+      Save_IPSM        : constant Boolean := Ignore_Pragma_SPARK_Mode;
+      Save_Style_Check : constant Boolean := Style_Check;
+
+      Act_Body      : Node_Id;
+      Act_Body_Id   : Entity_Id;
       Act_Body_Name : Node_Id;
       Gen_Body      : Node_Id;
       Gen_Body_Id   : Node_Id;
-      Act_Body      : Node_Id;
-      Act_Body_Id   : Entity_Id;
+      Par_Ent       : Entity_Id := Empty;
+      Par_Vis       : Boolean   := False;
 
       Parent_Installed : Boolean := False;
-      Save_Style_Check : constant Boolean := Style_Check;
-
-      Par_Ent : Entity_Id := Empty;
-      Par_Vis : Boolean   := False;
 
       Vis_Prims_List : Elist_Id := No_Elist;
       --  List of primitives made temporarily visible in the instantiation
@@ -10783,8 +10786,17 @@ package body Sem_Ch12 is
       if Present (Gen_Body_Id) then
          Save_Env (Gen_Unit, Act_Decl_Id);
          Style_Check := False;
-         Current_Sem_Unit := Body_Info.Current_Sem_Unit;
 
+         --  If the context of the instance is subject to SPARK_Mode "off" or
+         --  the annotation is altogether missing, set the global flag which
+         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+         --  the instance.
+
+         if SPARK_Mode /= On then
+            Ignore_Pragma_SPARK_Mode := True;
+         end if;
+
+         Current_Sem_Unit := Body_Info.Current_Sem_Unit;
          Gen_Body := Unit_Declaration_Node (Gen_Body_Id);
 
          Create_Instantiation_Source
@@ -10943,6 +10955,7 @@ package body Sem_Ch12 is
          end if;
 
          Restore_Env;
+         Ignore_Pragma_SPARK_Mode := Save_IPSM;
          Style_Check := Save_Style_Check;
 
       --  If we have no body, and the unit requires a body, then complain. This
@@ -11019,6 +11032,7 @@ package body Sem_Ch12 is
       Pack_Id     : constant Entity_Id  :=
                       Defining_Unit_Name (Parent (Act_Decl));
 
+      Saved_IPSM        : constant Boolean        := Ignore_Pragma_SPARK_Mode;
       Saved_Style_Check : constant Boolean        := Style_Check;
       Saved_Warnings    : constant Warning_Record := Save_Warnings;
 
@@ -11104,6 +11118,16 @@ package body Sem_Ch12 is
 
          Save_Env (Gen_Unit, Anon_Id);
          Style_Check := False;
+
+         --  If the context of the instance is subject to SPARK_Mode "off" or
+         --  the annotation is altogether missing, set the global flag which
+         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+         --  the instance.
+
+         if SPARK_Mode /= On then
+            Ignore_Pragma_SPARK_Mode := True;
+         end if;
+
          Current_Sem_Unit := Body_Info.Current_Sem_Unit;
          Create_Instantiation_Source
            (Inst_Node,
@@ -11203,6 +11227,7 @@ package body Sem_Ch12 is
          end if;
 
          Restore_Env;
+         Ignore_Pragma_SPARK_Mode := Saved_IPSM;
          Style_Check := Saved_Style_Check;
          Restore_Warnings (Saved_Warnings);
 
@@ -11268,9 +11293,10 @@ package body Sem_Ch12 is
                           (Make_Simple_Return_Statement (Loc, Ret_Expr))));
          end if;
 
-         Pack_Body := Make_Package_Body (Loc,
-           Defining_Unit_Name => New_Copy (Pack_Id),
-           Declarations       => New_List (Act_Body));
+         Pack_Body :=
+           Make_Package_Body (Loc,
+             Defining_Unit_Name => New_Copy (Pack_Id),
+             Declarations       => New_List (Act_Body));
 
          Insert_After (Inst_Node, Pack_Body);
          Set_Corresponding_Spec (Pack_Body, Pack_Id);
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index b820f4d..40d4d35 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -122,7 +122,7 @@ package body Sem_Ch13 is
    --  to generate appropriate semantic checks that are delayed until this
    --  point (they had to be delayed this long for cases of delayed aspects,
    --  e.g. analysis of statically predicated subtypes in choices, for which
-   --  we have to be sure the subtypes in question are frozen before checking.
+   --  we have to be sure the subtypes in question are frozen before checking).
 
    function Get_Alignment_Value (Expr : Node_Id) return Uint;
    --  Given the expression for an alignment value, returns the corresponding