===================================================================
@@ -3065,6 +3065,32 @@
return False;
end Special_Msg_Delete;
+ -----------------
+ -- SPARK_Msg_N --
+ -----------------
+
+ procedure SPARK_Msg_N (Msg : String; N : Node_Or_Entity_Id) is
+ begin
+ if SPARK_Mode = On then
+ Error_Msg_N (Msg, N);
+ end if;
+ end SPARK_Msg_N;
+
+ ------------------
+ -- SPARK_Msg_NE --
+ ------------------
+
+ procedure SPARK_Msg_NE
+ (Msg : String;
+ N : Node_Or_Entity_Id;
+ E : Node_Or_Entity_Id)
+ is
+ begin
+ if SPARK_Mode = On then
+ Error_Msg_NE (Msg, N, E);
+ end if;
+ end SPARK_Msg_NE;
+
--------------------------
-- Unwind_Internal_Type --
--------------------------
===================================================================
@@ -909,6 +909,29 @@
-- Debugging routine to dump an error message
------------------------------------
+ -- SPARK Error Output Subprograms --
+ ------------------------------------
+
+ -- The following routines are intended to report semantic errors in SPARK
+ -- constructs subject to aspect/pragma SPARK_Mode. Note that syntax errors
+ -- must be reported using the Error_Msg_XXX routines. This allows for the
+ -- partial analysis of SPARK features when they are disabled via SPARK_Mode
+ -- set to "off".
+
+ procedure SPARK_Msg_N (Msg : String; N : Node_Or_Entity_Id);
+ pragma Inline (SPARK_Msg_N);
+ -- Same as Error_Msg_N, but the error is reported only when SPARK_Mode is
+ -- "on". The routine is inlined because it acts as a simple wrapper.
+
+ procedure SPARK_Msg_NE
+ (Msg : String;
+ N : Node_Or_Entity_Id;
+ E : Node_Or_Entity_Id);
+ pragma Inline (SPARK_Msg_NE);
+ -- Same as Error_Msg_NE, but the error is reported only when SPARK_Mode is
+ -- "on". The routine is inlined because it acts as a simple wrapper.
+
+ ------------------------------------
-- Utility Interface for Back End --
------------------------------------
===================================================================
@@ -2007,10 +2007,51 @@
-- immediately.
when Aspect_Abstract_State => Abstract_State : declare
+ procedure Insert_After_SPARK_Mode
+ (Ins_Nod : Node_Id;
+ Decls : List_Id);
+ -- Insert Aitem before node Ins_Nod. If Ins_Nod denotes
+ -- pragma SPARK_Mode, then SPARK_Mode is skipped. Decls is
+ -- the associated declarative list where Aitem is to reside.
+
+ -----------------------------
+ -- Insert_After_SPARK_Mode --
+ -----------------------------
+
+ procedure Insert_After_SPARK_Mode
+ (Ins_Nod : Node_Id;
+ Decls : List_Id)
+ is
+ Decl : Node_Id := Ins_Nod;
+
+ begin
+ -- Skip SPARK_Mode
+
+ if Present (Decl)
+ and then Nkind (Decl) = N_Pragma
+ and then Pragma_Name (Decl) = Name_SPARK_Mode
+ then
+ Decl := Next (Decl);
+ end if;
+
+ if Present (Decl) then
+ Insert_Before (Decl, Aitem);
+
+ -- Aitem acts as the last declaration
+
+ else
+ Append_To (Decls, Aitem);
+ end if;
+ end Insert_After_SPARK_Mode;
+
+ -- Local variables
+
Context : Node_Id := N;
Decl : Node_Id;
Decls : List_Id;
+ -- Start of processing for Abstract_State
+
begin
-- When aspect Abstract_State appears on a generic package,
-- it is propageted to the package instance. The context in
@@ -2061,17 +2102,20 @@
Decl := Next (Decl);
end loop;
- if Present (Decl) then
- Insert_Before (Decl, Aitem);
- else
- Append_To (Decls, Aitem);
- end if;
+ -- Pragma Abstract_State must be inserted after
+ -- pragma SPARK_Mode in the tree. This ensures that
+ -- any error messages dependent on SPARK_Mode will
+ -- be properly enabled/suppressed.
+ Insert_After_SPARK_Mode (Decl, Decls);
+
-- The related package is not a generic instance, the
- -- corresponding pragma must be the first declaration.
+ -- corresponding pragma must be the first declaration
+ -- except when SPARK_Mode is already in the list. In
+ -- that case pragma Abstract_State is placed second.
else
- Prepend_To (Decls, Aitem);
+ Insert_After_SPARK_Mode (First (Decls), Decls);
end if;
-- Otherwise the pragma forms a new declarative list
===================================================================
@@ -184,19 +184,6 @@
-- whether a particular item appears in a mixed list of nodes and entities.
-- It is assumed that all nodes in the list have entities.
- procedure Check_Dependence_List_Syntax (List : Node_Id);
- -- Subsidiary to the analysis of pragmas Depends and Refined_Depends.
- -- Verify the syntax of dependence relation List.
-
- procedure Check_Global_List_Syntax (List : Node_Id);
- -- Subsidiary to the analysis of pragmas Global and Refined_Global. Verify
- -- the syntax of global list List.
-
- procedure Check_Item_Syntax (Item : Node_Id);
- -- Subsidiary to the analysis of pragmas Depends, Global, Initializes,
- -- Part_Of, Refined_Depends, Refined_Depends and Refined_State. Verify the
- -- syntax of a SPARK annotation item.
-
function Check_Kind (Nam : Name_Id) return Name_Id;
-- This function is used in connection with pragmas Assert, Check,
-- and assertion aspects and pragmas, to determine if Check pragmas
@@ -674,7 +661,7 @@
if Nkind (Inputs) = N_Aggregate then
if Present (Component_Associations (Inputs)) then
- Error_Msg_N
+ SPARK_Msg_N
("nested dependency relations not allowed", Inputs);
elsif Present (Expressions (Inputs)) then
@@ -692,6 +679,8 @@
Next (Input);
end loop;
+ -- Syntax error, always report
+
else
Error_Msg_N ("malformed input dependency list", Inputs);
end if;
@@ -714,7 +703,7 @@
-- (null =>[+] null)
if Null_Output_Seen and then Null_Input_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("null dependency clause cannot have a null input list",
Inputs);
end if;
@@ -742,10 +731,10 @@
if Nkind (Item) = N_Aggregate then
if not Top_Level then
- Error_Msg_N ("nested grouping of items not allowed", Item);
+ SPARK_Msg_N ("nested grouping of items not allowed", Item);
elsif Present (Component_Associations (Item)) then
- Error_Msg_N
+ SPARK_Msg_N
("nested dependency relations not allowed", Item);
-- Recursively analyze the grouped items
@@ -765,6 +754,8 @@
Next (Grouped);
end loop;
+ -- Syntax error, always report
+
else
Error_Msg_N ("malformed dependency list", Item);
end if;
@@ -787,7 +778,7 @@
or else Entity (Prefix (Item)) /= Spec_Id
then
Error_Msg_Name_1 := Name_Result;
- Error_Msg_N
+ SPARK_Msg_N
("prefix of attribute % must denote the enclosing "
& "function", Item);
@@ -795,10 +786,10 @@
-- dependency clause (SPARK RM 6.1.5(6)).
elsif Is_Input then
- Error_Msg_N ("function result cannot act as input", Item);
+ SPARK_Msg_N ("function result cannot act as input", Item);
elsif Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix null and non-null dependency items", Item);
else
@@ -811,11 +802,11 @@
elsif Nkind (Item) = N_Null then
if Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("multiple null dependency relations not allowed", Item);
elsif Non_Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix null and non-null dependency items", Item);
else
@@ -823,7 +814,7 @@
if Is_Output then
if not Is_Last then
- Error_Msg_N
+ SPARK_Msg_N
("null output list must be the last clause in a "
& "dependency relation", Item);
@@ -831,7 +822,7 @@
-- null =>+ ...
elsif Self_Ref then
- Error_Msg_N
+ SPARK_Msg_N
("useless dependence, null depends on itself", Item);
end if;
end if;
@@ -843,7 +834,7 @@
Non_Null_Seen := True;
if Null_Seen then
- Error_Msg_N ("cannot mix null and non-null items", Item);
+ SPARK_Msg_N ("cannot mix null and non-null items", Item);
end if;
Analyze (Item);
@@ -873,7 +864,7 @@
-- item to the list of processed relations.
if Contains (Seen, Item_Id) then
- Error_Msg_NE
+ SPARK_Msg_NE
("duplicate use of item &", Item, Item_Id);
else
Add_Item (Item_Id, Seen);
@@ -887,7 +878,7 @@
and then Null_Output_Seen
and then Contains (All_Inputs_Seen, Item_Id)
then
- Error_Msg_N
+ SPARK_Msg_N
("input of a null output list cannot appear in "
& "multiple input lists", Item);
end if;
@@ -903,10 +894,10 @@
if Ekind (Item_Id) = E_Abstract_State then
if Has_Visible_Refinement (Item_Id) then
- Error_Msg_NE
+ SPARK_Msg_NE
("cannot mention state & in global refinement",
Item, Item_Id);
- Error_Msg_N
+ SPARK_Msg_N
("\use its constituents instead", Item);
return;
@@ -948,18 +939,17 @@
-- (SPARK RM 6.1.5(1)).
else
- Error_Msg_N
+ SPARK_Msg_N
("item must denote parameter, variable, or state",
Item);
end if;
-- All other input/output items are illegal
- -- (SPARK RM 6.1.5(1))
+ -- (SPARK RM 6.1.5(1)). This is a syntax error, always report.
else
Error_Msg_N
- ("item must denote parameter, variable, or state",
- Item);
+ ("item must denote parameter, variable, or state", Item);
end if;
end if;
end Analyze_Input_Output;
@@ -1015,7 +1005,7 @@
procedure Check_Function_Return is
begin
if Ekind (Spec_Id) = E_Function and then not Result_Seen then
- Error_Msg_NE
+ SPARK_Msg_NE
("result of & must appear in exactly one output list",
N, Spec_Id);
end if;
@@ -1164,10 +1154,10 @@
(" & cannot appear in dependence relation");
Error_Msg := Name_Find;
- Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+ SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
Error_Msg_Name_1 := Chars (Subp_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("\& is not part of the input or output set of subprogram %",
Item, Item_Id);
@@ -1194,7 +1184,7 @@
Add_Str_To_Name_Buffer (" in dependence relation");
Error_Msg := Name_Find;
- Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+ SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
end if;
end Role_Error;
@@ -1266,7 +1256,7 @@
(" & must appear in at least one input dependence list");
Error_Msg := Name_Find;
- Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+ SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
end if;
-- Output case (SPARK RM 6.1.5(10))
@@ -1279,7 +1269,7 @@
(" & must appear in exactly one output dependence list");
Error_Msg := Name_Find;
- Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+ SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
end if;
end Usage_Error;
@@ -1486,7 +1476,7 @@
-- appear in the input list of a relation (SPARK RM 6.1.5(10)).
elsif Is_Attribute_Result (Output) then
- Error_Msg_N ("function result cannot depend on itself", Output);
+ SPARK_Msg_N ("function result cannot depend on itself", Output);
return;
end if;
@@ -1683,14 +1673,6 @@
begin
Set_Analyzed (N);
- -- Verify the syntax of pragma Depends when SPARK checks are suppressed.
- -- Semantic analysis and normalization are disabled in this mode.
-
- if SPARK_Mode = Off then
- Check_Dependence_List_Syntax (Deps);
- return;
- end if;
-
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Subp_Id := Defining_Entity (Subp_Decl);
@@ -1809,14 +1791,16 @@
Check_Usage (Subp_Outputs, All_Outputs_Seen, False);
Check_Function_Return;
- -- The dependency list is malformed
+ -- The dependency list is malformed. This is a syntax error, always
+ -- report.
else
Error_Msg_N ("malformed dependency relation", Deps);
return;
end if;
- -- The top level dependency relation is malformed
+ -- The top level dependency relation is malformed. This is a syntax
+ -- error, always report.
else
Error_Msg_N ("malformed dependency relation", Deps);
@@ -1855,10 +1839,10 @@
and then Present (Entity (Obj))
and then Is_Formal (Entity (Obj))
then
- Error_Msg_N ("external property % cannot apply to parameter", N);
+ SPARK_Msg_N ("external property % cannot apply to parameter", N);
end if;
else
- Error_Msg_N
+ SPARK_Msg_N
("external property % must apply to a volatile object", N);
end if;
@@ -1874,7 +1858,7 @@
Expr_Val := Is_True (Expr_Value (Expr));
else
Error_Msg_Name_1 := Pragma_Name (N);
- Error_Msg_N ("expression of % must be static", Expr);
+ SPARK_Msg_N ("expression of % must be static", Expr);
end if;
end if;
end Analyze_External_Property_In_Decl_Part;
@@ -1969,7 +1953,7 @@
-- with Global => (Name, null)
if Nkind (Item) = N_Null then
- Error_Msg_N ("cannot mix null and non-null global items", Item);
+ SPARK_Msg_N ("cannot mix null and non-null global items", Item);
return;
end if;
@@ -1990,7 +1974,7 @@
if Is_Formal (Item_Id) then
if Scope (Item_Id) = Spec_Id then
- Error_Msg_NE
+ SPARK_Msg_NE
("global item cannot reference parameter of subprogram",
Item, Spec_Id);
return;
@@ -2000,13 +1984,13 @@
-- Do this check first to provide a better error diagnostic.
elsif Ekind (Item_Id) = E_Constant then
- Error_Msg_N ("global item cannot denote a constant", Item);
+ SPARK_Msg_N ("global item cannot denote a constant", Item);
-- The only legal references are those to abstract states and
-- variables (SPARK RM 6.1.4(4)).
elsif not Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
- Error_Msg_N
+ SPARK_Msg_N
("global item must denote variable or state", Item);
return;
end if;
@@ -2020,10 +2004,10 @@
-- some of its constituents (SPARK RM 6.1.4(8)).
if Has_Visible_Refinement (Item_Id) then
- Error_Msg_NE
+ SPARK_Msg_NE
("cannot mention state & in global refinement",
Item, Item_Id);
- Error_Msg_N ("\use its constituents instead", Item);
+ SPARK_Msg_N ("\use its constituents instead", Item);
return;
-- If the reference to the abstract state appears in an
@@ -2093,7 +2077,7 @@
-- (SPARK RM 6.1.4(11)).
if Contains (Seen, Item_Id) then
- Error_Msg_N ("duplicate global item", Item);
+ SPARK_Msg_N ("duplicate global item", Item);
-- Add the entity of the current item to the list of processed
-- items.
@@ -2123,7 +2107,7 @@
is
begin
if Status then
- Error_Msg_N ("duplicate global mode", Mode);
+ SPARK_Msg_N ("duplicate global mode", Mode);
end if;
Status := True;
@@ -2166,10 +2150,10 @@
if Appears_In (Inputs, Item_Id)
and then not Appears_In (Outputs, Item_Id)
then
- Error_Msg_NE
+ SPARK_Msg_NE
("global item & cannot have mode In_Out or Output",
Item, Item_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("\item already appears as input of subprogram &",
Item, Context);
@@ -2190,7 +2174,7 @@
procedure Check_Mode_Restriction_In_Function (Mode : Node_Id) is
begin
if Ekind (Spec_Id) = E_Function then
- Error_Msg_N
+ SPARK_Msg_N
("global mode & is not applicable to functions", Mode);
end if;
end Check_Mode_Restriction_In_Function;
@@ -2225,7 +2209,7 @@
if Present (Expressions (List)) then
if Present (Component_Associations (List)) then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix moded and non-moded global lists", List);
end if;
@@ -2242,7 +2226,7 @@
elsif Present (Component_Associations (List)) then
if Present (Expressions (List)) then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix moded and non-moded global lists", List);
end if;
@@ -2266,11 +2250,11 @@
Check_Duplicate_Mode (Mode, Proof_Seen);
else
- Error_Msg_N ("invalid mode selector", Mode);
+ SPARK_Msg_N ("invalid mode selector", Mode);
end if;
else
- Error_Msg_N ("invalid mode selector", Mode);
+ SPARK_Msg_N ("invalid mode selector", Mode);
end if;
-- Items in a moded list appear as a collection of
@@ -2290,7 +2274,8 @@
raise Program_Error;
end if;
- -- Any other attempt to declare a global item is illegal
+ -- Any other attempt to declare a global item is illegal. This is a
+ -- syntax error, always report.
else
Error_Msg_N ("malformed global list", List);
@@ -2312,14 +2297,6 @@
Set_Analyzed (N);
Check_SPARK_Aspect_For_ASIS (N);
- -- Verify the syntax of pragma Global when SPARK checks are suppressed.
- -- Semantic analysis is disabled in this mode.
-
- if SPARK_Mode = Off then
- Check_Global_List_Syntax (Items);
- return;
- end if;
-
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Subp_Id := Defining_Entity (Subp_Decl);
@@ -2434,9 +2411,6 @@
-- Verify the legality of a single initialization item followed by a
-- list of input items.
- procedure Check_Initialization_List_Syntax (List : Node_Id);
- -- Verify the syntax of initialization list List
-
procedure Collect_States_And_Variables;
-- Inspect the visible declarations of the related package and gather
-- the entities of all abstract states and variables in States_And_Vars.
@@ -2453,10 +2427,10 @@
if Nkind (Item) = N_Null then
if Null_Seen then
- Error_Msg_N ("multiple null initializations not allowed", Item);
+ SPARK_Msg_N ("multiple null initializations not allowed", Item);
elsif Non_Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix null and non-null initialization items", Item);
else
Null_Seen := True;
@@ -2468,7 +2442,7 @@
Non_Null_Seen := True;
if Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix null and non-null initialization items", Item);
end if;
@@ -2485,7 +2459,7 @@
if not Contains (States_And_Vars, Item_Id) then
Error_Msg_Name_1 := Chars (Pack_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("initialization item & must appear in the visible "
& "declarations of package %", Item, Item_Id);
@@ -2493,7 +2467,7 @@
-- (SPARK RM 7.1.5(5)).
elsif Contains (Items_Seen, Item_Id) then
- Error_Msg_N ("duplicate initialization item", Item);
+ SPARK_Msg_N ("duplicate initialization item", Item);
-- The item is legal, add it to the list of processed states
-- and variables.
@@ -2514,13 +2488,13 @@
-- variable (SPARK RM 7.1.5(3)).
else
- Error_Msg_N
+ SPARK_Msg_N
("initialization item must denote variable or state",
Item);
end if;
-- Some form of illegal construct masquerading as a name
- -- (SPARK RM 7.1.5(3)).
+ -- (SPARK RM 7.1.5(3)). This is a syntax error, always report.
else
Error_Msg_N
@@ -2557,11 +2531,11 @@
if Nkind (Input) = N_Null then
if Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("multiple null initializations not allowed", Item);
elsif Non_Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix null and non-null initialization item", Item);
else
Null_Seen := True;
@@ -2573,7 +2547,7 @@
Non_Null_Seen := True;
if Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix null and non-null initialization item", Item);
end if;
@@ -2594,7 +2568,7 @@
if Within_Scope (Input_Id, Current_Scope) then
Error_Msg_Name_1 := Chars (Pack_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("input item & cannot denote a visible variable or "
& "state of package % (SPARK RM 7.1.5(4))",
Input, Input_Id);
@@ -2603,7 +2577,7 @@
-- (SPARK RM 7.1.5(5)).
elsif Contains (Inputs_Seen, Input_Id) then
- Error_Msg_N ("duplicate input item", Input);
+ SPARK_Msg_N ("duplicate input item", Input);
-- Input is legal, add it to the list of processed inputs
@@ -2625,7 +2599,7 @@
-- variable (SPARK RM 7.1.5(3)).
else
- Error_Msg_N
+ SPARK_Msg_N
("input item must denote variable or state", Input);
end if;
@@ -2633,7 +2607,7 @@
-- (SPARK RM 7.1.5(3)).
else
- Error_Msg_N
+ SPARK_Msg_N
("input item must denote variable or state", Input);
end if;
end if;
@@ -2656,7 +2630,7 @@
Elmt := First (Choices (Item));
while Present (Elmt) loop
if Name_Seen then
- Error_Msg_N ("only one item allowed in initialization", Elmt);
+ SPARK_Msg_N ("only one item allowed in initialization", Elmt);
else
Name_Seen := True;
Analyze_Initialization_Item (Elmt);
@@ -2677,7 +2651,7 @@
end if;
if Present (Component_Associations (Inputs)) then
- Error_Msg_N
+ SPARK_Msg_N
("inputs must appear in named association form", Inputs);
end if;
@@ -2688,61 +2662,6 @@
end if;
end Analyze_Initialization_Item_With_Inputs;
- --------------------------------------
- -- Check_Initialization_List_Syntax --
- --------------------------------------
-
- procedure Check_Initialization_List_Syntax (List : Node_Id) is
- Init : Node_Id;
- Input : Node_Id;
-
- begin
- -- Null initialization list
-
- if Nkind (List) = N_Null then
- null;
-
- elsif Nkind (List) = N_Aggregate then
-
- -- Simple initialization items
-
- if Present (Expressions (List)) then
- Init := First (Expressions (List));
- while Present (Init) loop
- Check_Item_Syntax (Init);
- Next (Init);
- end loop;
- end if;
-
- -- Initialization items with a input lists
-
- if Present (Component_Associations (List)) then
- Init := First (Component_Associations (List));
- while Present (Init) loop
- Check_Item_Syntax (First (Choices (Init)));
-
- if Nkind (Expression (Init)) = N_Aggregate
- and then Present (Expressions (Expression (Init)))
- then
- Input := First (Expressions (Expression (Init)));
- while Present (Input) loop
- Check_Item_Syntax (Input);
- Next (Input);
- end loop;
-
- else
- Error_Msg_N ("malformed initialization item", Init);
- end if;
-
- Next (Init);
- end loop;
- end if;
-
- else
- Error_Msg_N ("malformed initialization list", List);
- end if;
- end Check_Initialization_List_Syntax;
-
----------------------------------
-- Collect_States_And_Variables --
----------------------------------
@@ -2792,13 +2711,6 @@
if Nkind (Inits) = N_Null then
return;
-
- -- Verify the syntax of pragma Initializes when SPARK checks are
- -- suppressed. Semantic analysis is disabled in this mode.
-
- elsif SPARK_Mode = Off then
- Check_Initialization_List_Syntax (Inits);
- return;
end if;
-- Single and multiple initialization clauses appear as an aggregate. If
@@ -2840,10 +2752,6 @@
-- Analyze_Pragma --
--------------------
- --------------------
- -- Analyze_Pragma --
- --------------------
-
procedure Analyze_Pragma (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
Prag_Id : Pragma_Id;
@@ -3478,21 +3386,25 @@
Legal := False;
- -- Verify the syntax of the encapsulating state when SPARK check are
- -- suppressed. Semantic analysis is disabled in this mode.
+ if Nkind_In (State, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
+ then
+ Analyze (State);
+ Resolve_State (State);
- if SPARK_Mode = Off then
- Check_Item_Syntax (State);
- return;
- end if;
+ if Is_Entity_Name (State)
+ and then Ekind (Entity (State)) = E_Abstract_State
+ then
+ State_Id := Entity (State);
- Analyze (State);
- Resolve_State (State);
+ else
+ SPARK_Msg_N
+ ("indicator Part_Of must denote an abstract state", State);
+ return;
+ end if;
- if Is_Entity_Name (State)
- and then Ekind (Entity (State)) = E_Abstract_State
- then
- State_Id := Entity (State);
+ -- This is a syntax error, always report
else
Error_Msg_N
@@ -3516,11 +3428,11 @@
-- visible.
if Placement = Not_In_Package then
- Error_Msg_N
+ SPARK_Msg_N
("indicator Part_Of cannot appear in this context "
& "(SPARK RM 7.2.6(5))", Indic);
Error_Msg_Name_1 := Chars (Scope (State_Id));
- Error_Msg_NE
+ SPARK_Msg_NE
("\& is not part of the hidden state of package %",
Indic, Item_Id);
@@ -3554,7 +3466,7 @@
Parent_Unit := Scope (Parent_Unit);
if not Is_Child_Or_Sibling (Pack_Id, Scope (State_Id)) then
- Error_Msg_NE
+ SPARK_Msg_NE
("indicator Part_Of must denote an abstract state of& "
& "or public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
@@ -3567,7 +3479,7 @@
null;
else
- Error_Msg_NE
+ SPARK_Msg_NE
("indicator Part_Of must denote an abstract state of& "
& "or public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
@@ -3577,11 +3489,11 @@
-- a private child unit or a public descendant thereof.
else
- Error_Msg_N
- ("indicator Part_Of cannot appear in this context (SPARK "
- & "RM 7.2.6(5))", Indic);
+ SPARK_Msg_N
+ ("indicator Part_Of cannot appear in this context "
+ & "(SPARK RM 7.2.6(5))", Indic);
Error_Msg_Name_1 := Chars (Pack_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("\& is declared in the visible part of package %",
Indic, Item_Id);
end if;
@@ -3591,11 +3503,11 @@
elsif Placement = Private_State_Space then
if Scope (State_Id) /= Pack_Id then
- Error_Msg_NE
+ SPARK_Msg_NE
("indicator Part_Of must designate an abstract state of "
& "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
Error_Msg_Name_1 := Chars (Pack_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("\& is declared in the private part of package %",
Indic, Item_Id);
end if;
@@ -3604,13 +3516,13 @@
-- Part_Of indicators as the refinement has already been seen.
else
- Error_Msg_N
+ SPARK_Msg_N
("indicator Part_Of cannot appear in this context "
& "(SPARK RM 7.2.6(5))", Indic);
if Scope (State_Id) = Pack_Id then
Error_Msg_Name_1 := Chars (Pack_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("\& is declared in the body of package %", Indic, Item_Id);
end if;
end if;
@@ -4227,7 +4139,7 @@
-- If we get here, then the aspects are out of order
- Error_Msg_N ("aspect % cannot come after aspect %", First);
+ SPARK_Msg_N ("aspect % cannot come after aspect %", First);
end Check_Aspect_Specification_Order;
-- Local variables
@@ -4262,7 +4174,7 @@
else
if From_Aspect_Specification (Second) then
- Error_Msg_N ("pragma % cannot come after aspect %", First);
+ SPARK_Msg_N ("pragma % cannot come after aspect %", First);
-- Both pragmas are source constructs. Try to reach First from
-- Second by traversing the declarations backwards.
@@ -4282,7 +4194,7 @@
-- If we get here, then the pragmas are out of order
- Error_Msg_N ("pragma % cannot come after pragma %", First);
+ SPARK_Msg_N ("pragma % cannot come after pragma %", First);
end if;
end if;
end Check_Declaration_Order;
@@ -10235,9 +10147,6 @@
-- decorate a state abstraction entity and introduce it into the
-- visibility chain.
- procedure Check_State_Declaration_Syntax (State : Node_Id);
- -- Verify the syntex of state declaration State
-
----------------------------
-- Analyze_Abstract_State --
----------------------------
@@ -10392,7 +10301,7 @@
if Nkind (Prop) = N_Others_Choice then
if Others_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("only one others choice allowed in option External",
Prop);
else
@@ -10400,7 +10309,7 @@
end if;
elsif Others_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("others must be the last property in option External",
Prop);
@@ -10418,7 +10327,7 @@
-- Otherwise the construct is not a valid property
else
- Error_Msg_N ("invalid external state property", Prop);
+ SPARK_Msg_N ("invalid external state property", Prop);
return;
end if;
@@ -10431,7 +10340,7 @@
if Is_Static_Expression (Expr) then
Expr_Val := Is_True (Expr_Value (Expr));
else
- Error_Msg_N
+ SPARK_Msg_N
("expression of external state property must be "
& "static", Expr);
end if;
@@ -10525,7 +10434,7 @@
is
begin
if Status then
- Error_Msg_N ("duplicate state option", Opt);
+ SPARK_Msg_N ("duplicate state option", Opt);
end if;
Status := True;
@@ -10541,7 +10450,7 @@
is
begin
if Status then
- Error_Msg_N ("duplicate external property", Prop);
+ SPARK_Msg_N ("duplicate external property", Prop);
end if;
Status := True;
@@ -10605,7 +10514,7 @@
-- declare additional states.
if Null_Seen then
- Error_Msg_NE
+ SPARK_Msg_NE
("package & has null abstract state", State, Pack_Id);
-- Null states appear as internally generated entities
@@ -10622,7 +10531,7 @@
-- non-null states.
if Non_Null_Seen then
- Error_Msg_NE
+ SPARK_Msg_NE
("package & has non-null abstract state",
State, Pack_Id);
end if;
@@ -10649,7 +10558,7 @@
Is_Null => False);
Non_Null_Seen := True;
else
- Error_Msg_N
+ SPARK_Msg_N
("state name must be an identifier",
Ancestor_Part (State));
end if;
@@ -10671,12 +10580,12 @@
-- (SPARK RM 7.1.4(9)).
elsif Chars (Opt) = Name_Part_Of then
- Error_Msg_N
+ SPARK_Msg_N
("indicator Part_Of must denote an abstract state",
Opt);
else
- Error_Msg_N
+ SPARK_Msg_N
("simple option not allowed in state declaration",
Opt);
end if;
@@ -10699,19 +10608,21 @@
Analyze_Part_Of_Option (Opt);
else
- Error_Msg_N ("invalid state option", Opt);
+ SPARK_Msg_N ("invalid state option", Opt);
end if;
else
- Error_Msg_N ("invalid state option", Opt);
+ SPARK_Msg_N ("invalid state option", Opt);
end if;
Next (Opt);
end loop;
- -- Any other attempt to declare a state is illegal
+ -- Any other attempt to declare a state is illegal. This is a
+ -- syntax error, always report.
else
Error_Msg_N ("malformed abstract state declaration", State);
+ return;
end if;
-- Guard against a junk state. In such cases no entity is
@@ -10743,49 +10654,6 @@
end if;
end Analyze_Abstract_State;
- ------------------------------------
- -- Check_State_Declaration_Syntax --
- ------------------------------------
-
- procedure Check_State_Declaration_Syntax (State : Node_Id) is
- Decl : Node_Id;
-
- begin
- -- Null abstract state
-
- if Nkind (State) = N_Null then
- null;
-
- -- Single state
-
- elsif Nkind (State) = N_Identifier then
- null;
-
- -- State with various options
-
- elsif Nkind (State) = N_Extension_Aggregate then
- if Nkind (Ancestor_Part (State)) /= N_Identifier then
- Error_Msg_N
- ("state name must be an identifier",
- Ancestor_Part (State));
- end if;
-
- -- Multiple states
-
- elsif Nkind (State) = N_Aggregate
- and then Present (Expressions (State))
- then
- Decl := First (Expressions (State));
- while Present (Decl) loop
- Check_State_Declaration_Syntax (Decl);
- Next (Decl);
- end loop;
-
- else
- Error_Msg_N ("malformed abstract state", State);
- end if;
- end Check_State_Declaration_Syntax;
-
-- Local variables
Context : constant Node_Id := Parent (Parent (N));
@@ -10808,16 +10676,7 @@
return;
end if;
- State := Expression (Arg1);
-
- -- Verify the syntax of pragma Abstract_State when SPARK checks
- -- are suppressed. Semantic analysis is disabled in this mode.
-
- if SPARK_Mode = Off then
- Check_State_Declaration_Syntax (State);
- return;
- end if;
-
+ State := Expression (Arg1);
Pack_Id := Defining_Entity (Context);
-- Multiple non-null abstract states appear as an aggregate
@@ -17699,7 +17558,7 @@
-- indicator, but has no visible state.
if not Has_Item then
- Error_Msg_NE
+ SPARK_Msg_NE
("package instantiation & has Part_Of indicator but "
& "lacks visible state", Instance, Pack_Id);
end if;
@@ -17765,7 +17624,7 @@
if Nkind (Stmt) = N_Object_Declaration
and then Ekind (Defining_Entity (Stmt)) /= E_Variable
then
- Error_Msg_N ("indicator Part_Of must apply to a variable", N);
+ SPARK_Msg_N ("indicator Part_Of must apply to a variable", N);
return;
end if;
@@ -22135,12 +21994,12 @@
-- a matching clause, emit an error.
else
- Error_Msg_NE
+ SPARK_Msg_NE
("dependence clause of subprogram & has no matching refinement "
& "in body", Ref_Clause, Spec_Id);
if Has_Refined_State then
- Error_Msg_N
+ SPARK_Msg_N
("\check the use of constituents in dependence refinement",
Ref_Clause);
end if;
@@ -22166,7 +22025,7 @@
procedure Match_Error (Msg : String; N : Node_Id) is
begin
if Post_Errors then
- Error_Msg_N (Msg, N);
+ SPARK_Msg_N (Msg, N);
end if;
end Match_Error;
@@ -22400,7 +22259,7 @@
if Present (Ref_Inputs) and then Post_Errors then
Input := First (Ref_Inputs);
while Present (Input) loop
- Error_Msg_N
+ SPARK_Msg_N
("unmatched or extra input in refinement clause", Input);
Next (Input);
@@ -22575,7 +22434,7 @@
if Nkind (Clause) /= N_Component_Association
or else Nkind (Expression (Clause)) /= N_Null
then
- Error_Msg_N
+ SPARK_Msg_N
("unmatched or extra clause in dependence refinement",
Clause);
end if;
@@ -22597,14 +22456,6 @@
-- Start of processing for Analyze_Refined_Depends_In_Decl_Part
begin
- -- Verify the syntax of pragma Refined_Depends when SPARK checks are
- -- suppressed. Semantic analysis is disabled in this mode.
-
- if SPARK_Mode = Off then
- Check_Dependence_List_Syntax (Refs);
- return;
- end if;
-
if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
else
@@ -22617,7 +22468,7 @@
-- rendered useless as there is nothing to refine (SPARK RM 7.2.5(2)).
if No (Depends) then
- Error_Msg_NE
+ SPARK_Msg_NE
("useless refinement, declaration of subprogram & lacks aspect or "
& "pragma Depends", N, Spec_Id);
return;
@@ -22631,7 +22482,7 @@
-- (SPARK RM 7.2.5(2)).
if Nkind (Deps) = N_Null then
- Error_Msg_NE
+ SPARK_Msg_NE
("useless refinement, subprogram & does not depend on abstract "
& "state with visible refinement",
N, Spec_Id);
@@ -22821,7 +22672,7 @@
elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then
Error_Msg_Name_1 := Chars (State_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("constituent & of state % must have mode Input, In_Out "
& "or Output in global refinement",
N, Constit_Id);
@@ -22851,7 +22702,7 @@
null;
else
- Error_Msg_NE
+ SPARK_Msg_NE
("global refinement of state & redefines the mode of its "
& "constituents", N, State_Id);
end if;
@@ -22924,7 +22775,7 @@
or else Present_Then_Remove (Proof_In_Constits, Constit_Id)
then
Error_Msg_Name_1 := Chars (State_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("constituent & of state % must have mode Input in global "
& "refinement", N, Constit_Id);
end if;
@@ -22935,7 +22786,7 @@
-- Not one of the constituents appeared as Input
if not In_Seen then
- Error_Msg_NE
+ SPARK_Msg_NE
("global refinement of state & must include at least one "
& "constituent of mode Input", N, State_Id);
end if;
@@ -23006,7 +22857,7 @@
or else Present_Then_Remove (Proof_In_Constits, Constit_Id)
then
Error_Msg_Name_1 := Chars (State_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("constituent & of state % must have mode Output in "
& "global refinement", N, Constit_Id);
@@ -23015,12 +22866,12 @@
else
if not Posted then
Posted := True;
- Error_Msg_NE
+ SPARK_Msg_NE
("output state & must be replaced by all its "
& "constituents in global refinement", N, State_Id);
end if;
- Error_Msg_NE
+ SPARK_Msg_NE
("\constituent & is missing in output list",
N, Constit_Id);
end if;
@@ -23096,7 +22947,7 @@
or else Present_Then_Remove (Out_Constits, Constit_Id)
then
Error_Msg_Name_1 := Chars (State_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("constituent & of state % must have mode Proof_In in "
& "global refinement", N, Constit_Id);
end if;
@@ -23107,7 +22958,7 @@
-- Not one of the constituents appeared as Proof_In
if not Proof_In_Seen then
- Error_Msg_NE
+ SPARK_Msg_NE
("global refinement of state & must include at least one "
& "constituent of mode Proof_In", N, State_Id);
end if;
@@ -23177,12 +23028,12 @@
procedure Inconsistent_Mode_Error (Expect : Name_Id) is
begin
- Error_Msg_NE
+ SPARK_Msg_NE
("global item & has inconsistent modes", Item, Item_Id);
Error_Msg_Name_1 := Global_Mode;
Error_Msg_Name_2 := Expect;
- Error_Msg_N ("\expected mode %, found mode %", Item);
+ SPARK_Msg_N ("\expected mode %, found mode %", Item);
end Inconsistent_Mode_Error;
-- Start of processing for Check_Refined_Global_Item
@@ -23233,7 +23084,7 @@
-- it must be an extra (SPARK RM 7.2.4(3)).
else
- Error_Msg_NE ("extra global item &", Item, Item_Id);
+ SPARK_Msg_NE ("extra global item &", Item, Item_Id);
end if;
end Check_Refined_Global_Item;
@@ -23342,7 +23193,7 @@
if Present (List) then
Constit_Elmt := First_Elmt (List);
while Present (Constit_Elmt) loop
- Error_Msg_NE ("extra constituent &", N, Node (Constit_Elmt));
+ SPARK_Msg_NE ("extra constituent &", N, Node (Constit_Elmt));
Next_Elmt (Constit_Elmt);
end loop;
end if;
@@ -23368,14 +23219,6 @@
-- Start of processing for Analyze_Refined_Global_In_Decl_Part
begin
- -- Verify the syntax of pragma Refined_Global when SPARK checks are
- -- suppressed. Semantic analysis is disabled in this mode.
-
- if SPARK_Mode = Off then
- Check_Global_List_Syntax (Items);
- return;
- end if;
-
if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
else
@@ -23388,7 +23231,7 @@
-- Refined_Global useless as there is nothing to refine.
if No (Global) then
- Error_Msg_NE
+ SPARK_Msg_NE
("useless refinement, declaration of subprogram & lacks aspect or "
& "pragma Global", N, Spec_Id);
return;
@@ -23418,7 +23261,7 @@
and then not Has_Proof_In_State
and then not Has_Null_State
then
- Error_Msg_NE
+ SPARK_Msg_NE
("useless refinement, subprogram & does not depend on abstract "
& "state with visible refinement", N, Spec_Id);
return;
@@ -23436,7 +23279,7 @@
or else Present (Proof_In_Items))
and then not Has_Null_State
then
- Error_Msg_NE
+ SPARK_Msg_NE
("refinement cannot be null, subprogram & has global items",
N, Spec_Id);
return;
@@ -23522,9 +23365,6 @@
procedure Analyze_Refinement_Clause (Clause : Node_Id);
-- Perform full analysis of a single refinement clause
- procedure Check_Refinement_List_Syntax (List : Node_Id);
- -- Verify the syntax of refinement clause list List
-
function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id;
-- Gather the entities of all abstract states and variables declared in
-- the body state space of package Pack_Id.
@@ -23664,7 +23504,7 @@
-- Detect a duplicate use of a constituent
if Contains (Constituents_Seen, Constit_Id) then
- Error_Msg_NE
+ SPARK_Msg_NE
("duplicate use of constituent &", Constit, Constit_Id);
return;
end if;
@@ -23681,10 +23521,10 @@
else
Error_Msg_Name_1 := Chars (State_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("& cannot act as constituent of state %",
Constit, Constit_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("\Part_Of indicator specifies & as encapsulating "
& "state", Constit, Encapsulating_State (Constit_Id));
end if;
@@ -23715,7 +23555,7 @@
-- refinement (SPARK RM 7.2.2(9)).
Error_Msg_Name_1 := Chars (Spec_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("cannot use & in refinement, constituent is not a hidden "
& "state of package %", Constit, Constit_Id);
end if;
@@ -23733,11 +23573,11 @@
if Nkind (Constit) = N_Null then
if Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("multiple null constituents not allowed", Constit);
elsif Non_Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix null and non-null constituents", Constit);
else
@@ -23760,7 +23600,7 @@
Non_Null_Seen := True;
if Null_Seen then
- Error_Msg_N
+ SPARK_Msg_N
("cannot mix null and non-null constituents", Constit);
end if;
@@ -23777,7 +23617,7 @@
Check_Matching_Constituent (Constit_Id);
else
- Error_Msg_NE
+ SPARK_Msg_NE
("constituent & must denote a variable or state (SPARK "
& "RM 7.2.2(5))", Constit, Constit_Id);
end if;
@@ -23785,7 +23625,7 @@
-- The constituent is illegal
else
- Error_Msg_N ("malformed constituent", Constit);
+ SPARK_Msg_N ("malformed constituent", Constit);
end if;
end if;
end Analyze_Constituent;
@@ -23807,7 +23647,7 @@
if Enabled then
if No (Constit) then
- Error_Msg_NE
+ SPARK_Msg_NE
("external state & requires at least one constituent with "
& "property %", State, State_Id);
end if;
@@ -23818,7 +23658,7 @@
elsif Present (Constit) then
Error_Msg_Name_2 := Chars (Constit);
- Error_Msg_NE
+ SPARK_Msg_NE
("external state & lacks property % set by constituent %",
State, State_Id);
end if;
@@ -23835,7 +23675,7 @@
-- Detect a duplicate refinement of a state (SPARK RM 7.2.2(8))
if Contains (Refined_States_Seen, State_Id) then
- Error_Msg_NE
+ SPARK_Msg_NE
("duplicate refinement of state &", State, State_Id);
return;
end if;
@@ -23865,7 +23705,7 @@
-- the package declaration.
Error_Msg_Name_1 := Chars (Spec_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("cannot refine state, & is not defined in package %",
State, State_Id);
end Check_Matching_State;
@@ -23893,7 +23733,7 @@
if not Posted then
Posted := True;
- Error_Msg_NE
+ SPARK_Msg_NE
("state & has unused Part_Of constituents",
State, State_Id);
end if;
@@ -23901,10 +23741,10 @@
Error_Msg_Sloc := Sloc (Constit_Id);
if Ekind (Constit_Id) = E_Abstract_State then
- Error_Msg_NE
+ SPARK_Msg_NE
("\abstract state & defined #", State, Constit_Id);
else
- Error_Msg_NE
+ SPARK_Msg_NE
("\variable & defined #", State, Constit_Id);
end if;
@@ -23925,6 +23765,7 @@
begin
-- A refinement clause appears as a component association where the
-- sole choice is the state and the expressions are the constituents.
+ -- This is a syntax error, always report.
if Nkind (Clause) /= N_Component_Association then
Error_Msg_N ("malformed state refinement clause", Clause);
@@ -23950,7 +23791,7 @@
if Ekind (State_Id) = E_Abstract_State then
Check_Matching_State;
else
- Error_Msg_NE
+ SPARK_Msg_NE
("& must denote an abstract state", State, State_Id);
return;
end if;
@@ -23967,15 +23808,15 @@
while Present (Body_Ref_Elmt) loop
Body_Ref := Node (Body_Ref_Elmt);
- Error_Msg_N ("reference to & not allowed", Body_Ref);
+ SPARK_Msg_N ("reference to & not allowed", Body_Ref);
Error_Msg_Sloc := Sloc (State);
- Error_Msg_N ("\refinement of & is visible#", Body_Ref);
+ SPARK_Msg_N ("\refinement of & is visible#", Body_Ref);
Next_Elmt (Body_Ref_Elmt);
end loop;
end if;
- -- The state name is illegal
+ -- The state name is illegal. This is a syntax error, always report.
else
Error_Msg_N ("malformed state name in refinement clause", State);
@@ -23987,7 +23828,7 @@
Extra_State := Next (State);
if Present (Extra_State) then
- Error_Msg_N
+ SPARK_Msg_N
("refinement clause cannot cover multiple states", Extra_State);
end if;
@@ -24003,7 +23844,7 @@
if Nkind (Constit) = N_Aggregate then
if Present (Component_Associations (Constit)) then
- Error_Msg_N
+ SPARK_Msg_N
("constituents of refinement clause must appear in "
& "positional form", Constit);
@@ -24062,7 +23903,7 @@
-- external (SPARK RM 7.2.8(2)).
else
- Error_Msg_NE
+ SPARK_Msg_NE
("external state & requires at least one external "
& "constituent or null refinement", State, State_Id);
end if;
@@ -24071,7 +23912,7 @@
-- constituents (SPARK RM 7.2.8(1)).
elsif External_Constit_Seen then
- Error_Msg_NE
+ SPARK_Msg_NE
("non-external state & cannot contain external constituents in "
& "refinement", State, State_Id);
end if;
@@ -24082,70 +23923,6 @@
Report_Unused_Constituents (Part_Of_Constits);
end Analyze_Refinement_Clause;
- ----------------------------------
- -- Check_Refinement_List_Syntax --
- ----------------------------------
-
- procedure Check_Refinement_List_Syntax (List : Node_Id) is
- procedure Check_Clause_Syntax (Clause : Node_Id);
- -- Verify the syntax of state refinement clause Clause
-
- -------------------------
- -- Check_Clause_Syntax --
- -------------------------
-
- procedure Check_Clause_Syntax (Clause : Node_Id) is
- Constits : constant Node_Id := Expression (Clause);
- Constit : Node_Id;
-
- begin
- -- State to be refined
-
- Check_Item_Syntax (First (Choices (Clause)));
-
- -- Multiple constituents
-
- if Nkind (Constits) = N_Aggregate
- and then Present (Expressions (Constits))
- then
- Constit := First (Expressions (Constits));
- while Present (Constit) loop
- Check_Item_Syntax (Constit);
- Next (Constit);
- end loop;
-
- -- Single constituent
-
- else
- Check_Item_Syntax (Constits);
- end if;
- end Check_Clause_Syntax;
-
- -- Local variables
-
- Clause : Node_Id;
-
- -- Start of processing for Check_Refinement_List_Syntax
-
- begin
- -- Multiple state refinement clauses
-
- if Nkind (List) = N_Aggregate
- and then Present (Component_Associations (List))
- then
- Clause := First (Component_Associations (List));
- while Present (Clause) loop
- Check_Clause_Syntax (Clause);
- Next (Clause);
- end loop;
-
- -- Single state refinement clause
-
- else
- Check_Clause_Syntax (List);
- end if;
- end Check_Refinement_List_Syntax;
-
-------------------------
-- Collect_Body_States --
-------------------------
@@ -24246,7 +24023,7 @@
if Present (States) then
State_Elmt := First_Elmt (States);
while Present (State_Elmt) loop
- Error_Msg_N
+ SPARK_Msg_N
("abstract state & must be refined", Node (State_Elmt));
Next_Elmt (State_Elmt);
@@ -24277,17 +24054,17 @@
if not Posted then
Posted := True;
- Error_Msg_N
+ SPARK_Msg_N
("body of package & has unused hidden states", Body_Id);
end if;
Error_Msg_Sloc := Sloc (State_Id);
if Ekind (State_Id) = E_Abstract_State then
- Error_Msg_NE
+ SPARK_Msg_NE
("\abstract state & defined #", Body_Id, State_Id);
else
- Error_Msg_NE
+ SPARK_Msg_NE
("\variable & defined #", Body_Id, State_Id);
end if;
@@ -24308,14 +24085,6 @@
begin
Set_Analyzed (N);
- -- Verify the syntax of pragma Refined_State when SPARK checks are
- -- suppressed. Semantic analysis is disabled in this mode.
-
- if SPARK_Mode = Off then
- Check_Refinement_List_Syntax (Clauses);
- return;
- end if;
-
Body_Id := Defining_Entity (Body_Decl);
Spec_Id := Corresponding_Spec (Body_Decl);
@@ -24334,7 +24103,7 @@
if Nkind (Clauses) = N_Aggregate then
if Present (Expressions (Clauses)) then
- Error_Msg_N
+ SPARK_Msg_N
("state refinements must appear as component associations",
Clauses);
@@ -24500,110 +24269,6 @@
end if;
end Check_Applicable_Policy;
- ----------------------------------
- -- Check_Dependence_List_Syntax --
- ----------------------------------
-
- procedure Check_Dependence_List_Syntax (List : Node_Id) is
- procedure Check_Clause_Syntax (Clause : Node_Id);
- -- Verify the syntax of a dependency clause Clause
-
- -------------------------
- -- Check_Clause_Syntax --
- -------------------------
-
- procedure Check_Clause_Syntax (Clause : Node_Id) is
- Input : Node_Id;
- Inputs : Node_Id;
- Output : Node_Id;
- Outputs : Node_Id;
-
- begin
- -- Output items
-
- Outputs := First (Choices (Clause));
- while Present (Outputs) loop
-
- -- Multiple output items
-
- if Nkind (Outputs) = N_Aggregate then
- Output := First (Expressions (Outputs));
- while Present (Output) loop
- Check_Item_Syntax (Output);
- Next (Output);
- end loop;
-
- -- Single output item
-
- else
- Check_Item_Syntax (Outputs);
- end if;
-
- Next (Outputs);
- end loop;
-
- Inputs := Expression (Clause);
-
- -- A self-dependency appears as operator "+"
-
- if Nkind (Inputs) = N_Op_Plus then
- Inputs := Right_Opnd (Inputs);
- end if;
-
- -- Input items
-
- if Nkind (Inputs) = N_Aggregate then
- if Present (Expressions (Inputs)) then
- Input := First (Expressions (Inputs));
- while Present (Input) loop
- Check_Item_Syntax (Input);
- Next (Input);
- end loop;
-
- else
- Error_Msg_N ("malformed input dependency list", Inputs);
- end if;
-
- -- Single input item
-
- else
- Check_Item_Syntax (Inputs);
- end if;
- end Check_Clause_Syntax;
-
- -- Local variables
-
- Clause : Node_Id;
-
- -- Start of processing for Check_Dependence_List_Syntax
-
- begin
- -- Null dependency relation
-
- if Nkind (List) = N_Null then
- null;
-
- -- Verify the syntax of a single or multiple dependency clauses
-
- elsif Nkind (List) = N_Aggregate
- and then Present (Component_Associations (List))
- then
- Clause := First (Component_Associations (List));
- while Present (Clause) loop
- if Has_Extra_Parentheses (Clause) then
- null;
- else
- Check_Clause_Syntax (Clause);
- end if;
-
- Next (Clause);
- end loop;
-
- else
- Error_Msg_N ("malformed dependency relation", List);
- end if;
- end Check_Dependence_List_Syntax;
-
-------------------------------
-- Check_External_Properties --
-------------------------------
@@ -24649,97 +24314,12 @@
null;
else
- Error_Msg_N
+ SPARK_Msg_N
("illegal combination of external properties (SPARK RM 7.1.2(6))",
Item);
end if;
end Check_External_Properties;
- ------------------------------
- -- Check_Global_List_Syntax --
- ------------------------------
-
- procedure Check_Global_List_Syntax (List : Node_Id) is
- Assoc : Node_Id;
- Item : Node_Id;
-
- begin
- -- Null global list
-
- if Nkind (List) = N_Null then
- null;
-
- -- Single global item
-
- elsif Nkind_In (List, N_Expanded_Name,
- N_Identifier,
- N_Selected_Component)
- then
- null;
-
- elsif Nkind (List) = N_Aggregate then
-
- -- Items in a simple global list
-
- if Present (Expressions (List)) then
- Item := First (Expressions (List));
- while Present (Item) loop
- Check_Item_Syntax (Item);
- Next (Item);
- end loop;
-
- -- Items in a moded global list
-
- elsif Present (Component_Associations (List)) then
- Assoc := First (Component_Associations (List));
- while Present (Assoc) loop
- Check_Item_Syntax (First (Choices (Assoc)));
- Check_Global_List_Syntax (Expression (Assoc));
-
- Next (Assoc);
- end loop;
- end if;
-
- -- Anything else is an error
-
- else
- Error_Msg_N ("malformed global list", List);
- end if;
- end Check_Global_List_Syntax;
-
- -----------------------
- -- Check_Item_Syntax --
- -----------------------
-
- procedure Check_Item_Syntax (Item : Node_Id) is
- begin
- -- Null can appear in various annotation lists to denote a missing or
- -- optional relation.
-
- if Nkind (Item) = N_Null then
- null;
-
- -- Formal parameter, state or variable nodes
-
- elsif Nkind_In (Item, N_Expanded_Name,
- N_Identifier,
- N_Selected_Component)
- then
- null;
-
- -- Attribute 'Result can appear in annotations to denote the outcome of
- -- a function call.
-
- elsif Is_Attribute_Result (Item) then
- null;
-
- -- Any other node cannot possibly denote a legal SPARK item
-
- else
- Error_Msg_N ("malformed item", Item);
- end if;
- end Check_Item_Syntax;
-
----------------
-- Check_Kind --
----------------
@@ -24853,10 +24433,17 @@
-- Start of processing for Check_Missing_Part_Of
begin
+ -- Do not consider abstract states, variables or package instantiations
+ -- coming from an instance as those always inherit the Part_Of indicator
+ -- of the instance itself.
+
+ if In_Instance then
+ return;
+
-- Do not consider internally generated entities as these can never
-- have a Part_Of indicator.
- if not Comes_From_Source (Item_Id) then
+ elsif not Comes_From_Source (Item_Id) then
return;
-- Perform these checks only when SPARK_Mode is enabled as they will
@@ -25059,7 +24646,7 @@
if Present (State_Id) then
Error_Msg_Name_1 := Chars (Constit_Id);
- Error_Msg_NE
+ SPARK_Msg_NE
("cannot mention state & and its constituent % in the same "
& "context", Context, State_Id);
exit;
@@ -25199,10 +24786,12 @@
raise Program_Error;
end if;
- -- Invalid list
+ -- To accomodate partial decoration of disabled SPARK features, this
+ -- routine may be called with illegal input. If this is the case, do
+ -- not raise Program_Error.
else
- raise Program_Error;
+ null;
end if;
end Process_Global_List;
@@ -25305,10 +24894,12 @@
end loop;
end if;
- -- Invalid list
+ -- To accomodate partial decoration of disabled SPARK features, this
+ -- routine may be called with illegal input. If this is the case, do
+ -- not raise Program_Error.
else
- raise Program_Error;
+ null;
end if;
end Collect_Global_List;
@@ -25616,13 +25207,13 @@
if Nkind (Expr) = N_Aggregate
and then Present (Component_Associations (Expr))
then
- Error_Msg_N
+ SPARK_Msg_N
("dependency clause contains extra parentheses", Expr);
-- Otherwise the expression is a malformed construct
else
- Error_Msg_N ("malformed dependency clause", Expr);
+ SPARK_Msg_N ("malformed dependency clause", Expr);
end if;
Next (Expr);
This patch modifies the analysis machinery to allow for the quiet analysis of SPARK features that have been disabled by setting SPARK_Mode to "off". Syntax errors are always reported regardless of what SPARK_Mode is set to. ------------ -- Source -- ------------ -- disabled_features.ads package Disabled_Features with SPARK_Mode => Off, Abstract_State => State is Var_1 : Integer := 1; procedure Illegal_Disabled (Formal : Integer) with Global => (Input => ("junk", -- always reported, syntax error Formal, -- illegal, but not reported Var_1, -- ok Var_2)); -- always reported, can't be disabled private Var_2 : Integer := 2 with Part_Of => State; end Disabled_Features; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c disabled_features.ads disabled_features.ads:9:24: global item must denote variable or state disabled_features.ads:12:24: "Var_2" is undefined Tested on x86_64-pc-linux-gnu, committed on trunk 2014-06-13 Hristian Kirtchev <kirtchev@adacore.com> * errout.adb (SPARK_Msg_N): New routine. (SPARK_Msg_NE): New routine. * errout.ads Add a section on SPARK-related error routines. (SPARK_Msg_N): New routine. (SPARK_Msg_NE): New routine. * sem_ch13.adb (Analyze_Aspect_Specifications): Ensure that pragma Abstract_State is always inserted after SPARK_Mode. (Insert_After_SPARK_Mode): New routine. * sem_prag.adb (Analyze_Abstract_State, Analyze_Constituent, Analyze_External_Property, Analyze_External_Property_In_Decl_Part, Analyze_Global_Item, Analyze_Global_List, Analyze_Initialization_Item, Analyze_Initialization_Item_With_Inputs, Analyze_Input_Item, Analyze_Input_List, Analyze_Input_Output, Analyze_Part_Of, Analyze_Pragma, Analyze_Refined_Depends_In_Decl_Part, Analyze_Refined_Global_In_Decl_Part, Analyze_Refined_State_In_Decl_Part, Analyze_Refinement_Clause, Check_Aspect_Specification_Order, Check_Constituent_Usage, Check_Declaration_Order, Check_Dependency_Clause, Check_Duplicate_Mode, Check_Duplicate_Option, Check_Duplicate_Property, Check_External_Properties, Check_External_Property, Check_Function_Return, Check_Matching_Constituent, Check_Matching_State, Check_Mode_Restriction_In_Enclosing_Context, Check_Mode_Restriction_In_Function, Check_Refined_Global_Item, Check_State_And_Constituent_Use, Create_Or_Modify_Clause, Has_Extra_Parentheses, Inconsistent_Mode_Error, Match_Error, Propagate_Part_Of, Report_Extra_Clauses, Report_Extra_Constituents_In_List, Report_Extra_Inputs, Report_Unrefined_States, Report_Unused_Constituents, Report_Unused_States, Role_Error, Usage_Error): Convert Error_Msg_XXX calls to SPARK_Msg_XXX calls to report semantic errors only when SPARK_Mode is on. (Analyze_Depends_In_Decl_Part): Do not check the syntax of pragma Depends explicitly, this is now done by the analysis. (Analyze_Global_In_Decl_List): Do not check the syntax of pragma Global explicitly, this is now done by the analysis. (Analyze_Initializes_In_Decl_Part): Do not check the syntax of pragma Initializes explicitly, this is now done by the analysis. (Analyze_Part_Of): Do not check the syntax of the encapsulating state, this is now done by the analysis. (Analyze_Pragma): Do not check the syntax of a state declaration, this is now done by the analysis. (Analyze_Refined_Depends_In_Decl_Part): Do not check the syntax of pragma Refined_Depends explicitly, this is now done by the analysis. (Analyze_Refined_Global_In_Decl_Part): Do not check the syntax of pragma Refined_Global explicitly, this is now done by the analysis. (Analyze_Refined_State_In_Decl_Part): Do not check the syntax of pragma Refined_State explicitly, this is now done by the analysis. (Check_Dependence_List_Syntax): Removed. (Check_Global_List_Syntax): Removed. (Check_Initialization_List_Syntax): Removed. (Check_Item_Syntax): Removed. (Check_Missing_Part_Of): Do not consider items from an instance. (Check_Refinement_List_Syntax): Removed. (Check_State_Declaration_Syntax): Removed. (Collect_Global_List): Do not raise Program_Error when the input is malformed. (Process_Global_List): Do not raise Program_Error when the input is malformed. * sem_ch13.adb: Minor reformatting.