diff options
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 28 | ||||
| -rw-r--r-- | gcc/ada/err_vars.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/errout.adb | 61 | ||||
| -rw-r--r-- | gcc/ada/errout.ads | 38 | ||||
| -rw-r--r-- | gcc/ada/opt.adb | 6 | ||||
| -rw-r--r-- | gcc/ada/opt.ads | 16 | ||||
| -rw-r--r-- | gcc/ada/par-ch4.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/par-ch5.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/par-endh.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/par-prag.adb | 56 | ||||
| -rw-r--r-- | gcc/ada/par.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_attr.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_ch11.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_ch5.adb | 34 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 55 | ||||
| -rw-r--r-- | gcc/ada/sem_ch9.adb | 20 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 17 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 2 |
20 files changed, 221 insertions, 153 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 97fc48e4bb8..d79f7c7c793 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,31 @@ +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, diff --git a/gcc/ada/err_vars.ads b/gcc/ada/err_vars.ads index 2cf2bedc9a6..22f70f61251 100644 --- a/gcc/ada/err_vars.ads +++ b/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; diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index 0703afc89a7..be963dbf952 100644 --- a/gcc/ada/errout.adb +++ b/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 diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads index af219647a57..611ca02e0d0 100644 --- a/gcc/ada/errout.ads +++ b/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 diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb index cb03ef51ecd..1e7bf0f709e 100644 --- a/gcc/ada/opt.adb +++ b/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; --------------- diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 66c1e85578d..ed6c53c43b4 100644 --- a/gcc/ada/opt.ads +++ b/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 diff --git a/gcc/ada/par-ch4.adb b/gcc/ada/par-ch4.adb index e80a7ccdda6..74ab7604a8a 100644 --- a/gcc/ada/par-ch4.adb +++ b/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 diff --git a/gcc/ada/par-ch5.adb b/gcc/ada/par-ch5.adb index 27bc899f09e..3c8f2d5f562 100644 --- a/gcc/ada/par-ch5.adb +++ b/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; diff --git a/gcc/ada/par-endh.adb b/gcc/ada/par-endh.adb index ae18703e8ed..12c5509e431 100644 --- a/gcc/ada/par-endh.adb +++ b/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 diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 8ddd2209ad6..502cb70b253 100644 --- a/gcc/ada/par-prag.adb +++ b/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) -- ------------------------- diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb index 99f6806057d..b4c8d83e4dd 100644 --- a/gcc/ada/par.adb +++ b/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 diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 73239e600aa..1b6d3ef30b6 100644 --- a/gcc/ada/sem_attr.adb +++ b/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 diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index ce71e7fc91b..1b0c182713a 100644 --- a/gcc/ada/sem_ch11.adb +++ b/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 diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 5aaf772a0e4..52ff6134439 100644 --- a/gcc/ada/sem_ch3.adb +++ b/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; diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 42b474a0c39..e572aa20791 100644 --- a/gcc/ada/sem_ch5.adb +++ b/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; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 530a51c9f21..213f55addb9 100644 --- a/gcc/ada/sem_ch6.adb +++ b/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 diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index e25c92f4e59..523f62167a6 100644 --- a/gcc/ada/sem_ch9.adb +++ b/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; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index f66c8f91eee..f09f744ba8f 100644 --- a/gcc/ada/sem_prag.adb +++ b/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, diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 9974ec98526..45e4a4f202c 100644 --- a/gcc/ada/sem_util.adb +++ b/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 diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 03def0d825a..dbe0814ce41 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/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, |