err_vars.ads (Error_Msg_Lang, [...]): new variables for insertion character ~~

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

	* err_vars.ads (Error_Msg_Lang, Error_Msg_Langlen): new variables for
	insertion character ~~
	* errout.ads, errout.adb (Formal_Error_Msg_...): remove procedures
	(Set_Error_Msg_Lang): new procedure which fixes the language for use
	with insertion character ~~
	(Set_Msg_Text): treat insertion character ~~
	* par-ch4.adb, par-ch5.adb, par-endh.adb, sem_attr.adb, sem_ch11.adb,
	sem_ch3.adb, sem_ch5.adb, sem_ch9.adb, sem_util.adb: Replace calls to
	Formal_Error_Msg_... procedures by equivalent Error_Msg_...
	procedures. Favor calls to Error_Msg_F(E) over Error_Msg_N(E). Make
	errors related to the formal language restriction not serious
	(insertion character |).
	* par.adb (Par): set formal language for error messages if needed
	* sem_ch6.adb (Check_Missing_Return): take into account possible
	generated statements at the end of the function
	* snames.ads-tmpl (Name_SPARK_95, Pragma_SPARK_95): new variable and
	enumeration value to define a new pragma SPARK_95
	* opt.ads, opt.adb (SPARK_Version_Type, SPARK_Version_Default,
	SPARK_Version): new type and variables to store the SPARK version
	(none by default).
	(SPARK_Mode): return True when SPARK_Version is set
	* par-prag.adb: Correct indentation
	(Prag): take Pragma_SPARK_95 into account
	* sem_prag.adb (Set_Mechanism_Value, Sig_Flags): take Pragma_SPARK_95
	into account.

From-SVN: r177056

gcc/ada/ChangeLog

+2011-08-01  Yannick Moy  <moy@adacore.com>
+
+	* err_vars.ads (Error_Msg_Lang, Error_Msg_Langlen): new variables for
+	insertion character ~~
+	* errout.ads, errout.adb (Formal_Error_Msg_...): remove procedures
+	(Set_Error_Msg_Lang): new procedure which fixes the language for use
+	with insertion character ~~
+	(Set_Msg_Text): treat insertion character ~~
+	* par-ch4.adb, par-ch5.adb, par-endh.adb, sem_attr.adb, sem_ch11.adb,
+	sem_ch3.adb, sem_ch5.adb, sem_ch9.adb, sem_util.adb: Replace calls to
+	Formal_Error_Msg_... procedures by equivalent Error_Msg_...
+	procedures. Favor calls to Error_Msg_F(E) over Error_Msg_N(E). Make
+	errors related to the formal language restriction not serious
+	(insertion character |).
+	* par.adb (Par): set formal language for error messages if needed
+	* sem_ch6.adb (Check_Missing_Return): take into account possible
+	generated statements at the end of the function
+	* snames.ads-tmpl (Name_SPARK_95, Pragma_SPARK_95): new variable and
+	enumeration value to define a new pragma SPARK_95
+	* opt.ads, opt.adb (SPARK_Version_Type, SPARK_Version_Default,
+	SPARK_Version): new type and variables to store the SPARK version
+	(none by default).
+	(SPARK_Mode): return True when SPARK_Version is set
+	* par-prag.adb: Correct indentation
+	(Prag): take Pragma_SPARK_95 into account
+	* sem_prag.adb (Set_Mechanism_Value, Sig_Flags): take Pragma_SPARK_95
+	into account.
+
 2011-08-01  Robert Dewar  <dewar@adacore.com>
 
 	* sem_ch3.adb, sem_ch3.ads, sem_ch5.adb, prj-part.adb, par-ch4.adb,

gcc/ada/err_vars.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2009, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2010, 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- --
@@ -150,4 +150,9 @@ package Err_Vars is
    --  Used if current message contains a ~ insertion character to indicate
    --  insertion of the string Error_Msg_String (1 .. Error_Msg_Strlen).
 
+   Error_Msg_Lang : String (1 .. 4096);
+   Error_Msg_Langlen : Natural;
+   --  Used if current message contains a ~~ insertion character to indicate
+   --  insertion of the string Error_Msg_Lang (1 .. Error_Msg_Langlen).
+
 end Err_Vars;

gcc/ada/errout.adb

