+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,
-- --
-- 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- --
-- 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;
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 --
----------------
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 --
-----------------------
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;
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
-- 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 --
----------------------------------------
-- 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 --
-----------------------------------------------------
-- 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
-- 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
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;
---------------
-- 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
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
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;
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
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) --
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) --
-------------------------
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
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
-- 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
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
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
-- 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;
-- 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
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
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);
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;
-- 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
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
-- 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;
-- 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
(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:
-- 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
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;
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
-- 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
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
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
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
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
-- 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;
-- 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;
-- 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;
-- 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;
-- 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;
-- 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;
-- 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;
-- 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;
-- 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;
-- 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;
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 --
--------------------------------
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,
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
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
Pragma_Short_Descriptors,
Pragma_Source_File_Name,
Pragma_Source_File_Name_Project,
+ Pragma_SPARK_95,
Pragma_Style_Checks,
Pragma_Suppress,
Pragma_Suppress_Exception_Locations,
projects / gcc.git / commitdiff