Skip to content

R
riscv-gcc-1
Commit d2adb45e by Arnaud Charlet
Options

[multiple changes] 

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.
2014-06-13  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch3.adb (Find_Type_Name): Diagnose a private type completion
	that is an interface definition with an interface list.
	(Process_Full_View): Move error message on missmatched interfaces
	between views to the declaration of full view, for clarity.
	* sem_ch9.adb (Check_Interfaces): Move error message to full view,
	for clarity.

From-SVN: r211626
parent 6aa4c5b6
Showing with 377 additions and 615 deletions
gcc/ada/ChangeLog
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.
2014-06-13 Ed Schonberg <schonberg@adacore.com>
* sem_ch3.adb (Find_Type_Name): Diagnose a private type completion
that is an interface definition with an interface list.
(Process_Full_View): Move error message on missmatched interfaces
between views to the declaration of full view, for clarity.
* sem_ch9.adb (Check_Interfaces): Move error message to full view,
for clarity.
2014-06-13 Robert Dewar <dewar@adacore.com>
* exp_attr.adb (Expand_N_Attribute_Reference, case Pred/Succ): Change
......
gcc/ada/errout.adb
......@@ -3065,6 +3065,32 @@ package body Errout is
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 --
--------------------------
......
gcc/ada/errout.ads
......@@ -909,6 +909,29 @@ package Errout is
-- 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 --
------------------------------------
......
gcc/ada/sem_ch13.adb
......@@ -2007,10 +2007,51 @@ package body Sem_Ch13 is
-- 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 @@ package body Sem_Ch13 is
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
......
gcc/ada/sem_ch3.adb
......@@ -15599,8 +15599,10 @@ package body Sem_Ch3 is
elsif Nkind (N) = N_Full_Type_Declaration
and then
Nkind (Type_Definition (N)) = N_Record_Definition
and then Interface_Present (Type_Definition (N))
(Nkind (Type_Definition (N)) = N_Record_Definition
or else Nkind (Type_Definition (N))
= N_Derived_Type_Definition)
and then Interface_Present (Type_Definition (N))
then
Error_Msg_N
("completion of private type cannot be an interface", N);
......@@ -18307,8 +18309,8 @@ package body Sem_Ch3 is
if Present (Iface) then
Error_Msg_NE
("interface & not implemented by full type " &
"(RM-2005 7.3 (7.3/2))", Priv_T, Iface);
("interface in partial view& not implemented by full type " &
"(RM-2005 7.3 (7.3/2))", Full_T, Iface);
end if;
Iface := Find_Hidden_Interface (Full_T_Ifaces, Priv_T_Ifaces);
......
gcc/ada/sem_ch9.adb
......@@ -3327,8 +3327,8 @@ package body Sem_Ch9 is
if Present (Iface) then
Error_Msg_NE
("interface & not implemented by full type " &
"(RM-2005 7.3 (7.3/2))", Priv_T, Iface);
("interface in partial view& not implemented by full "
& "type (RM-2005 7.3 (7.3/2))", T, Iface);
end if;
Iface := Find_Hidden_Interface (Full_T_Ifaces, Priv_T_Ifaces);
......
gcc/ada/sem_prag.adb
......@@ -184,19 +184,6 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
Next (Input);
end loop;
-- Syntax error, always report
else
Error_Msg_N ("malformed input dependency list", Inputs);
end if;
......@@ -714,7 +703,7 @@ package body Sem_Prag is
-- (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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
Next (Grouped);
end loop;
-- Syntax error, always report
else
Error_Msg_N ("malformed dependency list", Item);
end if;
......@@ -787,7 +778,7 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- (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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
(" & 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
(" & 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 @@ package body Sem_Prag is
(" & 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- (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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- (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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- (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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- (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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- (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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- (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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment