===================================================================
@@ -399,7 +399,8 @@
if Present (Extra_Guard) then
Error_Msg_N
- ("contract case may have only one case guard", Extra_Guard);
+ ("contract case must have exactly one case guard",
+ Extra_Guard);
end if;
-- Check the placement of "others" (if available)
@@ -407,7 +408,7 @@
if Nkind (Case_Guard) = N_Others_Choice then
if Others_Seen then
Error_Msg_N
- ("only one others choice allowed in aspect Contract_Cases "
+ ("only one others choice allowed in contract cases "
& "(SPARK RM 6.1.3(1))", Case_Guard);
else
Others_Seen := True;
@@ -415,7 +416,7 @@
elsif Others_Seen then
Error_Msg_N
- ("others must be the last choice in aspect Contract_Cases "
+ ("others must be the last choice in contract cases "
& "(SPARK RM 6.1.3(1))", N);
end if;
@@ -460,7 +461,7 @@
pragma Assert (Nkind (All_Cases) = N_Aggregate);
if No (Component_Associations (All_Cases)) then
- Error_Msg_N ("wrong syntax for aspect Contract_Cases", N);
+ Error_Msg_N ("wrong syntax for constract cases", N);
-- Individual contract cases appear as component associations
@@ -536,6 +537,15 @@
-- Two lists containing the full set of inputs and output of the related
-- subprograms. Note that these lists contain both nodes and entities.
+ procedure Add_Item_To_Name_Buffer (Item_Id : Entity_Id);
+ -- Subsidiary routine to Check_Role and Check_Usage. Add the item kind
+ -- to the name buffer. The individual kinds are as follows:
+ -- E_Abstract_State - "state"
+ -- E_In_Parameter - "parameter"
+ -- E_In_Out_Parameter - "parameter"
+ -- E_Out_Parameter - "parameter"
+ -- E_Variable - "global"
+
procedure Analyze_Dependency_Clause
(Clause : Node_Id;
Is_Last : Boolean);
@@ -545,16 +555,17 @@
procedure Check_Function_Return;
-- Verify that Funtion'Result appears as one of the outputs
- procedure Check_Mode
+ procedure Check_Role
(Item : Node_Id;
Item_Id : Entity_Id;
Is_Input : Boolean;
Self_Ref : Boolean);
- -- Ensure that an item has a proper IN, IN OUT, or OUT mode depending
- -- on its function. If this is not the case, emit an error. Item and
- -- Item_Id denote the attributes of an item. Flag Is_Input should be set
- -- when item comes from an input list. Flag Self_Ref should be set when
- -- the item is an output and the dependency clause has operator "+".
+ -- Ensure that an item fulfils its designated input and/or output role
+ -- as specified by pragma Global (if any) or the enclosing context. If
+ -- this is not the case, emit an error. Item and Item_Id denote the
+ -- attributes of an item. Flag Is_Input should be set when item comes
+ -- from an input list. Flag Self_Ref should be set when the item is an
+ -- output and the dependency clause has operator "+".
procedure Check_Usage
(Subp_Items : Elist_Id;
@@ -568,6 +579,28 @@
-- a clause with multiple outputs into multiple clauses with a single
-- output.
+ -----------------------------
+ -- Add_Item_To_Name_Buffer --
+ -----------------------------
+
+ procedure Add_Item_To_Name_Buffer (Item_Id : Entity_Id) is
+ begin
+ if Ekind (Item_Id) = E_Abstract_State then
+ Add_Str_To_Name_Buffer ("state");
+
+ elsif Is_Formal (Item_Id) then
+ Add_Str_To_Name_Buffer ("parameter");
+
+ elsif Ekind (Item_Id) = E_Variable then
+ Add_Str_To_Name_Buffer ("global");
+
+ -- The routine should not be called with non-SPARK items
+
+ else
+ raise Program_Error;
+ end if;
+ end Add_Item_To_Name_Buffer;
+
-------------------------------
-- Analyze_Dependency_Clause --
-------------------------------
@@ -807,17 +840,19 @@
E_Out_Parameter,
E_Variable)
then
- -- Ensure that the item is of the correct mode depending
- -- on its function.
+ -- Ensure that the item fulfils its role as input and/or
+ -- output as specified by pragma Global or the enclosing
+ -- context.
- Check_Mode (Item, Item_Id, Is_Input, Self_Ref);
+ Check_Role (Item, Item_Id, Is_Input, Self_Ref);
-- Detect multiple uses of the same state, variable or
-- formal parameter. If this is not the case, add the
-- item to the list of processed relations.
if Contains (Seen, Item_Id) then
- Error_Msg_N ("duplicate use of item", Item);
+ Error_Msg_NE
+ ("duplicate use of item &", Item, Item_Id);
else
Add_Item (Item_Id, Seen);
end if;
@@ -831,8 +866,9 @@
and then Contains (All_Inputs_Seen, Item_Id)
then
Error_Msg_N
- ("input of a null output list appears in multiple "
- & "input lists (SPARK RM 6.1.5(13))", Item);
+ ("input of a null output list cannot appear in "
+ & "multiple input lists (SPARK RM 6.1.5(13))",
+ Item);
end if;
-- Add an input or a self-referential output to the list
@@ -850,7 +886,7 @@
("cannot mention state & in global refinement",
Item, Item_Id);
Error_Msg_N
- ("\use its constituents instead "
+ ("\\use its constituents instead "
& "(SPARK RM 6.1.5(3))", Item);
return;
@@ -892,15 +928,15 @@
else
Error_Msg_N
- ("item must denote variable, state or formal "
- & "parameter (SPARK RM 6.1.5(1))", Item);
+ ("item must denote parameter, variable or state "
+ & "(SPARK RM 6.1.5(1))", Item);
end if;
-- All other input/output items are illegal
else
Error_Msg_N
- ("item must denote variable, state or formal parameter "
+ ("item must denote parameter, variable or state "
& "(SPARK RM 6.1.5(1))", Item);
end if;
end if;
@@ -964,36 +1000,39 @@
end Check_Function_Return;
----------------
- -- Check_Mode --
+ -- Check_Role --
----------------
- procedure Check_Mode
+ procedure Check_Role
(Item : Node_Id;
Item_Id : Entity_Id;
Is_Input : Boolean;
Self_Ref : Boolean)
is
- procedure Find_Mode
- (Is_Input : out Boolean;
- Is_Output : out Boolean;
- From_Global : out Boolean);
- -- Find the mode of Item_Id. Flags Is_Input and Is_Output are set
- -- depending on the mode. Flag From_Global is set when the mode is
- -- determined by pragma [Refined_]Global.
+ procedure Find_Role
+ (Item_Is_Input : out Boolean;
+ Item_Is_Output : out Boolean);
+ -- Find the input/output role of Item_Id. Flags Item_Is_Input and
+ -- Item_Is_Output are set depending on the role.
+ procedure Role_Error
+ (Item_Is_Input : Boolean;
+ Item_Is_Output : Boolean);
+ -- Emit an error message concerning the incorrect use of Item in
+ -- pragma [Refined_]Depends. Flags Item_Is_Input and Item_Is_Output
+ -- denote whether the item is an input and/or an output.
+
---------------
- -- Find_Mode --
+ -- Find_Role --
---------------
- procedure Find_Mode
- (Is_Input : out Boolean;
- Is_Output : out Boolean;
- From_Global : out Boolean)
+ procedure Find_Role
+ (Item_Is_Input : out Boolean;
+ Item_Is_Output : out Boolean)
is
begin
- Is_Input := False;
- Is_Output := False;
- From_Global := False;
+ Item_Is_Input := False;
+ Item_Is_Output := False;
-- Abstract state cases
@@ -1004,30 +1043,28 @@
if Global_Seen then
if Appears_In (Subp_Inputs, Item_Id) then
- Is_Input := True;
- From_Global := True;
+ Item_Is_Input := True;
end if;
if Appears_In (Subp_Outputs, Item_Id) then
- Is_Output := True;
- From_Global := True;
+ Item_Is_Output := True;
end if;
-- Otherwise the state has a default IN OUT mode
else
- Is_Input := True;
- Is_Output := True;
+ Item_Is_Input := True;
+ Item_Is_Output := True;
end if;
-- Parameter cases
elsif Ekind (Item_Id) = E_In_Parameter then
- Is_Input := True;
+ Item_Is_Input := True;
elsif Ekind (Item_Id) = E_In_Out_Parameter then
- Is_Input := True;
- Is_Output := True;
+ Item_Is_Input := True;
+ Item_Is_Output := True;
elsif Ekind (Item_Id) = E_Out_Parameter then
if Scope (Item_Id) = Spec_Id then
@@ -1037,17 +1074,17 @@
-- bounds, discriminants or tags can be read.
if Is_Unconstrained_Or_Tagged_Item (Item_Id) then
- Is_Input := True;
+ Item_Is_Input := True;
end if;
- Is_Output := True;
+ Item_Is_Output := True;
-- An OUT parameter of an enclosing subprogram behaves as a
-- read-write variable in which case the mode is IN OUT.
else
- Is_Input := True;
- Is_Output := True;
+ Item_Is_Input := True;
+ Item_Is_Output := True;
end if;
-- Variable cases
@@ -1066,73 +1103,120 @@
if Appears_In (Subp_Inputs, Item_Id)
or else Is_Unconstrained_Or_Tagged_Item (Item_Id)
then
- Is_Input := True;
- From_Global := True;
+ Item_Is_Input := True;
end if;
if Appears_In (Subp_Outputs, Item_Id) then
- Is_Output := True;
- From_Global := True;
+ Item_Is_Output := True;
end if;
-- Otherwise the variable has a default IN OUT mode
else
- Is_Input := True;
- Is_Output := True;
+ Item_Is_Input := True;
+ Item_Is_Output := True;
end if;
end if;
- end Find_Mode;
+ end Find_Role;
+ ----------------
+ -- Role_Error --
+ ----------------
+
+ procedure Role_Error
+ (Item_Is_Input : Boolean;
+ Item_Is_Output : Boolean)
+ is
+ Error_Msg : Name_Id;
+
+ begin
+ Name_Len := 0;
+
+ -- When the item is not part of the input and the output set of
+ -- the related subprogram, then it appears as extra in pragma
+ -- [Refined_]Depends.
+
+ if not Item_Is_Input and then not Item_Is_Output then
+ Add_Item_To_Name_Buffer (Item_Id);
+ Add_Str_To_Name_Buffer
+ (" & cannot appear in dependence relation");
+
+ Error_Msg := Name_Find;
+ Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+
+ Error_Msg_Name_1 := Chars (Subp_Id);
+ Error_Msg_NE
+ ("\\& is not part of the input or output set of subprogram %",
+ Item, Item_Id);
+
+ -- The mode of the item and its role in pragma [Refined_]Depends
+ -- are in conflict. Construct a detailed message explaining the
+ -- illegality.
+
+ else
+ if Item_Is_Input then
+ Add_Str_To_Name_Buffer ("read-only");
+ else
+ Add_Str_To_Name_Buffer ("write-only");
+ end if;
+
+ Add_Char_To_Name_Buffer (' ');
+ Add_Item_To_Name_Buffer (Item_Id);
+ Add_Str_To_Name_Buffer (" & cannot appear as ");
+
+ if Item_Is_Input then
+ Add_Str_To_Name_Buffer ("output");
+ else
+ Add_Str_To_Name_Buffer ("input");
+ end if;
+
+ Add_Str_To_Name_Buffer (" in dependence relation ");
+
+ -- Even though the two SPARK references differ by one character
+ -- they are fully written out to facilitate reference finding
+ -- and updating.
+
+ if Item_Is_Input then
+ Add_Str_To_Name_Buffer ("(SPARK RM 6.1.5(5))");
+ else
+ Add_Str_To_Name_Buffer ("(SPARK RM 6.1.5(6))");
+ end if;
+
+ Error_Msg := Name_Find;
+ Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+ end if;
+ end Role_Error;
+
-- Local variables
Item_Is_Input : Boolean;
Item_Is_Output : Boolean;
- From_Global : Boolean;
- -- Start of processing for Check_Mode
+ -- Start of processing for Check_Role
begin
- Find_Mode (Item_Is_Input, Item_Is_Output, From_Global);
+ Find_Role (Item_Is_Input, Item_Is_Output);
-- Input item
if Is_Input then
if not Item_Is_Input then
- if From_Global then
- Error_Msg_NE
- ("item & must have mode `IN` or `IN OUT`", Item, Item_Id);
- else
- Error_Msg_NE
- ("item & appears as extra in input list", Item, Item_Id);
- end if;
+ Role_Error (Item_Is_Input, Item_Is_Output);
end if;
-- Self-referential item
elsif Self_Ref then
if not Item_Is_Input or else not Item_Is_Output then
- if From_Global then
- Error_Msg_NE
- ("item & must have mode `IN OUT`", Item, Item_Id);
- else
- Error_Msg_NE
- ("item & appears as extra in In_Out list", Item, Item_Id);
- end if;
+ Role_Error (Item_Is_Input, Item_Is_Output);
end if;
-- Output item
elsif not Item_Is_Output then
- if From_Global then
- Error_Msg_NE
- ("item & must have mode `OUT` or `IN OUT`", Item, Item_Id);
- else
- Error_Msg_NE
- ("item & appears as extra in output list", Item, Item_Id);
- end if;
+ Role_Error (Item_Is_Input, Item_Is_Output);
end if;
- end Check_Mode;
+ end Check_Role;
-----------------
-- Check_Usage --
@@ -1151,46 +1235,52 @@
-----------------
procedure Usage_Error (Item : Node_Id; Item_Id : Entity_Id) is
- Typ : constant Entity_Id := Etype (Item_Id);
+ Typ : constant Entity_Id := Etype (Item_Id);
+ Error_Msg : Name_Id;
begin
+ Name_Len := 0;
+
-- Input case
if Is_Input then
- Error_Msg_NE
- ("item & must appear in at least one input dependence list "
- & "(SPARK RM 6.1.5(8))", Item, Item_Id);
+ Add_Item_To_Name_Buffer (Item_Id);
+ Add_Str_To_Name_Buffer
+ (" & must appear in at least one input dependence list "
+ & "(SPARK RM 6.1.5(8))");
- -- Refine the error message for unconstrained OUT parameters
- -- by giving the reason for the illegality.
+ Error_Msg := Name_Find;
+ Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
+ -- Refine the error message for unconstrained parameters and
+ -- variables by giving the reason for the illegality.
+
if Ekind (Item_Id) = E_Out_Parameter then
- -- One case is an unconstrained array where the bounds
- -- must be read, if we have this case, output a message
- -- indicating why the OUT parameter is read.
+ -- Unconstrained arrays must appear as inputs because their
+ -- bounds must be read.
if Is_Array_Type (Typ)
and then not Is_Constrained (Typ)
then
Error_Msg_NE
- ("\& is an unconstrained array type, so bounds must be "
- & "read", Item, Typ);
+ ("\\type & is an unconstrained array", Item, Typ);
+ Error_Msg_N ("\\array bounds must be read", Item);
- -- Another case is an unconstrained discriminated record
- -- type where the constrained flag must be read (and if
- -- set, the discriminants). Again output a message.
+ -- Unconstrained discriminated records must appear as inputs
+ -- because their discriminants and constrained flag must be
+ -- read.
elsif Is_Record_Type (Typ)
and then Has_Discriminants (Typ)
and then not Is_Constrained (Typ)
then
Error_Msg_NE
- ("\& is an unconstrained discriminated record type",
+ ("\\type & is an unconstrained discriminated record",
Item, Typ);
Error_Msg_N
- ("\constrained flag and possible discriminants must be "
- & "read", Item);
+ ("\\discriminants and constrained flag must be read",
+ Item);
-- Not clear if there are other cases. Anyway, we will
-- simply ignore any other cases.
@@ -1203,9 +1293,13 @@
-- Output case
else
- Error_Msg_NE
- ("item & must appear in exactly one output dependence list "
- & "(SPARK RM 6.1.5(10))", Item, Item_Id);
+ Add_Item_To_Name_Buffer (Item_Id);
+ Add_Str_To_Name_Buffer
+ (" & must appear in exactly one output dependence list "
+ & "(SPARK RM 6.1.5(10))");
+
+ Error_Msg := Name_Find;
+ Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
end if;
end Usage_Error;
@@ -1805,7 +1899,7 @@
and then Is_Formal (Entity (Obj))
then
Error_Msg_N
- ("external property % cannot apply to a formal parameter "
+ ("external property % cannot apply to parameter "
& "(SPARK RM 7.1.3(2))", N);
end if;
else
@@ -1943,9 +2037,9 @@
if Is_Formal (Item_Id) then
if Scope (Item_Id) = Spec_Id then
- Error_Msg_N
- ("global item cannot reference formal parameter "
- & "(SPARK RM 6.1.4(6))", Item);
+ Error_Msg_NE
+ ("global item cannot reference parameter of subprogram "
+ & "& (SPARK RM 6.1.4(6))", Item, Spec_Id);
return;
end if;
@@ -1977,9 +2071,11 @@
if Has_Visible_Refinement (Item_Id) then
Error_Msg_NE
- ("cannot mention state & in global refinement, use its "
- & "constituents instead (SPARK RM 6.1.4(8))",
+ ("cannot mention state & in global refinement",
Item, Item_Id);
+ Error_Msg_N
+ ("\\use its constituents instead (SPARK RM 6.1.4(8))",
+ Item);
return;
-- If the reference to the abstract state appears in an
@@ -2003,9 +2099,9 @@
and then Global_Mode = Name_Input
then
Error_Msg_NE
- ("volatile global item & with property Effective_Reads "
- & "must have mode In_Out or Output "
- & "(SPARK RM 7.1.3(11))", Item, Item_Id);
+ ("volatile item & with property Effective_Reads must "
+ & "have mode In_Out or Output (SPARK RM 7.1.3(11))",
+ Item, Item_Id);
return;
end if;
end if;
@@ -2129,7 +2225,7 @@
("global item & cannot have mode In_Out or Output "
& "(SPARK RM 6.1.4(12))", Item, Item_Id);
Error_Msg_NE
- ("\item already appears as input of subprogram &",
+ ("\\item already appears as input of subprogram &",
Item, Context);
-- Stop the traversal once an error has been detected
@@ -2472,8 +2568,8 @@
else
Error_Msg_N
- ("initialization item must denote variable or state (SPARK "
- & "RM 7.1.5(3))", Item);
+ ("initialization item must denote variable or state "
+ & "(SPARK RM 7.1.5(3))", Item);
end if;
end if;
end Analyze_Initialization_Item;
@@ -3369,11 +3465,11 @@
if Placement = Not_In_Package then
Error_Msg_N
- ("indicator Part_Of may not appear in this context "
+ ("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
- ("\& is not part of the hidden state of package %",
+ ("\\& is not part of the hidden state of package %",
Indic, Item_Id);
-- The item appears in the visible state space of some package. In
@@ -3397,11 +3493,11 @@
else
Error_Msg_N
- ("indicator Part_Of may not appear in this context (SPARK "
+ ("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
- ("\& is declared in the visible part of package %",
+ ("\\& is declared in the visible part of package %",
Indic, Item_Id);
end if;
@@ -3415,7 +3511,7 @@
& "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
Error_Msg_Name_1 := Chars (Pack_Id);
Error_Msg_NE
- ("\& is declared in the private part of package %",
+ ("\\& is declared in the private part of package %",
Indic, Item_Id);
end if;
@@ -3424,13 +3520,13 @@
else
Error_Msg_N
- ("indicator Part_Of may not appear in this context "
+ ("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
- ("\& is declared in the body of package %", Indic, Item_Id);
+ ("\\& is declared in the body of package %", Indic, Item_Id);
end if;
end if;
@@ -6531,7 +6627,8 @@
Error_Msg_N
("& may not have Ghost convention", E);
Error_Msg_N
- ("\only functions are permitted to have Ghost convention", E);
+ ("\\only functions are permitted to have Ghost convention",
+ E);
return;
end if;
@@ -21644,7 +21741,7 @@
if Has_Refined_State then
Error_Msg_N
- ("\check the use of constituents in dependence refinement",
+ ("\\check the use of constituents in dependence refinement",
Ref_Clause);
end if;
end if;
@@ -21869,7 +21966,7 @@
if Has_Refined_State then
Match_Error
- ("\check the use of constituents in dependence refinement",
+ ("\\check the use of constituents in dependence refinement",
Dep_Input);
end if;
@@ -22107,8 +22204,8 @@
if No (Depends) then
Error_Msg_NE
- ("useless refinement, subprogram & lacks dependence clauses (SPARK "
- & "RM 7.2.5(2))", N, Spec_Id);
+ ("useless refinement, declaration of subprogram & lacks aspect or "
+ & "pragma Depends (SPARK RM 7.2.5(2))", N, Spec_Id);
return;
end if;
@@ -22510,7 +22607,7 @@
end if;
Error_Msg_NE
- ("\ constituent & is missing in output list",
+ ("\\ constituent & is missing in output list",
N, Constit_Id);
end if;
@@ -22670,10 +22767,10 @@
("global item & has inconsistent modes", Item, Item_Id);
Error_Msg_Name_1 := Global_Mode;
- Error_Msg_N ("\ expected mode %", Item);
+ Error_Msg_N ("\\ expected mode %", Item);
Error_Msg_Name_1 := Expect;
- Error_Msg_N ("\ found mode %", Item);
+ Error_Msg_N ("\\ found mode %", Item);
end Inconsistent_Mode_Error;
-- Start of processing for Check_Refined_Global_Item
@@ -22867,7 +22964,8 @@
if No (Global) then
Error_Msg_NE
- ("useless refinement, subprogram & lacks global items", N, Spec_Id);
+ ("useless refinement, declaration of subprogram & lacks aspect or "
+ & "pragma Global", N, Spec_Id);
return;
end if;
@@ -22896,8 +22994,8 @@
and then not Has_Null_State
then
Error_Msg_NE
- ("useless refinement, subprogram & does not mention abstract state "
- & "with visible refinement", N, Spec_Id);
+ ("useless refinement, subprogram & does not depends on abstract "
+ & "state with visible refinement (SPARK RM 7.2.4(2))", N, Spec_Id);
return;
end if;
@@ -23159,7 +23257,7 @@
("& cannot act as constituent of state %",
Constit, Constit_Id);
Error_Msg_NE
- ("\Part_Of indicator specifies & as encapsulating "
+ ("\\Part_Of indicator specifies & as encapsulating "
& "state", Constit, Encapsulating_State (Constit_Id));
end if;
@@ -23446,7 +23544,7 @@
("reference to & not allowed (SPARK RM 6.1.4(8))",
Body_Ref);
Error_Msg_Sloc := Sloc (State);
- Error_Msg_N ("\refinement of & is visible#", Body_Ref);
+ Error_Msg_N ("\\refinement of & is visible#", Body_Ref);
Next_Elmt (Body_Ref_Elmt);
end loop;
@@ -24130,8 +24228,8 @@
& "(SPARK RM 7.2.6(3))", Item_Id);
Error_Msg_Name_1 := Chars (Pack_Id);
Error_Msg_N
- ("\& is declared in the visible part of private child unit %",
- Item_Id);
+ ("\\& is declared in the visible part of private child "
+ & "unit %", Item_Id);
end if;
end if;
@@ -24163,7 +24261,7 @@
& "(SPARK RM 7.2.6(2))", Item_Id);
Error_Msg_Name_1 := Chars (Pack_Id);
Error_Msg_N
- ("\& is declared in the private part of package %", Item_Id);
+ ("\\& is declared in the private part of package %", Item_Id);
end if;
end if;
end Check_Missing_Part_Of;
This patch updates the error diagnostics of various SPARK features to emit clearer and more descriptive messages. ------------ -- Source -- ------------ -- messages.ads package Messages with SPARK_Mode => On is A : Integer := 1; B : Integer := 2; procedure Error_1 (X : in Integer) with Depends => (X => +null); procedure Error_2 (X : out Integer) with Depends => (X => X); procedure Error_3 (X : in out Integer) with Depends => (X => null); procedure Error_4 with Global => (In_Out => A), Depends => ((A, B) => null); end Messages; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c messages.ads messages.ads:8:23: read-only parameter "X" cannot appear as output in dependence relation (SPARK RM 6.1.5(5)) messages.ads:11:28: write-only parameter "X" cannot appear as input in dependence relation (SPARK RM 6.1.5(6)) messages.ads:13:23: parameter "X" must appear in at least one input dependence list (SPARK RM 6.1.5(8)) messages.ads:17:33: global "A" must appear in at least one input dependence list (SPARK RM 6.1.5(8)) messages.ads:18:27: global "B" cannot appear in dependence relation messages.ads:18:27: "B" is not part of the input or output set of subprogram "Error_4" Tested on x86_64-pc-linux-gnu, committed on trunk 2014-02-20 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Add_Item_To_Name_Buffer): New routine. (Analyze_Contract_Case): Remove the use of "may". Replace "aspect Contract_Cases" to avoid categorization of aspect vs pragma. (Analyze_External_Property_In_Decl_Part): Remove the use of "formal". (Analyze_Global_Item): Remove the use of "formal", specify the subprogram. Split the error message about a state with visible refinement into two. Remove the use of "global" from "volatile global item". (Analyze_Initialization_Item): Ensure that the SPARK RM reference is on one line. (Analyze_Input_Output): Update the call to Check_Mode. Specify the duplicated item. Reword the error message concerning an input of a null output list. Use "\" for error message continuation. (Analyze_Part_Of): Remove the use of "may". Use "\" for error message continuation. (Analyze_Refined_Depends_In_Decl_Part): Update the error message concerning a useless refinement to match the format of Refined_Global. (Analyze_Refined_Global_In_Decl_Part): Reword the error message concerning a useless refinement. (Analyze_Refinement_Clause): Use "\" for error message continuation. (Check_Constituent_Usage): Use "\" for error message continuation. (Check_Dependency_Clause): Use "\" for error message continuation. (Check_Matching_Constituent): Use "\" for error message continuation. (Check_Missing_Part_Of): Use "\" for error message continuation. (Check_Mode): Renamed to Check_Role. Update the comment on usage. Redo the error reporting to use Role_Error. (Check_Mode_Restriction_In_Enclosing_Context): Use "\" for error message continuation. (Find_Mode): Renamed to Find_Role. Update the parameter profile along with comment on usage. Update all occurrences of Is_Input and Is_Output. (Inconsistent_Mode_Error): Use "\" for error message continuation. (Input_Match): Use "\" for error message continuation. (Role_Error): New routine. (Set_Convention_From_Pragma): Use "\" for error message continuation. (Usage_Error): Add local variable Error_Msg. Build specialized error message showcasing the offending item kind. Redo the diagnostics for unconstrained types.