+2014-01-20 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * einfo.ads: E_Abstract_State is now part of the entities that
+ can be overloaded. Update type Overloadable_Kind to reflect the
+ inclusion of abstract states.
+ * sem_ch6.adb (New_Overloaded_Entity): A function can now
+ overload an abstract state.
+ * sem_prag.adb (Analyze_Constituent): Handle the overloading
+ of states by functions. Use Entity_Of to obtain the entity of
+ a constituent. (Analyze_Global_Item): Handle the overloading of
+ states by functions.
+ (Analyze_Initialization_Item): Handle the
+ overloading of states by functions. Use Entity_Of to obtain the
+ entity of an item.
+ (Analyze_Input_Item): Handle the overloading
+ of states by functions. Use Entity_Of to obtain the entity of an item.
+ (Analyze_Input_Output): Handle the overloading of states by functions.
+ (Analyze_Refinement_Clause): Handle the overloading
+ of states by functions. Use Entity_Of to obtain the entity of an item.
+ (Appears_In): Use Entity_Of to obtain the entity of an element.
+ (Check_Usage): Use Entity_Of to obtain the entity of
+ an item. Add a guard to prevent a crash due to a previous error.
+ (Resolve_State): New routine.
+
+2014-01-20 Yannick Moy <moy@adacore.com>
+
+ * spark_xrefs.ads, debug.adb, gnat1drv.adb, errout.adb, errout.ads,
+ opt.ads: Minor comments updates.
+
2014-01-20 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb (Non_Limited_View): Applies to abstract states.
-- ALI files to compute effects of subprograms. Note that ALI files
-- are only written when option d.G is also given.
- -- d.G Frame condition mode for gnat2why. In this mode, gnat2why will not
- -- generate Why code. Instead, it generates ALI files with an extra
- -- section which contains the effects of subprograms.
+ -- d.G Frame condition mode for gnat2why. In this mode, gnat2why will
+ -- generate ALI files with an extra section which contains the effects
+ -- of subprograms.
-- d.I Do not ignore enum representation clauses in CodePeer mode.
-- The default of ignoring representation clauses for enumeration
-- An entry, created by an entry declaration in a task or protected
-- object.
+ E_Abstract_State,
+ -- A state abstraction. Used to designate entities introduced by aspect
+ -- or pragma Abstract_State. The entity carries the various properties
+ -- of the state.
+
--------------------
-- Other Entities --
--------------------
-- A task body. This entity serves almost no function, since all
-- semantic analysis uses the protected entity (E_Task_Type).
- E_Subprogram_Body,
+ E_Subprogram_Body
-- A subprogram body. Used when a subprogram has a separate declaration
-- to represent the entity for the body. This entity serves almost no
-- function, since all semantic analysis uses the subprogram entity
-- for the declaration (E_Function or E_Procedure).
-
- E_Abstract_State
- -- A state abstraction. Used to designate entities introduced by aspect
- -- or pragma Abstract_State. The entity carries the various properties
- -- of the state.
);
for Entity_Kind'Size use 8;
-- E_Function
-- E_Operator
-- E_Procedure
- E_Entry;
+ -- E_Entry
+ E_Abstract_State;
subtype Private_Kind is Entity_Kind range
E_Record_Type_With_Private ..
if not Finalize_Called then
raise Program_Error;
- -- In formal verification mode, errors issued when generating Why code
+ -- In formal verification mode, errors issued when analyzing code
-- are not compilation errors, and should not result in exiting with
-- an error status. These errors are handled in the driver of the
-- verification process instead.
-- Returns True if errors have been detected, or warnings in -gnatwe (treat
-- warnings as errors) mode. Note that it is mandatory to call Finalize
-- before calling this routine. Always returns False in formal verification
- -- mode, because errors issued when generating Why code are not compilation
+ -- mode, because errors issued when analyzing code are not compilation
-- errors, and should not result in exiting with an error status.
procedure Error_Msg_CRT (Feature : String; N : Node_Id);
end if;
-- Distinguish between the two modes of gnat2why: frame condition
- -- generation (generation of ALI files) and translation of Why (no
- -- ALI files generated). This is done with the switch -gnatd.G,
- -- which activates frame condition mode. The other changes in
- -- behavior depending on this switch are done in gnat2why directly.
+ -- generation (generation of ALI files) and analysis (no ALI files
+ -- generated). This is done with the switch -gnatd.G, which activates
+ -- frame condition mode. The other changes in behavior depending on
+ -- this switch are done in gnat2why directly.
if Debug_Flag_Dot_GG then
Frame_Condition_Mode := True;
-- It is not an error to analyze in GNATprove mode a spec which requires
-- a body, when the body is not available. During frame condition
-- generation, the corresponding ALI file is generated. During
- -- translation to Why, Why code is generated for the spec.
+ -- analysis, the spec is analyzed.
elsif GNATprove_Mode then
Back_End_Mode := Declarations_Only;
Frame_Condition_Mode : Boolean := False;
-- Specific mode to be used in combination with GNATprove_Mode. If set to
-- true, ALI files containing the frame conditions (global effects) are
- -- generated, and Why files are *not* generated. If not true, Why files
- -- are generated. Set by debug flag -gnatd.G.
+ -- generated, and analysis is *not* performed. If not true, analysis is
+ -- performed. Set by debug flag -gnatd.G.
Formal_Extensions : Boolean := False;
-- When this flag is set, new aspects/pragmas/attributes are accepted,
-- in a configuration file such as gnat.adc.
GNATprove_Mode : Boolean := False;
- -- Specific compiling mode targeting formal verification through the
- -- generation of Why code for those parts of the input code that belong to
- -- the SPARK 2014 subset of Ada. Set True by the gnat2why executable or by
- -- use of the -gnatd.F debug switch. Note that this is completely separate
- -- from the SPARK restriction defined in GNAT to detect violations of a
- -- subset of SPARK 2005 rules.
+ -- Specific compiling mode targeting formal verification for those parts
+ -- of the input code that belong to the SPARK 2014 subset of Ada. Set True
+ -- by the gnat2why executable or by use of the -gnatd.F debug switch. Note
+ -- that this is completely separate from the SPARK restriction defined in
+ -- GNAT to detect violations of a subset of SPARK 2005 rules.
SPARK_Strict_Mode : Boolean := False;
-- Interpret compiler permissions as strictly as possible. E.g. base ranges
if Scope (E) /= Current_Scope then
null;
+ -- A function can overload the name of an abstract state. The
+ -- state can be viewed as a function with a profile that cannot
+ -- be matched by anything.
+
+ elsif Ekind (S) = E_Function
+ and then Ekind (E) = E_Abstract_State
+ then
+ Enter_Overloaded_Entity (S);
+ return;
+
-- Ada 2012 (AI05-0165): For internally generated bodies of null
-- procedures locate the internally generated spec. We enforce
-- mode conformance since a tagged type may inherit from
-- determines if we have a body reference to an abstract state, which may
-- be illegal if the state is refined within the body.
+ procedure Resolve_State (N : Node_Id);
+ -- Handle the overloading of state names by functions. When N denotes a
+ -- function, this routine finds the corresponding state and sets the entity
+ -- of N to that of the state.
+
procedure Rewrite_Assertion_Kind (N : Node_Id);
-- If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
-- then it is rewritten as an identifier with the corresponding special
Error_Msg_N ("cannot mix null and non-null items", Item);
end if;
- Analyze (Item);
+ Analyze (Item);
+ Resolve_State (Item);
-- Find the entity of the item. If this is a renaming, climb
-- the renaming chain to reach the root object. Renamings of
if Nkind (Item) = N_Defining_Identifier then
Item_Id := Item;
else
- Item_Id := Entity (Item);
+ Item_Id := Entity_Of (Item);
end if;
-- The item does not appear in a dependency
- if not Contains (Used_Items, Item_Id) then
+ if Present (Item_Id)
+ and then not Contains (Used_Items, Item_Id)
+ then
if Is_Formal (Item_Id) then
Usage_Error (Item, Item_Id);
return;
end if;
- Analyze (Item);
+ Analyze (Item);
+ Resolve_State (Item);
-- Find the entity of the item. If this is a renaming, climb the
-- renaming chain to reach the root object. Renamings of non-
("cannot mix null and non-null initialization items", Item);
end if;
- Analyze (Item);
+ Analyze (Item);
+ Resolve_State (Item);
if Is_Entity_Name (Item) then
- Item_Id := Entity (Item);
+ Item_Id := Entity_Of (Item);
if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
("cannot mix null and non-null initialization item", Item);
end if;
- Analyze (Input);
+ Analyze (Input);
+ Resolve_State (Input);
if Is_Entity_Name (Input) then
- Input_Id := Entity (Input);
+ Input_Id := Entity_Of (Input);
if Ekind_In (Input_Id, E_Abstract_State, E_Variable) then
("cannot mix null and non-null constituents", Constit);
end if;
- Analyze (Constit);
+ Analyze (Constit);
+ Resolve_State (Constit);
-- Ensure that the constituent denotes a valid state or a
-- whole variable.
if Is_Entity_Name (Constit) then
- Constit_Id := Entity (Constit);
+ Constit_Id := Entity_Of (Constit);
if Ekind_In (Constit_Id, E_Abstract_State, E_Variable) then
Check_Matching_Constituent (Constit_Id);
("refinement clause cannot cover multiple states", State);
else
- Analyze (State);
+ Analyze (State);
+ Resolve_State (State);
-- Ensure that the state name denotes a valid abstract state
-- that is defined in the spec of the related package.
if Is_Entity_Name (State) then
- State_Id := Entity (State);
+ State_Id := Entity_Of (State);
-- Catch any attempts to re-refine a state or refine a
-- state that is not defined in the package declaration.
if Nkind (Node (Elmt)) = N_Defining_Identifier then
Id := Node (Elmt);
else
- Id := Entity (Node (Elmt));
+ Id := Entity_Of (Node (Elmt));
end if;
if Id = Item_Id then
end loop;
end Relocate_Pragmas_To_Body;
+ -------------------
+ -- Resolve_State --
+ -------------------
+
+ procedure Resolve_State (N : Node_Id) is
+ Func : Entity_Id;
+ State : Entity_Id;
+
+ begin
+ if Is_Entity_Name (N) and then Present (Entity (N)) then
+ Func := Entity (N);
+
+ -- Handle overloading of state names by functions. Traverse the
+ -- homonym chain looking for an abstract state.
+
+ if Ekind (Func) = E_Function and then Has_Homonym (Func) then
+ State := Homonym (Func);
+ while Present (State) loop
+
+ -- Resolve the overloading by setting the proper entity of the
+ -- reference to that of the state.
+
+ if Ekind (State) = E_Abstract_State then
+ Set_Etype (N, Standard_Void_Type);
+ Set_Entity (N, State);
+ Set_Associated_Node (N, State);
+ return;
+ end if;
+
+ State := Homonym (State);
+ end loop;
+
+ -- A function can never act as a state. If the homonym chain does
+ -- not contain a corresponding state, then something went wrong in
+ -- the overloading mechanism.
+
+ raise Program_Error;
+ end if;
+ end if;
+ end Resolve_State;
+
----------------------------
-- Rewrite_Assertion_Kind --
----------------------------
-- SPARK cross-reference information is generated on a unit-by-unit basis
-- in the ALI file, using lines that start with the identifying character F
- -- ("Formal"). These lines are generated if -gnatd.E or -gnatd.F (Why
- -- generation mode) switches are set.
+ -- ("Formal"). These lines are generated if Frame_Condition_Mode is True.
-- The SPARK cross-reference information comes after the shared
-- cross-reference information, so it needs not be read by tools like
projects / thirdparty / gcc.git / commitdiff