@@ -1402,49 +1402,6 @@ package body Errout is
       return S;
    end First_Sloc;
 
-   ----------------------
-   -- Formal_Error_Msg --
-   ----------------------
-
-   procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr) is
-   begin
-      pragma Assert (Formal_Verification_Mode);
-      Error_Msg ("(" & Formal_Language & ") " & Msg, Flag_Location);
-   end Formal_Error_Msg;
-
-   ------------------------
-   -- Formal_Error_Msg_N --
-   ------------------------
-
-   procedure Formal_Error_Msg_N (Msg : String; N : Node_Id) is
-   begin
-      pragma Assert (Formal_Verification_Mode);
-      Error_Msg_N ("(" & Formal_Language & ") " & Msg, N);
-   end Formal_Error_Msg_N;
-
-   -------------------------
-   -- Formal_Error_Msg_NE --
-   -------------------------
-
-   procedure Formal_Error_Msg_NE
-     (Msg : String;
-      N   : Node_Or_Entity_Id;
-      E   : Node_Or_Entity_Id) is
-   begin
-      pragma Assert (Formal_Verification_Mode);
-      Error_Msg_NE ("(" & Formal_Language & ") " & Msg, N, E);
-   end Formal_Error_Msg_NE;
-
-   -------------------------
-   -- Formal_Error_Msg_SP --
-   -------------------------
-
-   procedure Formal_Error_Msg_SP (Msg : String) is
-   begin
-      pragma Assert (Formal_Verification_Mode);
-      Error_Msg_SP ("(" & Formal_Language & ") " & Msg);
-   end Formal_Error_Msg_SP;
-
    ----------------
    -- Initialize --
    ----------------
@@ -2214,6 +2171,16 @@ package body Errout is
       Set_Casing (Desired_Case);
    end Set_Identifier_Casing;
 
+   ------------------------
+   -- Set_Error_Msg_Lang --
+   ------------------------
+
+   procedure Set_Error_Msg_Lang (To : String) is
+   begin
+      Error_Msg_Langlen := To'Length;
+      Error_Msg_Lang (1 .. Error_Msg_Langlen) := To;
+   end Set_Error_Msg_Lang;
+
    -----------------------
    -- Set_Ignore_Errors --
    -----------------------
@@ -2675,7 +2642,6 @@ package body Errout is
                if P <= Text'Last and then Text (P) = '$' then
                   P := P + 1;
                   Set_Msg_Insertion_Unit_Name (Suffix => False);
-
                else
                   Set_Msg_Insertion_Unit_Name;
                end if;
@@ -2733,7 +2699,12 @@ package body Errout is
                P := P + 1;
 
             when '~' =>
-               Set_Msg_Str (Error_Msg_String (1 .. Error_Msg_Strlen));
+               if P <= Text'Last and then Text (P) = '~' then
+                  P := P + 1;
+                  Set_Msg_Str (Error_Msg_Lang (1 .. Error_Msg_Langlen));
+               else
+                  Set_Msg_Str (Error_Msg_String (1 .. Error_Msg_Strlen));
+               end if;
 
             --  Upper case letter
 

gcc/ada/errout.ads

@@ -346,6 +346,16 @@ package Errout is
    --      inserted to replace the ~ character. The string is inserted in the
    --      literal form it appears, without any action on special characters.
 
+   --    Insertion character ~~ (Two tildes: insert language string)
+   --      Indicates that Error_Msg_Lang (1 .. Error_Msg_Langlen) is to be
+   --      inserted to replace the ~~ character. Typically the language string
+   --      will be inserted in parentheses as a prefix of the error message, as
+   --      in "(spark) error msg". The string is inserted in the literal form
+   --      it appears, without any action on special characters. Error_Msg_Lang
+   --      and Error_Msg_Langlen are expected to be set only once before
+   --      parsing starts, so that the caller to an error procedure does not
+   --      need to set them repeatedly.
+
    ----------------------------------------
    -- Specialization of Messages for VMS --
    ----------------------------------------
@@ -459,6 +469,11 @@ package Errout is
    --  Used if current message contains a ~ insertion character to indicate
    --  insertion of the string Error_Msg_String (1 .. Error_Msg_Strlen).
 
