-- A flag used to track the legality of a null output
Result_Seen : Boolean := False;
- -- A flag set when Subp_Id'Result is processed
+ -- A flag set when Spec_Id'Result is processed
States_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all states processed so far. It
Item_Is_Output := True;
end if;
+ -- Constant case
+
+ elsif Ekind (Item_Id) = E_Constant then
+ Item_Is_Input := True;
+
-- Generic parameter cases
elsif Ekind (Item_Id) = E_Generic_In_Parameter then
Item_Is_Output := True;
end if;
- -- Object cases
+ -- Variable case
- else pragma Assert (Ekind_In (Item_Id, E_Constant, E_Variable));
+ else pragma Assert (Ekind (Item_Id) = E_Variable);
- -- When pragma Global is present, the mode of the object may
+ -- When pragma Global is present, the mode of the variable may
-- be further constrained by setting a more restrictive mode.
if Global_Seen then
- -- An object has mode IN when its type is unconstrained or
+ -- A variable has mode IN when its type is unconstrained or
-- tagged because array bounds, discriminants or tags can be
-- read.
Item_Is_Output := True;
end if;
- -- Otherwise the object has a default IN OUT mode
+ -- Otherwise the variable has a default IN OUT mode
else
Item_Is_Input := True;
Ref => Item);
end if;
+ -- Constant related checks
+
+ elsif Ekind (Item_Id) = E_Constant then
+
+ -- A constant is read-only item, therefore it cannot act as
+ -- an output.
+
+ if Nam_In (Global_Mode, Name_In_Out, Name_Output) then
+ SPARK_Msg_NE
+ ("constant & cannot act as output", Item, Item_Id);
+ return;
+ end if;
+
-- Variable related checks. These are only relevant when
-- SPARK_Mode is on as they are not standard Ada legality
-- rules.
Null_Seen : Boolean := False;
-- Flags used to check the legality of a null initialization list
- States_And_Vars : Elist_Id := No_Elist;
- -- A list of all abstract states and variables declared in the visible
+ States_And_Objs : Elist_Id := No_Elist;
+ -- A list of all abstract states and objects declared in the visible
-- declarations of the related package. This list is used to detect the
-- legality of initialization items.
-- Verify the legality of a single initialization item followed by a
-- list of input items.
- procedure Collect_States_And_Variables;
+ procedure Collect_States_And_Objects;
-- Inspect the visible declarations of the related package and gather
- -- the entities of all abstract states and variables in States_And_Vars.
+ -- the entities of all abstract states and objects in States_And_Objs.
---------------------------------
-- Analyze_Initialization_Item --
if Is_Entity_Name (Item) then
Item_Id := Entity_Of (Item);
- if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
-
+ if Ekind_In (Item_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
+ then
-- The state or variable must be declared in the visible
-- declarations of the package (SPARK RM 7.1.5(7)).
- if not Contains (States_And_Vars, Item_Id) then
+ if not Contains (States_And_Objs, Item_Id) then
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("initialization item & must appear in the visible "
end if;
end if;
- -- The item references something that is not a state or a
- -- variable (SPARK RM 7.1.5(3)).
+ -- The item references something that is not a state or object
+ -- (SPARK RM 7.1.5(3)).
else
SPARK_Msg_N
- ("initialization item must denote variable or state",
- Item);
+ ("initialization item must denote object or state", Item);
end if;
-- Some form of illegal construct masquerading as a name
else
Error_Msg_N
- ("initialization item must denote variable or state", Item);
+ ("initialization item must denote object or state", Item);
end if;
end if;
end Analyze_Initialization_Item;
Input_Id := Entity_Of (Input);
if Ekind_In (Input_Id, E_Abstract_State,
+ E_Constant,
E_In_Parameter,
E_In_Out_Parameter,
E_Out_Parameter,
E_Variable)
then
- -- The input cannot denote states or variables declared
- -- within the related package.
+ -- The input cannot denote states or objects declared
+ -- within the related package (SPARK RM 7.1.5(4)).
if Within_Scope (Input_Id, Current_Scope) then
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
- ("input item & cannot denote a visible variable or "
- & "state of package % (SPARK RM 7.1.5(4))",
- Input, Input_Id);
+ ("input item & cannot denote a visible object or "
+ & "state of package %", Input, Input_Id);
-- Detect a duplicate use of the same input item
-- (SPARK RM 7.1.5(5)).
Add_Item (Input_Id, States_Seen);
end if;
- if Ekind_In (Input_Id, E_Abstract_State, E_Variable)
+ if Ekind_In (Input_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
and then Present (Encapsulating_State (Input_Id))
then
Add_Item (Input_Id, Constits_Seen);
end if;
end if;
- -- The input references something that is not a state or a
- -- variable (SPARK RM 7.1.5(3)).
+ -- The input references something that is not a state or an
+ -- object (SPARK RM 7.1.5(3)).
else
SPARK_Msg_N
- ("input item must denote variable or state", Input);
+ ("input item must denote object or state", Input);
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
- SPARK_Msg_N
- ("input item must denote variable or state", Input);
+ Error_Msg_N
+ ("input item must denote object or state", Input);
end if;
end if;
end Analyze_Input_Item;
end if;
end Analyze_Initialization_Item_With_Inputs;
- ----------------------------------
- -- Collect_States_And_Variables --
- ----------------------------------
+ --------------------------------
+ -- Collect_States_And_Objects --
+ --------------------------------
- procedure Collect_States_And_Variables is
+ procedure Collect_States_And_Objects is
Pack_Spec : constant Node_Id := Specification (Pack_Decl);
Decl : Node_Id;
-- Collect the abstract states defined in the package (if any)
if Present (Abstract_States (Pack_Id)) then
- States_And_Vars := New_Copy_Elist (Abstract_States (Pack_Id));
+ States_And_Objs := New_Copy_Elist (Abstract_States (Pack_Id));
end if;
- -- Collect all variables the appear in the visible declarations of
- -- the related package.
+ -- Collect all objects the appear in the visible declarations of the
+ -- related package.
if Present (Visible_Declarations (Pack_Spec)) then
Decl := First (Visible_Declarations (Pack_Spec));
while Present (Decl) loop
- if Nkind (Decl) = N_Object_Declaration
- and then Ekind (Defining_Entity (Decl)) = E_Variable
- and then Comes_From_Source (Decl)
+ if Comes_From_Source (Decl)
+ and then Nkind (Decl) = N_Object_Declaration
then
- Add_Item (Defining_Entity (Decl), States_And_Vars);
+ Add_Item (Defining_Entity (Decl), States_And_Objs);
end if;
Next (Decl);
end loop;
end if;
- end Collect_States_And_Variables;
+ end Collect_States_And_Objects;
-- Local variables
-- Initialize the various lists used during analysis
- Collect_States_And_Variables;
+ Collect_States_And_Objects;
if Present (Expressions (Inits)) then
Init := First (Expressions (Inits));
return;
end if;
- -- Determine where the state, variable or the package instantiation
+ -- Determine where the state, object or the package instantiation
-- lives with respect to the enclosing packages or package bodies (if
-- any). This placement dictates the legality of the encapsulating
-- state.
State_Id : Entity_Id;
Instance : Node_Id);
-- Propagate the Part_Of indicator to all abstract states and
- -- variables declared in the visible state space of a package
+ -- objects declared in the visible state space of a package
-- denoted by Pack_Id. State_Id is the encapsulating state.
-- Instance is the package instantiation node.
procedure Propagate_Part_Of (Pack_Id : Entity_Id);
-- Propagate the Part_Of indicator to all abstract states and
- -- variables declared in the visible state space of a package
+ -- objects declared in the visible state space of a package
-- denoted by Pack_Id.
-----------------------
begin
-- Traverse the entity chain of the package and set relevant
- -- attributes of abstract states and variables declared in
- -- the visible state space of the package.
+ -- attributes of abstract states and objects declared in the
+ -- visible state space of the package.
Item_Id := First_Entity (Pack_Id);
while Present (Item_Id)
if not Comes_From_Source (Item_Id) then
null;
- -- The Part_Of indicator turns an abstract state or a
- -- variable into a constituent of the encapsulating
- -- state.
+ -- The Part_Of indicator turns an abstract state or an
+ -- object into a constituent of the encapsulating state.
elsif Ekind_In (Item_Id, E_Abstract_State,
+ E_Constant,
E_Variable)
then
Has_Item := True;
Check_Arg_Count (1);
-- Ensure the proper placement of the pragma. Part_Of must appear
- -- on a variable declaration or a package instantiation.
+ -- on an object declaration or a package instantiation.
Stmt := Prev (N);
while Present (Stmt) loop
Stmt := Prev (Stmt);
end loop;
- -- When the context is an object declaration, ensure that it is a
- -- variable.
-
- if Nkind (Stmt) = N_Object_Declaration
- and then Ekind (Defining_Entity (Stmt)) /= E_Variable
- then
- SPARK_Msg_N ("indicator Part_Of must apply to a variable", N);
- return;
- end if;
-
-- Extract the entity of the related object declaration or package
-- instantiation. In the case of the instantiation, use the entity
-- of the instance spec.
if Legal then
State_Id := Entity (State);
- -- The Part_Of indicator turns a variable into a constituent
- -- of the encapsulating state.
+ -- The Part_Of indicator turns an object into a constituent of
+ -- the encapsulating state.
- if Ekind (Item_Id) = E_Variable then
+ if Ekind_In (Item_Id, E_Constant, E_Variable) then
Append_Elmt (Item_Id, Part_Of_Constituents (State_Id));
Set_Encapsulating_State (Item_Id, State_Id);
-- 2) Dep_Item denotes null and Ref_Item is Empty (special case)
-- 3) Both items denote attribute 'Result
-- 4) Both items denote the same formal parameter
- -- 5) Both items denote the same variable
+ -- 5) Both items denote the same object
-- 6) Dep_Item is an abstract state with visible null refinement
-- and Ref_Item denotes null.
-- 7) Dep_Item is an abstract state with visible null refinement
then
Matched := True;
- -- Abstract states, formal parameters and variables
+ -- Abstract states, formal parameters and objects
elsif Is_Entity_Name (Dep_Item) then
Matched := True;
end if;
- -- A formal parameter or a variable matches itself
+ -- A formal parameter or an object matches itself
elsif Is_Entity_Name (Ref_Item)
and then Entity_Of (Ref_Item) = Dep_Item_Id
Item := First (Expressions (List));
while Present (Item) loop
Check_Refined_Global_Item (Item, Global_Mode);
-
Next (Item);
end loop;
-- Perform full analysis of a single refinement clause
function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id;
- -- Gather the entities of all abstract states and variables declared in
+ -- Gather the entities of all abstract states and objects declared in
-- the body state space of package Pack_Id.
procedure Report_Unrefined_States (States : Elist_Id);
if Node (State_Elmt) = Constit_Id then
Check_Ghost_Constituent (Constit_Id);
-
Remove_Elmt (Body_States, State_Elmt);
Collect_Constituent;
return;
if Is_Entity_Name (Constit) then
Constit_Id := Entity_Of (Constit);
- if Ekind_In (Constit_Id, E_Abstract_State, E_Variable) then
+ if Ekind_In (Constit_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
+ then
Check_Matching_Constituent (Constit_Id);
else
if Ekind (Constit_Id) = E_Abstract_State then
SPARK_Msg_NE
("\abstract state & defined #", State, Constit_Id);
+
+ elsif Ekind (Constit_Id) = E_Constant then
+ SPARK_Msg_NE
+ ("\constant & defined #", State, Constit_Id);
+
else
+ pragma Assert (Ekind (Constit_Id) = E_Variable);
SPARK_Msg_NE ("\variable & defined #", State, Constit_Id);
end if;
----------------------------
procedure Collect_Visible_States (Pack_Id : Entity_Id) is
+ Decl : Node_Id;
Item_Id : Entity_Id;
begin
if not Comes_From_Source (Item_Id) then
null;
- elsif Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+ elsif Ekind (Item_Id) = E_Abstract_State then
Add_Item (Item_Id, Result);
+ elsif Ekind_In (Item_Id, E_Constant, E_Variable) then
+ Decl := Declaration_Node (Item_Id);
+
+ -- Do not consider constants or variables that map generic
+ -- formals to their actuals as the formals cannot be named
+ -- from the outside and participate in refinement.
+
+ if No (Corresponding_Generic_Association (Decl)) then
+ Add_Item (Item_Id, Result);
+ end if;
+
-- Recursively gather the visible states of a nested package
elsif Ekind (Item_Id) = E_Package then
Decl := First (Declarations (Pack_Body));
while Present (Decl) loop
+
+ -- Capture source objects as internally generated temporaries
+ -- cannot be named and participate in refinement.
+
if Nkind (Decl) = N_Object_Declaration then
Item_Id := Defining_Entity (Decl);
- -- Capture source variables as internally generated temporaries
- -- cannot be named and participate in refinement.
-
- if Ekind (Item_Id) = E_Variable
- and then Comes_From_Source (Item_Id)
- then
+ if Comes_From_Source (Item_Id) then
Add_Item (Item_Id, Result);
end if;
+ -- Capture the visible abstract states and objects of a source
+ -- package [instantiation].
+
elsif Nkind (Decl) = N_Package_Declaration then
Item_Id := Defining_Entity (Decl);
- -- Capture the visible abstract states and objects of a
- -- source package [instantiation].
-
if Comes_From_Source (Item_Id) then
Collect_Visible_States (Item_Id);
end if;
if Ekind (State_Id) = E_Abstract_State then
SPARK_Msg_NE
("\abstract state & defined #", Body_Id, State_Id);
+
+ elsif Ekind (State_Id) = E_Constant then
+ SPARK_Msg_NE ("\constant & defined #", Body_Id, State_Id);
+
else
+ pragma Assert (Ekind (State_Id) = E_Variable);
SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
end if;
Available_States := New_Copy_Elist (Abstract_States (Spec_Id));
- -- Gather all abstract states and variables declared in the visible
+ -- Gather all abstract states and objects declared in the visible
-- state space of the package body. These items must be utilized as
-- constituents in a state refinement.
Clause := First (Component_Associations (Clauses));
while Present (Clause) loop
Analyze_Refinement_Clause (Clause);
-
Next (Clause);
end loop;
end if;
Report_Unrefined_States (Available_States);
- -- Ensure that all abstract states and variables declared in the body
+ -- Ensure that all abstract states and objects declared in the body
-- state space of the related package are utilized as constituents.
Report_Unused_States (Body_States);
projects / gcc.git / commitdiff