diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-06-13 12:23:05 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-06-13 12:23:05 +0200 |
| commit | d2adb45e357e4416bca760e3c98fba735e99393e (patch) | |
| tree | 93f40ade93fdafebba80ead301dbccf38c7846cc /gcc/ada | |
| parent | 6aa4c5b68dbf3723a24d831f1340c91327211e5f (diff) | |
| download | gcc-d2adb45e357e4416bca760e3c98fba735e99393e.zip gcc-d2adb45e357e4416bca760e3c98fba735e99393e.tar.gz gcc-d2adb45e357e4416bca760e3c98fba735e99393e.tar.bz2 | |
[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
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 76 | ||||
| -rw-r--r-- | gcc/ada/errout.adb | 26 | ||||
| -rw-r--r-- | gcc/ada/errout.ads | 23 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 58 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/sem_ch9.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 795 |
7 files changed, 377 insertions, 615 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 5023f97..1760db5 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,79 @@ +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 diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index 0eb997a..3a037a4 100644 --- a/gcc/ada/errout.adb +++ b/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 -- -------------------------- diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads index d7bc700..a6b7a2b 100644 --- a/gcc/ada/errout.ads +++ b/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 -- ------------------------------------ diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 47bdff0..149826f 100644 --- a/gcc/ada/sem_ch13.adb +++ b/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 diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index f9ccf5b..b899e01 100644 --- a/gcc/ada/sem_ch3.adb +++ b/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); diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 4894a64..be46427 100644 --- a/gcc/ada/sem_ch9.adb +++ b/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); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 279c733..8aad039 100644 --- a/gcc/ada/sem_prag.adb +++ b/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); |