+   Error_Msg_Lang : String  renames Err_Vars.Error_Msg_Lang;
+   Error_Msg_Langlen : Natural renames Err_Vars.Error_Msg_Langlen;
+   --  Used if current message contains a ~~ insertion character to indicate
+   --  insertion of the string Error_Msg_Lang (1 .. Error_Msg_Langlen).
+
    -----------------------------------------------------
    -- Format of Messages and Manual Quotation Control --
    -----------------------------------------------------
@@ -735,25 +750,6 @@ package Errout is
    --  where the expression is parenthesized, an attempt is made to include
    --  the parentheses (i.e. to return the location of the initial paren).
 
-   procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr);
-   --  Wrapper on Error_Msg which adds a prefix to Msg giving the name of
-   --  the formal language analyzed (spark or alfa)
-
-   procedure Formal_Error_Msg_N (Msg : String; N : Node_Id);
-   --  Wrapper on Error_Msg_N which adds a prefix to Msg giving the name of
-   --  the formal language analyzed (spark or alfa)
-
-   procedure Formal_Error_Msg_NE
-     (Msg : String;
-      N   : Node_Or_Entity_Id;
-      E   : Node_Or_Entity_Id);
-   --  Wrapper on Error_Msg_NE which adds a prefix to Msg giving the name of
-   --  the formal language analyzed (spark or alfa)
-
-   procedure Formal_Error_Msg_SP (Msg : String);
-   --  Wrapper on Error_Msg_SP which adds a prefix to Msg giving the name of
-   --  the formal language analyzed (spark or alfa)
-
    procedure Purge_Messages (From : Source_Ptr; To : Source_Ptr)
      renames Erroutc.Purge_Messages;
    --  All error messages whose location is in the range From .. To (not
@@ -770,6 +766,10 @@ package Errout is
    --  Remove warnings on all elements of a list (Calls Remove_Warning_Messages
    --  on each element of the list, see above).
 
+   procedure Set_Error_Msg_Lang (To : String);
+   --  Set Error_Msg_Lang and Error_Msg_Langlen used for insertion character ~~
+   --  so that Error_Msg_Lang (1 .. Error_Msg_Langlen) = To.
+
    procedure Set_Ignore_Errors (To : Boolean);
    --  Following a call to this procedure with To=True, all error calls are
    --  ignored. A call with To=False restores the default treatment in which

gcc/ada/opt.adb

@@ -263,7 +263,11 @@ package body Opt is
 
    function SPARK_Mode return Boolean is
    begin
-      return Debug.Debug_Flag_Dot_DD;
+      --  When dropping the debug flag in favor of a compiler option,
+      --  the option should implicitly set the SPARK_Version, so that this test
+      --  becomes simply SPARK_Version > SPARK_None.
+
+      return Debug.Debug_Flag_Dot_DD or else SPARK_Version > SPARK_None;
    end SPARK_Mode;
 
    ---------------

gcc/ada/opt.ads

@@ -1167,6 +1167,22 @@ package Opt is
    --  GNAT
    --  Set True if a pragma Short_Descriptors applies to the current unit.
 
+   type SPARK_Version_Type is (SPARK_None, SPARK_95);
+   pragma Ordered (SPARK_Version_Type);
+   --  Versions of SPARK for SPARK_Version below. Note that these are ordered,
+   --  so that tests like SPARK_Version >= SPARK_95 are legitimate and useful.
+   --  Think twice before using "="; SPARK_Version >= SPARK_95 is more likely
+   --  what you want, because it will apply to future versions of the language.
+
+   SPARK_Version_Default : constant SPARK_Version_Type := SPARK_None;
+   --  GNAT
+   --  Default SPARK version if no switch given
+
+   SPARK_Version : SPARK_Version_Type := SPARK_Version_Default;
+   --  GNAT
+   --  Current SPARK version for compiler, as set by configuration pragmas or
+   --  compiler switches.
+
    Sprint_Line_Limit : Nat := 72;
    --  GNAT
    --  Limit values for chopping long lines in Sprint output, can be reset

gcc/ada/par-ch4.adb

@@ -670,8 +670,8 @@ package body Ch4 is
 
             if Token = Tok_Arrow or else Token = Tok_Colon_Equal then
                if SPARK_Mode then
-                  Formal_Error_Msg_SP ("no mixing of positional and named "
-                                       & "parameter association");
+                  Error_Msg_SP ("|~~no mixing of positional and named "
+                                & "parameter association");
                end if;
 
                Restore_Scan_State (Scan_State); -- to Id

gcc/ada/par-ch5.adb

@@ -2150,8 +2150,8 @@ package body Ch5 is
                      else
                         pragma Assert (SPARK_Mode);
                         Error_Msg_Sloc := Body_Sloc;
-                        Formal_Error_Msg_N
-                          ("decl cannot appear after body#", Decl);
+                        Error_Msg_F
+                          ("|~~decl cannot appear after body#", Decl);
                      end if;
                   end if;
 

gcc/ada/par-endh.adb

@@ -378,8 +378,8 @@ package body Endh is
                     and then Explicit_Start_Label (Scope.Last)
                   then
                      Error_Msg_Node_1 := Scope.Table (Scope.Last).Labl;
-                     Formal_Error_Msg_SP -- CODEFIX
-                       ("`END &` required");
+                     Error_Msg_SP -- CODEFIX
+                       ("|~~`END &` required");
                   end if;
 
                   --  Do style check for missing label

gcc/ada/par-prag.adb

@@ -439,37 +439,37 @@ begin
          List_Pragmas.Increment_Last;
          List_Pragmas.Table (List_Pragmas.Last) := (Page, Semi);
 
-         ------------------
-         -- Restrictions --
-         ------------------
+      ------------------
+      -- Restrictions --
+      ------------------
 
-         --  pragma Restrictions (RESTRICTION {, RESTRICTION});
+      --  pragma Restrictions (RESTRICTION {, RESTRICTION});
 
-         --  RESTRICTION ::=
-         --    restriction_IDENTIFIER
-         --  | restriction_parameter_IDENTIFIER => EXPRESSION
+      --  RESTRICTION ::=
+      --    restriction_IDENTIFIER
+      --  | restriction_parameter_IDENTIFIER => EXPRESSION
 
-         --  We process the case of No_Obsolescent_Features, since this has
-         --  a syntactic effect that we need to detect at parse time (the use
-         --  of replacement characters such as colon for pound sign).
+      --  We process the case of No_Obsolescent_Features, since this has
+      --  a syntactic effect that we need to detect at parse time (the use
+      --  of replacement characters such as colon for pound sign).
 
-         when Pragma_Restrictions =>
-            Process_Restrictions_Or_Restriction_Warnings;
+      when Pragma_Restrictions =>
+         Process_Restrictions_Or_Restriction_Warnings;
 
-         --------------------------
-         -- Restriction_Warnings --
-         --------------------------
+      --------------------------
+      -- Restriction_Warnings --
+      --------------------------
 
-         --  pragma Restriction_Warnings (RESTRICTION {, RESTRICTION});
+      --  pragma Restriction_Warnings (RESTRICTION {, RESTRICTION});
 
-         --  RESTRICTION ::=
-         --    restriction_IDENTIFIER
-         --  | restriction_parameter_IDENTIFIER => EXPRESSION
+      --  RESTRICTION ::=
+      --    restriction_IDENTIFIER
+      --  | restriction_parameter_IDENTIFIER => EXPRESSION
 
-         --  See above comment for pragma Restrictions
+      --  See above comment for pragma Restrictions
 
-         when Pragma_Restriction_Warnings =>
-            Process_Restrictions_Or_Restriction_Warnings;
+      when Pragma_Restriction_Warnings =>
+         Process_Restrictions_Or_Restriction_Warnings;
 
       ----------------------------------------------------------
       -- Source_File_Name and Source_File_Name_Project (GNAT) --
@@ -889,6 +889,18 @@ begin
          end if;
       end Source_Reference;
 
+      --------------
+      -- SPARK_95 --
+      --------------
+
+      --  This pragma must be processed at parse time, since we want to set
+      --  the SPARK version properly at parse time to recognize the appropriate
+      --  SPARK version syntax.
+
+      when Pragma_SPARK_95 =>
+         SPARK_Version := SPARK_95;
+         Set_Error_Msg_Lang ("(" & Formal_Language & ") ");
+
       -------------------------
       -- Style_Checks (GNAT) --
       -------------------------

gcc/ada/par.adb

@@ -1318,6 +1318,10 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is
 begin
    Compiler_State := Parsing;
 
+   if Formal_Verification_Mode then
+      Set_Error_Msg_Lang ("(" & Formal_Language & ") ");
+   end if;
+
    --  Deal with configuration pragmas case first
 
    if Configuration_Pragmas then

gcc/ada/sem_attr.adb

@@ -2065,8 +2065,8 @@ package body Sem_Attr is
         and then not In_Open_Scopes (Scope (P_Type))
         and then not In_Spec_Expression
       then
-         Formal_Error_Msg_NE
-           ("invisible attribute of}", N, First_Subtype (P_Type));
+         Error_Msg_FE
+           ("|~~invisible attribute of}", N, First_Subtype (P_Type));
       end if;
 
       --  Remaining processing depends on attribute

gcc/ada/sem_ch11.adb

@@ -444,7 +444,7 @@ package body Sem_Ch11 is
       --  Raise statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("raise statement is not allowed", N);
+         Error_Msg_F ("|~~raise statement is not allowed", N);
       end if;
 
       --  Proceed with analysis
@@ -620,7 +620,7 @@ package body Sem_Ch11 is
       if Formal_Verification_Mode
         and then Comes_From_Source (N)
       then
-         Formal_Error_Msg_N ("raise statement is not allowed", N);
+         Error_Msg_F ("|~~raise statement is not allowed", N);
       end if;
 
       --  Proceed with analysis

gcc/ada/sem_ch3.adb

@@ -2034,8 +2034,8 @@ package body Sem_Ch3 is
            and then Nkind (D) = N_Package_Declaration
            and then Nkind (Parent (L)) = N_Package_Specification
          then
-            Formal_Error_Msg_N ("package specification cannot contain "
-                                & "a package declaration", D);
+            Error_Msg_F ("|~~package specification cannot contain "
+                         & "a package declaration", D);
          end if;
 
          --  Complete analysis of declaration
@@ -2363,13 +2363,13 @@ package body Sem_Ch3 is
          --  Controlled type is not allowed in SPARK and ALFA
 
          if Is_Visibly_Controlled (T) then
-            Formal_Error_Msg_N ("controlled type is not allowed", N);
+            Error_Msg_F ("|~~controlled type is not allowed", N);
          end if;
 
          --  Discriminant type is not allowed in SPARK and ALFA
 
          if Present (Discriminant_Specifications (N)) then
-            Formal_Error_Msg_N ("discriminant type is not allowed", N);
+            Error_Msg_F ("|~~discriminant type is not allowed", N);
          end if;
       end if;
 

gcc/ada/sem_ch5.adb

@@ -809,7 +809,7 @@ package body Sem_Ch5 is
       --  Block statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("block statement is not allowed", N);
+         Error_Msg_F ("|~~block statement is not allowed", N);
       end if;
 
       --  If no handled statement sequence is present, things are really
@@ -1106,8 +1106,8 @@ package body Sem_Ch5 is
         and then Others_Present
         and then List_Length (Alternatives (N)) = 1
       then
-         Formal_Error_Msg_N
-           ("OTHERS as unique case alternative is not allowed", N);
+         Error_Msg_F
+           ("|~~OTHERS as unique case alternative is not allowed", N);
       end if;
 
       if Exp_Type = Universal_Integer and then not Others_Present then
@@ -1184,8 +1184,8 @@ package body Sem_Ch5 is
          elsif Formal_Verification_Mode
            and then Has_Loop_In_Inner_Open_Scopes (U_Name)
          then
-            Formal_Error_Msg_N
-              ("exit label must name the closest enclosing loop", N);
+            Error_Msg_F
+              ("|~~exit label must name the closest enclosing loop", N);
             return;
          else
             Set_Has_Exit (U_Name);
@@ -1230,32 +1230,32 @@ package body Sem_Ch5 is
       if Formal_Verification_Mode then
          if Present (Cond) then
             if Nkind (Parent (N)) /= N_Loop_Statement then
-               Formal_Error_Msg_N
-                 ("exit with when clause must be directly in loop", N);
+               Error_Msg_F
+                 ("|~~exit with when clause must be directly in loop", N);
             end if;
 
          else
             if Nkind (Parent (N)) /= N_If_Statement then
                if Nkind (Parent (N)) = N_Elsif_Part then
-                  Formal_Error_Msg_N ("exit must be in IF without ELSIF", N);
+                  Error_Msg_F ("|~~exit must be in IF without ELSIF", N);
                else
-                  Formal_Error_Msg_N ("exit must be directly in IF", N);
+                  Error_Msg_F ("|~~exit must be directly in IF", N);
                end if;
 
             elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
-               Formal_Error_Msg_N ("exit must be in IF directly in loop", N);
+               Error_Msg_F ("|~~exit must be in IF directly in loop", N);
 
             --  First test the presence of ELSE, so that an exit in an ELSE
             --  leads to an error mentioning the ELSE.
 
             elsif Present (Else_Statements (Parent (N))) then
-               Formal_Error_Msg_N ("exit must be in IF without ELSE", N);
+               Error_Msg_F ("|~~exit must be in IF without ELSE", N);
 
             --  An exit in an ELSIF does not reach here, as it would have been
             --  detected in the case (Nkind (Parent (N)) /= N_If_Statement).
 
             elsif Present (Elsif_Parts (Parent (N))) then
-               Formal_Error_Msg_N ("exit must be in IF without ELSIF", N);
+               Error_Msg_F ("|~~exit must be in IF without ELSIF", N);
             end if;
          end if;
       end if;
@@ -1287,7 +1287,7 @@ package body Sem_Ch5 is
       --  Goto statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("goto statement is not allowed", N);
+         Error_Msg_F ("|~~goto statement is not allowed", N);
       end if;
 
       --  Actual semantic checks
@@ -1873,8 +1873,8 @@ package body Sem_Ch5 is
                if Formal_Verification_Mode
                  and then Nkind (DS) = N_Range
                then
-                  Formal_Error_Msg_N ("loop parameter specification must "
-                                      & "include subtype mark", N);
+                  Error_Msg_F ("|~~loop parameter specification must "
+                               & "include subtype mark", N);
                end if;
 
                --  Now analyze the subtype definition. If it is a range, create
@@ -2437,8 +2437,8 @@ package body Sem_Ch5 is
                   --  Now issue the warning (or error in formal mode)
 
                   if Formal_Verification_Mode then
-                     Formal_Error_Msg
-                       ("unreachable code is not allowed", Error_Loc);
+                     Error_Msg
+                       ("|~~unreachable code is not allowed", Error_Loc);
                   else
                      Error_Msg ("?unreachable code!", Error_Loc);
                   end if;

gcc/ada/sem_ch6.adb

@@ -363,7 +363,7 @@ package body Sem_Ch6 is
       --  Abstract subprogram is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("abstract subprogram is not allowed", N);
+         Error_Msg_F ("|~~abstract subprogram is not allowed", N);
       end if;
 
       --  Proceed with analysis
@@ -694,15 +694,15 @@ package body Sem_Ch6 is
              (Nkind (Parent (Parent (N))) /= N_Subprogram_Body
                or else Present (Next (N)))
          then
-            Formal_Error_Msg_N
-              ("RETURN should be the last statement in function", N);
+            Error_Msg_F
+              ("|~~RETURN should be the last statement in function", N);
          end if;
 
       else
          --  Extended return is not allowed in SPARK or ALFA
 
          if Formal_Verification_Mode then
-            Formal_Error_Msg_N ("extended RETURN is not allowed", N);
+            Error_Msg_F ("|~~extended RETURN is not allowed", N);
          end if;
 
          --  Analyze parts specific to extended_return_statement:
@@ -1402,8 +1402,8 @@ package body Sem_Ch6 is
             --  Access result is not allowed in SPARK or ALFA
 
             if Formal_Verification_Mode then
-               Formal_Error_Msg_N
-                 ("access result is not allowed", Result_Definition (N));
+               Error_Msg_F
+                 ("|~~access result is not allowed", Result_Definition (N));
             end if;
 
             --  Ada 2005 (AI-254): Handle anonymous access to subprograms
@@ -1440,8 +1440,8 @@ package body Sem_Ch6 is
               and then Is_Array_Type (Typ)
               and then not Is_Constrained (Typ)
             then
-               Formal_Error_Msg_N
-                 ("returning an unconstrained array is not allowed",
+               Error_Msg_F
+                 ("|~~returning an unconstrained array is not allowed",
                  Result_Definition (N));
             end if;
 
@@ -1851,15 +1851,25 @@ package body Sem_Ch6 is
 
             if Formal_Verification_Mode then
                declare
-                  Last_Kind : constant Node_Kind :=
-                                Nkind (Last (Statements (HSS)));
+                  Stat : Node_Id := Last (Statements (HSS));
                begin
-                  if not Nkind_In (Last_Kind, N_Simple_Return_Statement,
-                                              N_Extended_Return_Statement)
-                  then
-                     Formal_Error_Msg_N
-                       ("last statement in function should be RETURN", N);
-                  end if;
+                  while Present (Stat) loop
+                     if Comes_From_Source (Stat) then
+                        if not Nkind_In (Nkind (Stat),
+                                         N_Simple_Return_Statement,
+                                         N_Extended_Return_Statement)
+                        then
+                           Error_Msg_F ("|~~last statement in function "
+                                        & "should be RETURN", N);
+                        end if;
+                        exit;
+                     end if;
+
+                     --  Reach before the generated statements at the end of
+                     --  the function.
+
+                     Stat := Prev (Stat);
+                  end loop;
                end;
 
             elsif Return_Present (Id) then
@@ -1891,7 +1901,7 @@ package body Sem_Ch6 is
             --  borrow the Check_Returns procedure here ???
 
             if Return_Present (Id) then
-               Formal_Error_Msg_N ("procedure should not have RETURN", N);
+               Error_Msg_F ("|~~procedure should not have RETURN", N);
             end if;
 
          --  If procedure with No_Return, check returns
@@ -2834,7 +2844,7 @@ package body Sem_Ch6 is
         and then Nkind (Specification (N)) = N_Procedure_Specification
         and then Null_Present (Specification (N))
       then
-         Formal_Error_Msg_N ("null procedure not allowed", N);
+         Error_Msg_F ("|~~null procedure not allowed", N);
       end if;
 
       --  For a null procedure, capture the profile before analysis, for
@@ -3079,7 +3089,7 @@ package body Sem_Ch6 is
         and then Comes_From_Source (N)
         and then Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
       then
-         Formal_Error_Msg_N ("user-defined operator is not allowed", N);
+         Error_Msg_F ("|~~user-defined operator is not allowed", N);
       end if;
 
       --  Proceed with analysis
@@ -8504,7 +8514,7 @@ package body Sem_Ch6 is
            and then Comes_From_Source (S)
          then
             Error_Msg_Sloc := Sloc (Homonym (S));
-            Formal_Error_Msg_N ("overloading not allowed with entity#", S);
+            Error_Msg_F ("|~~overloading not allowed with entity#", S);
          end if;
 
          --  If S is a derived operation for an untagged type then by
@@ -8770,15 +8780,14 @@ package body Sem_Ch6 is
          if Formal_Verification_Mode
            and then Ekind (Formal_Type) = E_Anonymous_Access_Type
          then
-            Formal_Error_Msg_N ("access parameter is not allowed", Param_Spec);
+            Error_Msg_F ("|~~access parameter is not allowed", Param_Spec);
          end if;
 
          if Present (Default) then
             --  Default expression is not allowed in SPARK or ALFA
 
             if Formal_Verification_Mode then
-               Formal_Error_Msg_N
-                 ("default expression is not allowed", Default);
+               Error_Msg_F ("|~~default expression is not allowed", Default);
             end if;
 
             --  Proceed with analysis

gcc/ada/sem_ch9.adb

@@ -103,7 +103,7 @@ package body Sem_Ch9 is
       --  Abort statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("abort statement is not allowed", N);
+         Error_Msg_F ("|~~abort statement is not allowed", N);
          return;
       end if;
 
@@ -181,7 +181,7 @@ package body Sem_Ch9 is
       --  Accept statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("accept statement is not allowed", N);
+         Error_Msg_F ("|~~accept statement is not allowed", N);
          return;
       end if;
 
@@ -420,7 +420,7 @@ package body Sem_Ch9 is
       --  Select statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("select statement is not allowed", N);
+         Error_Msg_F ("|~~select statement is not allowed", N);
          return;
       end if;
 
@@ -474,7 +474,7 @@ package body Sem_Ch9 is
       --  Select statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("select statement is not allowed", N);
+         Error_Msg_F ("|~~select statement is not allowed", N);
          return;
       end if;
 
@@ -579,7 +579,7 @@ package body Sem_Ch9 is
       --  Delay statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("delay statement is not allowed", N);
+         Error_Msg_F ("|~~delay statement is not allowed", N);
          return;
       end if;
 
@@ -605,7 +605,7 @@ package body Sem_Ch9 is
       --  Delay statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("delay statement is not allowed", N);
+         Error_Msg_F ("|~~delay statement is not allowed", N);
          return;
       end if;
 
@@ -900,7 +900,7 @@ package body Sem_Ch9 is
       --  Entry call is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("entry call is not allowed", N);
+         Error_Msg_F ("|~~entry call is not allowed", N);
          return;
       end if;
 
@@ -1359,7 +1359,7 @@ package body Sem_Ch9 is
       --  Requeue statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("requeue statement is not allowed", N);
+         Error_Msg_F ("|~~requeue statement is not allowed", N);
          return;
       end if;
 
@@ -1641,7 +1641,7 @@ package body Sem_Ch9 is
       --  Select statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("select statement is not allowed", N);
+         Error_Msg_F ("|~~select statement is not allowed", N);
          return;
       end if;
 
@@ -2178,7 +2178,7 @@ package body Sem_Ch9 is
       --  Select statement is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode then
-         Formal_Error_Msg_N ("select statement is not allowed", N);
+         Error_Msg_F ("|~~select statement is not allowed", N);
          return;
       end if;
 

gcc/ada/sem_prag.adb

@@ -12320,6 +12320,22 @@ package body Sem_Prag is
          when Pragma_Source_Reference =>
             GNAT_Pragma;
 
+         --------------
+         -- SPARK_95 --
+         --------------
+
+         --  pragma SPARK_95;
+
+         --  Note: this pragma also has some specific processing in Par.Prag
+         --  because we want to set the SPARK 95 version mode during parsing.
+
+         when Pragma_SPARK_95 =>
+            GNAT_Pragma;
+            Check_Arg_Count (0);
+            Check_Valid_Configuration_Pragma;
+            SPARK_Version := SPARK_95;
+            Set_Error_Msg_Lang ("(" & Formal_Language & ") ");
+
          --------------------------------
          -- Static_Elaboration_Desired --
          --------------------------------
@@ -14071,6 +14087,7 @@ package body Sem_Prag is
       Pragma_Source_File_Name              => -1,
       Pragma_Source_File_Name_Project      => -1,
       Pragma_Source_Reference              => -1,
+      Pragma_SPARK_95                      => -1,
       Pragma_Storage_Size                  => -1,
       Pragma_Storage_Unit                  => -1,
       Pragma_Static_Elaboration_Desired    => -1,

gcc/ada/sem_util.adb

@@ -3234,7 +3234,7 @@ package body Sem_Util is
         and then Comes_From_Source (C)
       then
          Error_Msg_Sloc := Sloc (C);
-         Formal_Error_Msg_N ("redeclaration of identifier &#", Def_Id);
+         Error_Msg_F ("|~~redeclaration of identifier &#", Def_Id);
       end if;
 
       --  Warn if new entity hides an old one

gcc/ada/snames.ads-tmpl

@@ -404,6 +404,7 @@ package Snames is
    Name_Short_Descriptors              : constant Name_Id := N + $; -- GNAT
    Name_Source_File_Name               : constant Name_Id := N + $; -- GNAT
    Name_Source_File_Name_Project       : constant Name_Id := N + $; -- GNAT
+   Name_SPARK_95                       : constant Name_Id := N + $; -- GNAT
    Name_Style_Checks                   : constant Name_Id := N + $; -- GNAT
    Name_Suppress                       : constant Name_Id := N + $;
    Name_Suppress_Exception_Locations   : constant Name_Id := N + $; -- GNAT
@@ -1517,6 +1518,7 @@ package Snames is
       Pragma_Short_Descriptors,
       Pragma_Source_File_Name,
       Pragma_Source_File_Name_Project,
+      Pragma_SPARK_95,
       Pragma_Style_Checks,
       Pragma_Suppress,
       Pragma_Suppress_Exception_Locations,