+2013-10-10 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb: Add an entry in table Canonical_Aspect for
+ Refined_State.
+ * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
+ Aspect_Names and Aspect_Delay for Refined_State.
+ * einfo.adb: Add with and use clauses for Elists.
+ Remove Refined_State from the list of node usage.
+ Add Refined_State_Pragma to the list of node usage.
+ (Has_Null_Abstract_State): New routine.
+ (Refined_State): Removed.
+ (Refined_State_Pragma): New routine.
+ (Set_Refined_State): Removed.
+ (Set_Refined_State_Pragma): New routine.
+ (Write_Field8_Name): Add output for Refined_State_Pragma.
+ (Write_Field9_Name): Remove the output for Refined_State.
+ * einfo.ads: Add new synthesized attribute Has_Null_Abstract_State
+ along with usage in nodes. Remove attribute Refined_State along
+ with usage in nodes. Add new attribute Refined_State_Pragma along
+ with usage in nodes.
+ (Has_Null_Abstract_State): New routine.
+ (Refined_State): Removed.
+ (Refined_State_Pragma): New routine.
+ (Set_Refined_State): Removed.
+ (Set_Refined_State_Pragma): New routine.
+ * elists.adb (Clone): New routine.
+ * elists.ads (Clone): New routine.
+ * par-prag.adb: Add Refined_State to the pragmas that do not
+ require special processing by the parser.
+ * sem_ch3.adb: Add with and use clause for Sem_Prag.
+ (Analyze_Declarations): Add local variables Body_Id, Context and
+ Spec_Id. Add processing for delayed aspect/pragma Refined_State.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Update the
+ handling of aspect Abstract_State. Add processing for aspect
+ Refined_State. Remove the bizzare insertion policy for aspect
+ Abstract_State.
+ (Check_Aspect_At_Freeze_Point): Add an entry for Refined_State.
+ * sem_prag.adb: Add an entry to table Sig_Flags
+ for pragma Refined_State.
+ (Add_Item): Update the
+ comment on usage. The inserted items need not be unique.
+ (Analyze_Contract_Cases_In_Decl_Part): Rename variable Restore to
+ Restore_Scope and update all its occurrences.
+ (Analyze_Pragma):
+ Update the handling of pragma Abstract_State. Add processing for
+ pragma Refined_State.
+ (Analyze_Pre_Post_Condition_In_Decl_Part):
+ Rename variable Restore to Restore_Scope and update all its
+ occurrences.
+ (Analyze_Refined_State_In_Decl_Part): New routine.
+ * sem_prag.ads (Analyze_Refined_State_In_Decl_Part): New routine.
+ * snames.ads-tmpl: Add new predefined name for Refined_State. Add
+ new Pragma_Id for Refined_State.
+
+2013-10-10 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch10.adb (Install_Limited_Withed_Unit): handle properly the
+ case of a record declaration in a limited view, when the record
+ contains a self-referential component of an anonymous access type.
+
2013-10-10 Thomas Quinot <quinot@adacore.com>
* exp_ch4.adb (Process_Transient_Object): For any context other
Aspect_Refined_Global => Aspect_Refined_Global,
Aspect_Refined_Post => Aspect_Refined_Post,
Aspect_Refined_Pre => Aspect_Refined_Pre,
+ Aspect_Refined_State => Aspect_Refined_State,
Aspect_Remote_Access_Type => Aspect_Remote_Access_Type,
Aspect_Remote_Call_Interface => Aspect_Remote_Call_Interface,
Aspect_Remote_Types => Aspect_Remote_Types,
Aspect_Refined_Global, -- GNAT
Aspect_Refined_Post, -- GNAT
Aspect_Refined_Pre, -- GNAT
+ Aspect_Refined_State, -- GNAT
Aspect_Relative_Deadline,
Aspect_Scalar_Storage_Order, -- GNAT
Aspect_Simple_Storage_Pool, -- GNAT
Aspect_Refined_Global => Expression,
Aspect_Refined_Post => Expression,
Aspect_Refined_Pre => Expression,
+ Aspect_Refined_State => Expression,
Aspect_Relative_Deadline => Expression,
Aspect_Scalar_Storage_Order => Expression,
Aspect_Simple_Storage_Pool => Name,
Aspect_Refined_Global => Name_Refined_Global,
Aspect_Refined_Post => Name_Refined_Post,
Aspect_Refined_Pre => Name_Refined_Pre,
+ Aspect_Refined_State => Name_Refined_State,
Aspect_Relative_Deadline => Name_Relative_Deadline,
Aspect_Remote_Access_Type => Name_Remote_Access_Type,
Aspect_Remote_Call_Interface => Name_Remote_Call_Interface,
Aspect_Read => Always_Delay,
Aspect_Refined_Depends => Always_Delay,
Aspect_Refined_Global => Always_Delay,
+ Aspect_Refined_State => Always_Delay,
Aspect_Relative_Deadline => Always_Delay,
Aspect_Remote_Access_Type => Always_Delay,
Aspect_Remote_Call_Interface => Always_Delay,
-- Turn off subprogram ordering, not used for this unit
with Atree; use Atree;
+with Elists; use Elists;
with Namet; use Namet;
with Nlists; use Nlists;
with Output; use Output;
-- Mechanism Uint8 (but returns Mechanism_Type)
-- Normalized_First_Bit Uint8
-- Postcondition_Proc Node8
+ -- Refined_State_Pragma Node8
-- Return_Applies_To Node8
-- First_Exit_Statement Node8
-- Class_Wide_Type Node9
-- Current_Value Node9
- -- Refined_State Node9
-- Renaming_Map Uint9
-- Direct_Primitive_Operations Elist10
return Flag227 (Id);
end Referenced_As_Out_Parameter;
- function Refined_State (Id : E) return E is
+ function Refined_State_Pragma (Id : E) return N is
begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- return Node9 (Id);
- end Refined_State;
+ pragma Assert (Ekind (Id) = E_Package_Body);
+ return Node8 (Id);
+ end Refined_State_Pragma;
function Register_Exception_Call (Id : E) return N is
begin
Set_Flag227 (Id, V);
end Set_Referenced_As_Out_Parameter;
- procedure Set_Refined_State (Id : E; V : E) is
+ procedure Set_Refined_State_Pragma (Id : E; V : N) is
begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- Set_Node9 (Id, V);
- end Set_Refined_State;
+ pragma Assert (Ekind (Id) = E_Package_Body);
+ Set_Node8 (Id, V);
+ end Set_Refined_State_Pragma;
procedure Set_Register_Exception_Call (Id : E; V : N) is
begin
return False;
end Has_Interrupt_Handler;
+ -----------------------------
+ -- Has_Null_Abstract_State --
+ -----------------------------
+
+ function Has_Null_Abstract_State (Id : E) return B is
+ begin
+ pragma Assert (Ekind_In (Id, E_Generic_Package, E_Package));
+
+ return
+ Present (Abstract_States (Id))
+ and then Is_Null_State (Node (First_Elmt (Abstract_States (Id))));
+ end Has_Null_Abstract_State;
+
--------------------
-- Has_Unmodified --
--------------------
when E_Procedure =>
Write_Str ("Postcondition_Proc");
+ when E_Package_Body =>
+ Write_Str ("Refined_State_Pragma");
+
when E_Return_Statement =>
Write_Str ("Return_Applies_To");
when Object_Kind =>
Write_Str ("Current_Value");
- when E_Abstract_State =>
- Write_Str ("Refined_State");
-
when E_Function |
E_Generic_Function |
E_Generic_Package |
-- are not considered to be significant since they do not affect
-- stored bit patterns.
+-- Has_Null_Abstract_State (synth)
+-- Defined in package entities. True if the package is subject to a null
+-- Abstract_State aspect/pragma.
+
-- Has_Object_Size_Clause (Flag172)
-- Defined in entities for types and subtypes. Set if an Object_Size
-- clause has been processed for the type Used to prevent multiple
-- we have a separate warning for variables that are only assigned and
-- never read, and out parameters are a special case.
--- Refined_State (Node9)
--- Defined in E_Abstract_State entities. Contains the entity of the
--- abstract state completion which is usually foung in package bodies.
+-- Refined_State_Pragma (Node8)
+-- Defined in [generic] package bodies. Contains the pragma that refines
+-- all abstract states defined in the corresponding package declaration.
-- Register_Exception_Call (Node20)
-- Defined in exception entities. When an exception is declared,
------------------------------------------
-- E_Abstract_State
- -- Refined_State (Node9)
-- Is_External_State (synth)
-- Is_Input_Only_State (synth)
-- Is_Null_State (synth)
-- Is_Visible_Lib_Unit (Flag116)
-- Renamed_In_Spec (Flag231) (non-generic case only)
-- Static_Elaboration_Desired (Flag77) (non-generic case only)
+ -- Has_Null_Abstract_State (synth)
-- Is_Wrapper_Package (synth) (non-generic case only)
-- Scope_Depth (synth)
-- E_Package_Body
+ -- Refined_State_Pragma (Node8)
-- Handler_Records (List10) (non-generic case only)
-- Related_Instance (Node15) (non-generic case only)
-- First_Entity (Node17)
function Referenced (Id : E) return B;
function Referenced_As_LHS (Id : E) return B;
function Referenced_As_Out_Parameter (Id : E) return B;
- function Refined_State (Id : E) return E;
+ function Refined_State_Pragma (Id : E) return E;
function Register_Exception_Call (Id : E) return N;
function Related_Array_Object (Id : E) return E;
function Related_Expression (Id : E) return N;
function Has_Attach_Handler (Id : E) return B;
function Has_Entries (Id : E) return B;
function Has_Foreign_Convention (Id : E) return B;
+ function Has_Null_Abstract_State (Id : E) return B;
function Implementation_Base_Type (Id : E) return E;
function Is_Base_Type (Id : E) return B;
function Is_Boolean_Type (Id : E) return B;
procedure Set_Referenced (Id : E; V : B := True);
procedure Set_Referenced_As_LHS (Id : E; V : B := True);
procedure Set_Referenced_As_Out_Parameter (Id : E; V : B := True);
- procedure Set_Refined_State (Id : E; V : E);
+ procedure Set_Refined_State_Pragma (Id : E; V : N);
procedure Set_Register_Exception_Call (Id : E; V : N);
procedure Set_Related_Array_Object (Id : E; V : E);
procedure Set_Related_Expression (Id : E; V : N);
pragma Inline (Referenced);
pragma Inline (Referenced_As_LHS);
pragma Inline (Referenced_As_Out_Parameter);
- pragma Inline (Refined_State);
+ pragma Inline (Refined_State_Pragma);
pragma Inline (Register_Exception_Call);
pragma Inline (Related_Array_Object);
pragma Inline (Related_Expression);
pragma Inline (Set_Referenced);
pragma Inline (Set_Referenced_As_LHS);
pragma Inline (Set_Referenced_As_Out_Parameter);
- pragma Inline (Set_Refined_State);
+ pragma Inline (Set_Refined_State_Pragma);
pragma Inline (Set_Register_Exception_Call);
pragma Inline (Set_Related_Array_Object);
pragma Inline (Set_Related_Expression);
end loop;
end Append_Unique_Elmt;
+ -----------
+ -- Clone --
+ ------------
+
+ function Clone (List : Elist_Id) return Elist_Id is
+ Result : Elist_Id;
+ Elmt : Elmt_Id;
+
+ begin
+ if List = No_Elist then
+ return No_Elist;
+
+ -- Replicate the contents of the input list while preserving the
+ -- original order.
+
+ else
+ Result := New_Elmt_List;
+
+ Elmt := First_Elmt (List);
+ while Present (Elmt) loop
+ Append_Elmt (Node (Elmt), Result);
+ Next_Elmt (Elmt);
+ end loop;
+
+ return Result;
+ end if;
+ end Clone;
+
--------------
-- Contains --
--------------
-- affected, but the space used by the list element may be (but is not
-- required to be) freed for reuse in a subsequent Append_Elmt call.
+ function Clone (List : Elist_Id) return Elist_Id;
+ -- Create a copy of the input list. Internal list nodes are not shared and
+ -- order of elements is preserved.
+
function Contains (List : Elist_Id; N : Node_Or_Entity_Id) return Boolean;
-- Perform a sequential search to determine whether the given list contains
-- a node or an entity.
Pragma_Refined_Global |
Pragma_Refined_Post |
Pragma_Refined_Pre |
+ Pragma_Refined_State |
Pragma_Relative_Deadline |
Pragma_Remote_Access_Type |
Pragma_Remote_Call_Interface |
function Same_Unit (N : Node_Id; P : Entity_Id) return Boolean is
begin
return Entity (N) = P
- or else
- (Present (Renamed_Object (P))
- and then Entity (N) = Renamed_Object (P));
+ or else (Present (Renamed_Object (P))
+ and then Entity (N) = Renamed_Object (P));
end Same_Unit;
-- Start of processing for Process_Body_Clauses
elsif Nkind (Cont_Item) = N_Pragma
and then
Nam_In (Pragma_Name (Cont_Item), Name_Elaborate,
- Name_Elaborate_All)
+ Name_Elaborate_All)
and then not Used_Type_Or_Elab
then
Prag_Unit :=
First (Pragma_Argument_Associations (Cont_Item));
- while Present (Prag_Unit)
- and then not Used_Type_Or_Elab
- loop
+ while Present (Prag_Unit) and then not Used_Type_Or_Elab loop
if Entity (Expression (Prag_Unit)) = Nam_Ent then
Used_Type_Or_Elab := True;
end if;
-- with Pack;
-- with Pack;
-- pragma Elaborate (Pack);
- --
+
-- In this case, the second with clause is redundant since
-- the pragma applies only to the first "with Pack;".
if (Withed_In_Spec
and then not Used_Type_Or_Elab)
and then
- ((not Used_In_Spec
- and then not Used_In_Body)
- or else
- Used_In_Spec)
+ ((not Used_In_Spec and then not Used_In_Body)
+ or else Used_In_Spec)
then
Error_Msg_N -- CODEFIX
("redundant with clause in body??", Clause);
N_Package_Renaming_Declaration,
N_Subprogram_Declaration)
or else Nkind (Unit_Node) in N_Generic_Declaration
- or else
- (Nkind (Unit_Node) = N_Subprogram_Body
- and then Acts_As_Spec (Unit_Node))
+ or else (Nkind (Unit_Node) = N_Subprogram_Body
+ and then Acts_As_Spec (Unit_Node))
then
Remove_Unit_From_Visibility (Defining_Entity (Unit_Node));
Nam := Full_View (Nam);
end if;
- if No (Nam)
- or else not Is_Protected_Type (Etype (Nam))
- then
+ if No (Nam) or else not Is_Protected_Type (Etype (Nam)) then
Error_Msg_N ("missing specification for Protected body", N);
+
else
Set_Scope (Defining_Entity (N), Current_Scope);
Set_Has_Completion (Etype (Nam));
N_Subprogram_Body)
then
Decl := First (Declarations (Parent (N)));
- while Present (Decl)
- and then Decl /= N
- loop
+ while Present (Decl) and then Decl /= N loop
if Nkind (Decl) = N_Subprogram_Body_Stub
and then (Chars (Defining_Unit_Name (Specification (Decl))) =
Chars (Defining_Unit_Name (Specification (N))))
E := First_Entity (Current_Scope);
while Present (E) loop
- if not Is_Child_Unit (E)
- or else Is_Visible_Lib_Unit (E)
- then
+ if not Is_Child_Unit (E) or else Is_Visible_Lib_Unit (E) then
Set_Is_Immediately_Visible (E);
end if;
if Is_Package_Or_Generic_Package (Par_Unit) then
if not Is_Immediately_Visible (Par_Unit)
or else (Present (First_Entity (Par_Unit))
- and then not Is_Immediately_Visible
- (First_Entity (Par_Unit)))
+ and then not
+ Is_Immediately_Visible (First_Entity (Par_Unit)))
then
Set_Is_Immediately_Visible (Par_Unit);
Install_Visible_Declarations (Par_Unit);
or else Private_Present (Item)
or else Nkind_In (Lib_Unit, N_Package_Body, N_Subunit)
or else (Nkind (Lib_Unit) = N_Subprogram_Body
- and then not Acts_As_Spec (Parent (Lib_Unit)))
+ and then not Acts_As_Spec (Parent (Lib_Unit)))
then
null;
if Nkind (Lib_Unit) = N_Package_Body
or else (Nkind (Lib_Unit) = N_Subprogram_Body
- and then not Acts_As_Spec (N))
+ and then not Acts_As_Spec (N))
then
Install_Context (Library_Unit (N));
-- Check all the enclosing scopes.
E2 := E;
- while E2 /= Standard_Standard
- and then E2 /= WEnt
- loop
+ while E2 /= Standard_Standard and then E2 /= WEnt loop
E2 := Scope (E2);
end loop;
Check_Private_Limited_Withed_Unit (Item);
- if not Implicit_With (Item)
- and then Is_Child_Spec (Unit (N))
- then
+ if not Implicit_With (Item) and then Is_Child_Spec (Unit (N)) then
Check_Renamings (Parent_Spec (Unit (N)), Item);
end if;
or else Nkind (Original_Node (Lib_Unit)) in N_Generic_Instantiation
or else
(Nkind (Lib_Unit) = N_Package_Declaration
- and then Present (Generic_Parent (Specification (Lib_Unit))))
+ and then Present (Generic_Parent (Specification (Lib_Unit))))
then
null;
else
Set_Use (Generic_Formal_Declarations (Parent (P_Spec)));
end if;
- if Is_Private
- or else Private_Present (Parent (Lib_Unit))
- then
+ if Is_Private or else Private_Present (Parent (Lib_Unit)) then
Install_Private_Declarations (P_Name);
Install_Private_With_Clauses (P_Name);
Set_Use (Private_Declarations (P_Spec));
-- Replace E in the homonyms list, so that the limited view
-- becomes available.
- if E = Non_Limited_View (Lim_Typ) then
+ -- If the non-limited view is a record with an anonymous
+ -- self-referential component, the analysis of the record
+ -- declaration creates an incomplete type with the same name
+ -- in order to define an internal access type. The visible
+ -- entity is now the incomplete type, and that is the one to
+ -- replace in the visibility structure.
+
+ if E = Non_Limited_View (Lim_Typ)
+ or else
+ (Ekind (E) = E_Incomplete_Type
+ and then Full_View (E) = Non_Limited_View (Lim_Typ))
+ then
Set_Homonym (Lim_Typ, Homonym (Prev));
Set_Current_Entity (Lim_Typ);
-- limited_with_clause.
exit when No (E);
-
exit when E = Non_Limited_View (Lim_Typ);
-
Prev := Homonym (Prev);
end loop;
if Sloc (Uname) /= No_Location
and then (not Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
- or else Current_Sem_Unit = Main_Unit)
+ or else Current_Sem_Unit = Main_Unit)
then
Check_Restricted_Unit
(Unit_Name (Get_Source_Unit (Uname)), With_Clause);
begin
U2 := Homonym (Uname);
- while Present (U2)
- and then U2 /= Standard_Standard
- loop
+ while Present (U2) and then U2 /= Standard_Standard loop
P2 := Scope (U2);
Decl2 := Unit_Declaration_Node (P2);
Ent : Entity_Id;
begin
- if Is_Subprogram (E)
- and then Has_Pragma_Inline (E)
- then
+ if Is_Subprogram (E) and then Has_Pragma_Inline (E) then
return True;
elsif Ekind_In (E, E_Generic_Function, E_Generic_Procedure) then
begin
Item := First (Context_Items (Comp_Unit));
while Present (Item) loop
- if Nkind (Item) = N_With_Clause
- and then Private_Present (Item)
- then
+ if Nkind (Item) = N_With_Clause and then Private_Present (Item) then
+
-- If private_with_clause is redundant, remove it from context,
-- as a small optimization to subsequent handling of private_with
-- clauses in other nested packages.
Set_Name_Entity_Id (Chars (E), Homonym (E));
else
- while Present (Prev)
- and then Homonym (Prev) /= E
- loop
+ while Present (Prev) and then Homonym (Prev) /= E loop
Prev := Homonym (Prev);
end loop;
-- Abstract_State
- when Aspect_Abstract_State =>
- Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Abstract_State);
+ when Aspect_Abstract_State => Abstract_State : declare
+ Decls : List_Id;
+ Spec : Node_Id;
+
+ begin
+ -- Aspect Abstract_State introduces implicit declarations
+ -- for all state abstraction entities it defines. To emulate
+ -- this behavior, insert the pragma at the beginning of the
+ -- visible declarations of the related package so that it is
+ -- analyzed immediately.
+
+ if Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Spec := Specification (N);
+ Decls := Visible_Declarations (Spec);
+
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Abstract_State);
+ Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Visible_Declarations (N, Decls);
+ end if;
+
+ Prepend_To (Decls, Aitem);
+
+ else
+ Error_Msg_NE
+ ("aspect & must apply to a package declaration",
+ Aspect, Id);
+ end if;
+
+ goto Continue;
+ end Abstract_State;
-- Depends
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_Pre);
+ -- Refined_State
+
+ when Aspect_Refined_State => Refined_State : declare
+ Decls : List_Id;
+
+ begin
+ -- The corresponding pragma for Refined_State is inserted in
+ -- the declarations of the related package body. This action
+ -- synchronizes both the source and from-aspect versions of
+ -- the pragma.
+
+ if Nkind (N) = N_Package_Body then
+ Decls := Declarations (N);
+
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Refined_State);
+ Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (N, Decls);
+ end if;
+
+ Prepend_To (Decls, Aitem);
+
+ else
+ Error_Msg_NE
+ ("aspect & must apply to a package body", Aspect, Id);
+ end if;
+
+ goto Continue;
+ end Refined_State;
+
-- Relative_Deadline
when Aspect_Relative_Deadline =>
Set_From_Aspect_Specification (Aitem, True);
end if;
- -- Aspect Abstract_State introduces implicit declarations for all
- -- state abstraction entities it defines. To emulate this behavior
- -- insert the pragma at the start of the visible declarations of
- -- the related package.
-
- if Nam = Name_Abstract_State
- and then Nkind (N) = N_Package_Declaration
- then
- if No (Visible_Declarations (Specification (N))) then
- Set_Visible_Declarations (Specification (N), New_List);
- end if;
-
- Prepend (Aitem, Visible_Declarations (Specification (N)));
- goto Continue;
-
-- In the context of a compilation unit, we directly put the
-- pragma in the Pragmas_After list of the N_Compilation_Unit_Aux
-- node (no delay is required here) except for aspects on a
-- copy (see sem_ch12), and for package instantiations, where
-- the library unit pragmas are better handled early.
- elsif Nkind (Parent (N)) = N_Compilation_Unit
+ if Nkind (Parent (N)) = N_Compilation_Unit
and then (Present (Aitem) or else Is_Boolean_Aspect (Aspect))
then
declare
Aspect_Refined_Global |
Aspect_Refined_Post |
Aspect_Refined_Pre |
+ Aspect_Refined_State |
Aspect_SPARK_Mode |
Aspect_Test_Case =>
raise Program_Error;
with Sem_Elim; use Sem_Elim;
with Sem_Eval; use Sem_Eval;
with Sem_Mech; use Sem_Mech;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Smem; use Sem_Smem;
with Sem_Type; use Sem_Type;
-- Local variables
+ Body_Id : Entity_Id;
+ Context : Node_Id;
Freeze_From : Entity_Id := Empty;
Next_Decl : Node_Id;
+ Spec_Id : Entity_Id;
-- Start of processing for Analyze_Declarations
Decl := Next_Decl;
end loop;
+ -- Analyze the state refinements within a package body now, after all
+ -- hidden states have been encountered and freely visible. Refinements
+ -- must be processed before pragmas Refined_Depends and Refined_Global
+ -- because the last two may mention constituents.
+
+ if Present (L) then
+ Context := Parent (L);
+
+ if Nkind (Context) = N_Package_Body then
+ Body_Id := Defining_Entity (Context);
+ Spec_Id := Corresponding_Spec (Context);
+
+ -- The analysis of pragma Refined_State detects whether the spec
+ -- has abstract states available for refinement.
+
+ if Present (Refined_State_Pragma (Body_Id)) then
+ Analyze_Refined_State_In_Decl_Part
+ (Refined_State_Pragma (Body_Id));
+
+ -- State refinement is required when the package declaration has
+ -- abstract states. Null states are not considered.
+
+ elsif Present (Abstract_States (Spec_Id))
+ and then not Has_Null_Abstract_State (Spec_Id)
+ then
+ Error_Msg_NE
+ ("package & requires state refinement", Context, Spec_Id);
+ end if;
+ end if;
+ end if;
+
-- Analyze the contracts of a subprogram declaration or a body now due
-- to delayed visibility requirements of aspects.
-------------------------------------
procedure Add_Item (Item : Entity_Id; To_List : in out Elist_Id);
- -- Subsidiary routine to the analysis of pragmas Depends and Global. Append
- -- an input or output item to a list. If the list is empty, a new one is
- -- created.
+ -- Subsidiary routine to the analysis of pragmas Depends, Global and
+ -- Refined_State. Append an entity to a list. If the list is empty, create
+ -- a new list.
function Adjust_External_Name_Case (N : Node_Id) return Node_Id;
-- This routine is used for possible casing adjustment of an explicit
To_List := New_Elmt_List;
end if;
- Append_Unique_Elmt (Item, To_List);
+ Append_Elmt (Item, To_List);
end Add_Item;
-------------------------------
Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
All_Cases : Node_Id;
CCase : Node_Id;
- Restore : Boolean := False;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
+ Restore_Scope : Boolean := False;
+ -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
+
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
begin
-- for subprogram bodies because the formals are already visible.
if Requires_Profile_Installation (N, Subp_Decl) then
- Restore := True;
+ Restore_Scope := True;
Push_Scope (Subp_Id);
Install_Formals (Subp_Id);
end if;
Next (CCase);
end loop;
- if Restore then
+ if Restore_Scope then
End_Scope;
end if;
end if;
Set_Parent (Id, State);
Set_Ekind (Id, E_Abstract_State);
Set_Etype (Id, Standard_Void_Type);
- Set_Refined_State (Id, Empty);
-- Every non-null state must be nameable and resolvable the
-- same way a constant is.
-- Local variables
- Par : Node_Id;
- State : Node_Id;
+ Context : constant Node_Id := Parent (Parent (N));
+ State : Node_Id;
-- Start of processing for Abstract_State
-- Ensure the proper placement of the pragma. Abstract states must
-- be associated with a package declaration.
- if From_Aspect_Specification (N) then
- Par := Parent (Corresponding_Aspect (N));
- else
- Par := Parent (Parent (N));
- end if;
-
- if Nkind (Par) = N_Compilation_Unit then
- Par := Unit (Par);
- end if;
-
- if not Nkind_In (Par, N_Generic_Package_Declaration,
- N_Package_Declaration)
+ if not Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
then
Pragma_Misplaced;
return;
end if;
- Pack_Id := Defining_Entity (Par);
+ Pack_Id := Defining_Entity (Context);
State := Expression (Arg1);
-- Multiple abstract states appear as an aggregate
when Pragma_Refined_Pre =>
Analyze_Refined_Pre_Post_Condition;
+ -------------------
+ -- Refined_State --
+ -------------------
+
+ -- pragma Refined_State (REFINEMENT_LIST);
+
+ -- REFINEMENT_LIST ::=
+ -- REFINEMENT_CLAUSE
+ -- | (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE})
+
+ -- REFINEMENT_CLAUSE ::= state_NAME => CONSTITUENT_LIST
+
+ -- CONSTITUENT_LIST ::=
+ -- null
+ -- | CONSTITUENT
+ -- | (CONSTITUENT {, CONSTITUENT})
+
+ -- CONSTITUENT ::= object_NAME | state_NAME
+
+ when Pragma_Refined_State => Refined_State : declare
+ Context : constant Node_Id := Parent (N);
+ Spec_Id : Entity_Id;
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Refined states must
+ -- be associated with a package body.
+
+ if Nkind (Context) /= N_Package_Body then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ -- State refinement is allowed only when the corresponding package
+ -- declaration has a non-null aspect/pragma Abstract_State.
+
+ Spec_Id := Corresponding_Spec (Context);
+
+ if No (Abstract_States (Spec_Id))
+ or else Has_Null_Abstract_State (Spec_Id)
+ then
+ Error_Pragma
+ ("useless pragma %, package does not define abstract states");
+ return;
+ end if;
+
+ -- The pragma must be analyzed at the end of the declarations as
+ -- it has visibility over the whole declarative region. Save the
+ -- pragma for later (see Analyze_Refined_Depends_In_Decl_Part).
+
+ Set_Refined_State_Pragma (Defining_Entity (Context), N);
+ end Refined_State;
+
-----------------------
-- Relative_Deadline --
-----------------------
(Prag : Node_Id;
Subp_Id : Entity_Id)
is
- Arg1 : constant Node_Id :=
- First (Pragma_Argument_Associations (Prag));
- Expr : Node_Id;
- Restore : Boolean := False;
+ Arg1 : constant Node_Id := First (Pragma_Argument_Associations (Prag));
+ Expr : Node_Id;
+
+ Restore_Scope : Boolean := False;
+ -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
begin
-- Ensure that the subprogram and its formals are visible when analyzing
-- the expression of the pragma.
if Current_Scope /= Subp_Id then
- Restore := True;
+ Restore_Scope := True;
Push_Scope (Subp_Id);
Install_Formals (Subp_Id);
end if;
-- Remove the subprogram from the scope stack now that the pre-analysis
-- of the precondition/postcondition is done.
- if Restore then
+ if Restore_Scope then
End_Scope;
end if;
end Analyze_Pre_Post_Condition_In_Decl_Part;
null;
end Analyze_Refined_Global_In_Decl_Part;
+ ----------------------------------------
+ -- Analyze_Refined_State_In_Decl_Part --
+ ----------------------------------------
+
+ procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id) is
+ Pack_Body : constant Node_Id := Parent (N);
+ Spec_Id : constant Entity_Id := Corresponding_Spec (Pack_Body);
+
+ Abstr_States : Elist_Id := No_Elist;
+ -- A list of all abstract states defined in the package declaration. The
+ -- list is used to report unrefined states.
+
+ Constituents_Seen : Elist_Id := No_Elist;
+ -- A list that contains all constituents processed so far. The list is
+ -- used to detect multiple uses of the same constituent.
+
+ Hidden_States : Elist_Id := No_Elist;
+ -- A list of all hidden states (abstract states and variables) that
+ -- appear in the package spec and body. The list is used to report
+ -- unused hidden states.
+
+ Refined_States_Seen : Elist_Id := No_Elist;
+ -- A list that contains all refined states processed so far. The list is
+ -- used to detect duplicate refinements.
+
+ procedure Analyze_Refinement_Clause (Clause : Node_Id);
+ -- Perform full analysis of a single refinement clause
+
+ function Collect_Hidden_States return Elist_Id;
+ -- Gather the entities of all hidden states that appear in the spec and
+ -- body of the related package.
+
+ procedure Report_Unrefined_States;
+ -- Emit errors for all abstract states that have not been refined by
+ -- the pragma.
+
+ procedure Report_Unused_Hidden_States;
+ -- Emit errors for all hidden states of the related package that do not
+ -- participate in a refinement.
+
+ -------------------------------
+ -- Analyze_Refinement_Clause --
+ -------------------------------
+
+ procedure Analyze_Refinement_Clause (Clause : Node_Id) is
+ Non_Null_Seen : Boolean := False;
+ Null_Seen : Boolean := False;
+ -- Flags used to detect multiple uses of null in a single clause or a
+ -- mixture of null and non-null constituents.
+
+ procedure Analyze_Constituent (Constit : Node_Id);
+ -- Perform full analysis of a single constituent
+
+ procedure Check_Matching_State
+ (State : Node_Id;
+ State_Id : Entity_Id);
+ -- Determine whether state State denoted by its name State_Id appears
+ -- in Abstr_States. Emit an error when attempting to re-refine the
+ -- state or when the state is not defined in the package declaration.
+ -- Otherwise remove the state from Abstr_States.
+
+ -------------------------
+ -- Analyze_Constituent --
+ -------------------------
+
+ procedure Analyze_Constituent (Constit : Node_Id) is
+ procedure Check_Matching_Constituent (Constit_Id : Entity_Id);
+ -- Determine whether constituent Constit denoted by its entity
+ -- Constit_Id appears in Hidden_States. Emit an error when the
+ -- constituent is not a valid hidden state of the related package
+ -- or when it is used more than once. Otherwise remove the
+ -- constituent from Hidden_States.
+
+ --------------------------------
+ -- Check_Matching_Constituent --
+ --------------------------------
+
+ procedure Check_Matching_Constituent (Constit_Id : Entity_Id) is
+ State_Elmt : Elmt_Id;
+
+ begin
+ -- Detect a duplicate use of a constituent
+
+ if Contains (Constituents_Seen, Constit_Id) then
+ Error_Msg_NE
+ ("duplicate use of constituent &", Constit, Constit_Id);
+ return;
+ end if;
+
+ -- Inspect the hidden states of the related package looking for
+ -- a match.
+
+ State_Elmt := First_Elmt (Hidden_States);
+ while Present (State_Elmt) loop
+
+ -- A valid hidden state or variable participates in a
+ -- refinement. Add the constituent to the list of processed
+ -- items to aid with the detection of duplicate constituent
+ -- use. Remove the constituent from Hidden_States to signal
+ -- that it has already been used.
+
+ if Node (State_Elmt) = Constit_Id then
+ Add_Item (Constit_Id, Constituents_Seen);
+ Remove_Elmt (Hidden_States, State_Elmt);
+
+ return;
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+
+ -- If we get here, we are refining a state that is not hidden
+ -- with respect to the related package.
+
+ Error_Msg_Name_1 := Chars (Spec_Id);
+ Error_Msg_NE
+ ("cannot use & in refinement, constituent is not a hidden "
+ & "state of package %", Constit, Constit_Id);
+ end Check_Matching_Constituent;
+
+ -- Local variables
+
+ Constit_Id : Entity_Id;
+
+ -- Start of processing for Analyze_Constituent
+
+ begin
+ -- Detect multiple uses of null in a single refinement clause or a
+ -- mixture of null and non-null constituents.
+
+ if Nkind (Constit) = N_Null then
+ if Null_Seen then
+ Error_Msg_N
+ ("multiple null constituents not allowed", Constit);
+
+ elsif Non_Null_Seen then
+ Error_Msg_N
+ ("cannot mix null and non-null constituents", Constit);
+
+ else
+ Null_Seen := True;
+ end if;
+
+ -- Non-null constituents
+
+ else
+ Non_Null_Seen := True;
+
+ if Null_Seen then
+ Error_Msg_N
+ ("cannot mix null and non-null constituents", Constit);
+ end if;
+
+ Analyze (Constit);
+
+ -- Ensure that the constituent denotes a valid state or a
+ -- whole variable.
+
+ if Is_Entity_Name (Constit) then
+ Constit_Id := Entity (Constit);
+
+ if Ekind_In (Constit_Id, E_Abstract_State, E_Variable) then
+ Check_Matching_Constituent (Constit_Id);
+ else
+ Error_Msg_NE
+ ("constituent & must denote a variable or state",
+ Constit, Constit_Id);
+ end if;
+
+ -- The constituent is illegal
+
+ else
+ Error_Msg_N ("malformed constituent", Constit);
+ end if;
+ end if;
+ end Analyze_Constituent;
+
+ --------------------------
+ -- Check_Matching_State --
+ --------------------------
+
+ procedure Check_Matching_State
+ (State : Node_Id;
+ State_Id : Entity_Id)
+ is
+ State_Elmt : Elmt_Id;
+
+ begin
+ -- Detect a duplicate refinement of a state
+
+ if Contains (Refined_States_Seen, State_Id) then
+ Error_Msg_NE
+ ("duplicate refinement of state &", State, State_Id);
+ return;
+ end if;
+
+ -- Inspect the abstract states defined in the package declaration
+ -- looking for a match.
+
+ State_Elmt := First_Elmt (Abstr_States);
+ while Present (State_Elmt) loop
+
+ -- A valid abstract state is being refined in the body. Add
+ -- the state to the list of processed refined states to aid
+ -- with the detection of duplicate refinements. Remove the
+ -- state from Abstr_States to signal that it has already been
+ -- refined.
+
+ if Node (State_Elmt) = State_Id then
+ Add_Item (State_Id, Refined_States_Seen);
+ Remove_Elmt (Abstr_States, State_Elmt);
+
+ return;
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+
+ -- If we get here, we are refining a state that is not defined in
+ -- the package declaration.
+
+ Error_Msg_Name_1 := Chars (Spec_Id);
+ Error_Msg_NE
+ ("cannot refine state, & is not defined in package %",
+ State, State_Id);
+ end Check_Matching_State;
+
+ -- Local declarations
+
+ Constit : Node_Id;
+ State : Node_Id;
+ State_Id : Entity_Id := Empty;
+
+ -- Start of processing for Analyze_Refinement_Clause
+
+ begin
+ -- Analyze the state name of a refinement clause
+
+ State := First (Choices (Clause));
+ while Present (State) loop
+ if Present (State_Id) then
+ Error_Msg_N
+ ("refinement clause cannot cover multiple states", State);
+
+ else
+ Analyze (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);
+
+ -- Catch any attempts to re-refine a state or refine a
+ -- state that is not defined in the package declaration.
+
+ if Ekind (State_Id) = E_Abstract_State then
+ Check_Matching_State (State, State_Id);
+ else
+ Error_Msg_NE
+ ("& must denote an abstract state", State, State_Id);
+ end if;
+
+ -- The state name is illegal
+
+ else
+ Error_Msg_N
+ ("malformed state name in refinement clause", State);
+ end if;
+ end if;
+
+ Next (State);
+ end loop;
+
+ -- Analyze all constituents of the refinement. Multiple constituents
+ -- appear as an aggregate.
+
+ Constit := Expression (Clause);
+
+ if Nkind (Constit) = N_Aggregate then
+ if Present (Component_Associations (Constit)) then
+ Error_Msg_N
+ ("constituents of refinement clause must appear in "
+ & "positional form", Constit);
+
+ else pragma Assert (Present (Expressions (Constit)));
+ Constit := First (Expressions (Constit));
+ while Present (Constit) loop
+ Analyze_Constituent (Constit);
+
+ Next (Constit);
+ end loop;
+ end if;
+
+ -- Various forms of a single constituent. Note that these may include
+ -- malformed constituents.
+
+ else
+ Analyze_Constituent (Constit);
+ end if;
+ end Analyze_Refinement_Clause;
+
+ ---------------------------
+ -- Collect_Hidden_States --
+ ---------------------------
+
+ function Collect_Hidden_States return Elist_Id is
+ Result : Elist_Id := No_Elist;
+
+ procedure Collect_Hidden_States_In_Decls (Decls : List_Id);
+ -- Find all hidden states that appear in declarative list Decls and
+ -- append their entities to Result.
+
+ ------------------------------------
+ -- Collect_Hidden_States_In_Decls --
+ ------------------------------------
+
+ procedure Collect_Hidden_States_In_Decls (Decls : List_Id) is
+ procedure Collect_Abstract_States (States : Elist_Id);
+ -- Copy the abstract states defined in list States to list Result
+
+ -----------------------------
+ -- Collect_Abstract_States --
+ -----------------------------
+
+ procedure Collect_Abstract_States (States : Elist_Id) is
+ State_Elmt : Elmt_Id;
+
+ begin
+ State_Elmt := First_Elmt (States);
+ while Present (State_Elmt) loop
+ Add_Item (Node (State_Elmt), Result);
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end Collect_Abstract_States;
+
+ -- Local variables
+
+ Decl : Node_Id;
+
+ -- Start of processing for Collect_Hidden_States_In_Decls
+
+ begin
+ Decl := First (Decls);
+ while Present (Decl) loop
+
+ -- Objects (non-constants) are valid hidden states
+
+ if Nkind (Decl) = N_Object_Declaration
+ and then not Constant_Present (Decl)
+ then
+ Add_Item (Defining_Entity (Decl), Result);
+
+ -- Gather the abstract states of a package along with all
+ -- hidden states in its visible declarations.
+
+ elsif Nkind (Decl) = N_Package_Declaration then
+ Collect_Abstract_States
+ (Abstract_States (Defining_Entity (Decl)));
+
+ Collect_Hidden_States_In_Decls
+ (Visible_Declarations (Specification (Decl)));
+ end if;
+
+ Next (Decl);
+ end loop;
+ end Collect_Hidden_States_In_Decls;
+
+ -- Local variables
+
+ Pack_Spec : constant Node_Id := Parent (Spec_Id);
+
+ -- Start of processing for Collect_Hidden_States
+
+ begin
+ -- Process the private declarations of the package spec and the
+ -- declarations of the body.
+
+ Collect_Hidden_States_In_Decls (Private_Declarations (Pack_Spec));
+ Collect_Hidden_States_In_Decls (Declarations (Pack_Body));
+
+ return Result;
+ end Collect_Hidden_States;
+
+ -----------------------------
+ -- Report_Unrefined_States --
+ -----------------------------
+
+ procedure Report_Unrefined_States is
+ State_Elmt : Elmt_Id;
+
+ begin
+ if Present (Abstr_States) then
+ State_Elmt := First_Elmt (Abstr_States);
+ while Present (State_Elmt) loop
+ Error_Msg_N
+ ("abstract state & must be refined", Node (State_Elmt));
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end Report_Unrefined_States;
+
+ ---------------------------------
+ -- Report_Unused_Hidden_States --
+ ---------------------------------
+
+ procedure Report_Unused_Hidden_States is
+ Posted : Boolean := False;
+ State_Elmt : Elmt_Id;
+ State_Id : Entity_Id;
+
+ begin
+ if Present (Hidden_States) then
+ State_Elmt := First_Elmt (Hidden_States);
+ while Present (State_Elmt) loop
+ State_Id := Node (State_Elmt);
+
+ -- Generate an error message of the form:
+
+ -- package ... has unused hidden states
+ -- abstract state ... defined at ...
+ -- variable ... defined at ...
+
+ if not Posted then
+ Posted := True;
+ Error_Msg_NE
+ ("package & has unused hidden states", N, Spec_Id);
+ end if;
+
+ Error_Msg_Sloc := Sloc (State_Id);
+
+ if Ekind (State_Id) = E_Abstract_State then
+ Error_Msg_NE ("\ abstract state & defined #", N, State_Id);
+ else
+ Error_Msg_NE ("\ variable & defined #", N, State_Id);
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end Report_Unused_Hidden_States;
+
+ -- Local declarations
+
+ Clauses : constant Node_Id :=
+ Expression (First (Pragma_Argument_Associations (N)));
+ Clause : Node_Id;
+
+ -- Start of processing for Analyze_Refined_State_In_Decl_Part
+
+ begin
+ Set_Analyzed (N);
+
+ -- Initialize the various lists used during analysis
+
+ Abstr_States := Clone (Abstract_States (Spec_Id));
+ Hidden_States := Collect_Hidden_States;
+
+ -- Multiple state refinements appear as an aggregate
+
+ if Nkind (Clauses) = N_Aggregate then
+ if Present (Expressions (Clauses)) then
+ Error_Msg_N
+ ("state refinements must appear as component associations",
+ Clauses);
+
+ else pragma Assert (Present (Component_Associations (Clauses)));
+ Clause := First (Component_Associations (Clauses));
+ while Present (Clause) loop
+ Analyze_Refinement_Clause (Clause);
+
+ Next (Clause);
+ end loop;
+ end if;
+
+ -- Various forms of a single state refinement. Note that these may
+ -- include malformed refinements.
+
+ else
+ Analyze_Refinement_Clause (Clauses);
+ end if;
+
+ -- Ensure that all abstract states have been refined and all hidden
+ -- states of the related package unilized in refinements.
+
+ Report_Unrefined_States;
+ Report_Unused_Hidden_States;
+ end Analyze_Refined_State_In_Decl_Part;
+
------------------------------------
-- Analyze_Test_Case_In_Decl_Part --
------------------------------------
Pragma_Refined_Global => -1,
Pragma_Refined_Post => -1,
Pragma_Refined_Pre => -1,
+ Pragma_Refined_State => -1,
Pragma_Relative_Deadline => -1,
Pragma_Remote_Access_Type => -1,
Pragma_Remote_Call_Interface => -1,
procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Refined_Global
+ procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Refined_State
+
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id);
-- Perform preanalysis of pragma Test_Case that applies to a subprogram
-- declaration. Parameter N denotes the pragma, S is the entity of the
Name_Refined_Global : constant Name_Id := N + $; -- GNAT
Name_Refined_Post : constant Name_Id := N + $; -- GNAT
Name_Refined_Pre : constant Name_Id := N + $; -- GNAT
+
+ -- Kirchev
+
+ Name_Refined_State : constant Name_Id := N + $; -- GNAT
Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05
Name_Remote_Access_Type : constant Name_Id := N + $; -- GNAT
Name_Remote_Call_Interface : constant Name_Id := N + $;
Pragma_Refined_Global,
Pragma_Refined_Post,
Pragma_Refined_Pre,
+ Pragma_Refined_State,
Pragma_Relative_Deadline,
Pragma_Remote_Access_Type,
Pragma_Remote_Call_Interface,
projects / gcc.git / commitdiff