+2015-10-26 Bob Duff <duff@adacore.com>
+
+ * exp_ch7.adb, exp_ch6.adb: Minor comment fix.
+
+2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb (Move_Or_Merge_Aspects): Move all aspects related
+ to a single concurrent type declaration to the declaration
+ of the anonymous object if they qualify.
+ (Relocate_Aspect): Update comment on usage.
+ * aspects.ads Add new sectioon on aspect specifications on single
+ concurrent types. Add new table Aspect_On_Anonymous_Object_OK.
+ (Move_Or_Merge_Aspects): Udate the comment on usage.
+ * atree.adb (Elist36): New routine.
+ (Set_Elist36): New routine.
+ * atree.ads (Elist36): New routine along with pragma Inline.
+ (Set_Elist36): New routine along with pragma Inline.
+ * atree.h: Elist36 is now an alias for Field36.
+ * contracts.adb (Add_Contract_Item): Add processing
+ for protected units and extra processing for variables.
+ (Analyze_Object_Contract): Code cleanup. The processing of
+ Part_Of now depends on wherer the object is a constant or
+ a variable. Add processing for pragmas Depends and Global
+ when they apply to a single concurrent object. Verify that a
+ variable which is part of a single concurrent type has full
+ default initialization. Set/restore the SPARK_Mode of a single
+ concurrent object.
+ (Analyze_Protected_Contract): New routine.
+ * contracts.ads (Add_Contract_Item): Update the comment on usage.
+ (Analyze_Object_Contract): Update the comment on usage.
+ (Analyze_Protected_Contract): New routine.
+ (Analyze_Task_Contract): Update the comment on usage.
+ * einfo.adb Part_Of_Constituents now uses Elist10.
+ (Anonymous_Object): New routine.
+ (Contract): Code cleanup.
+ (Has_Option): Remove the assumption that the only simple
+ option is External.
+ (Is_Synchronized_State): New routine.
+ (Part_Of_Constituents): This attribute applies to
+ variables and uses Elist10.
+ (Set_Anonymous_Object): New routine.
+ (Set_Contract): Code cleanup.
+ (Set_Part_Of_Constituents): This attribute applies to variables and
+ uses Elist10.
+ (Set_SPARK_Aux_Pragma): Code cleanup.
+ (Set_SPARK_Aux_Pragma_Inherited): Code cleanup.
+ (Set_SPARK_Pragma): Code cleanup. This attribute applies to
+ variables.
+ (Set_SPARK_Pragma_Inherited): Code cleanup. This
+ attribute applies to variables.
+ (SPARK_Aux_Pragma): Code cleanup.
+ (SPARK_Aux_Pragma_Inherited): Code cleanup.
+ (SPARK_Pragma): Code cleanup. This attribute applies to variables.
+ (SPARK_Pragma_Inherited): Code cleanup. This attribute applies
+ to variables.
+ (Write_Field9_Name): Remove the output for Part_Of_Constituents.
+ (Write_Field10_Name): Add output for Part_Of_Constituents.
+ (Write_Field30_Name): Add output for Anonymous_Object.
+ (Write_Field34_Name): Output SPARK_Pragma
+ for protected types and variables.
+ * einfo.ads: New attributes Anonymous_Object and
+ Is_Synchronized_State along with usage in entities. Update
+ the documentation of attributes Contract Encapsulating_State
+ Part_Of_Constituents SPARK_Aux_Pragma SPARK_Aux_Pragma_Inherited
+ SPARK_Pragma SPARK_Pragma_Inherited (Anonymous_Object): New
+ routine along with pragma Inline.
+ (Is_Synchronized_State): New routine.
+ (Set_Anonymous_Object): New routine along with pragma Inline.
+ * freeze.adb (Freeze_Record_Type): Ensure that a non-synchronized
+ record does not have synchronized components.
+ * sem_ch3.adb (Analyze_Declarations): Code cleanup. Analyze the
+ contract of protected units.
+ * sem_ch9.adb Add with and use clauses for Sem_Prag. Code cleanup.
+ (Analyze_Single_Protected_Declaration): Reimplemented.
+ (Analyze_Single_Task_Declaration): Reimplemented.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Aspect Part_Of
+ can now apply to a single concurrent type declaration. Rely on
+ Insert_Pragma to place the pragma. Update the error message on
+ usage to reflect the new context.
+ (Insert_Pragma): When inserting
+ pragmas for a protected or task type, create a definition if
+ the type lacks one.
+ * sem_elab.adb (Check_A_Call): Code cleanup. Issue error message
+ related to elaboration issues for SPARK when SPARK_Mode is "on"
+ and the offending entity comes from source.
+ * sem_prag.adb (Analyze_Abstract_State): Add new flag
+ Synchronous_Seen. Update the analysis of simple options Externa,
+ Ghost and Synchronous. Update various error messages to reflect
+ the use of single concurrent types.
+ (Analyze_Depends_Global): Pragmas Depends and Global can now apply to
+ a single task type or a single concurrent object created for a task
+ type.
+ (Analyze_Depends_In_Decl_Part): Do not push a scope when the
+ context is a single concurrent object. (Analyze_Part_Of):
+ Moved out of Analyze_Pragma. The routine has a new profile
+ and comment on usage.
+ (Analyze_Part_Of_In_Decl_Part): New routine.
+ (Analyze_Part_Of_Option): Update the call to Analyze_Part_Of.
+ (Analyze_Pragma): Pragma Abstract_State can
+ now carry simple option Synchronous. Pragma Part_Of can now
+ apply to a single concurrent type declaration. The analysis
+ of pragma Part_Of is delayed when the context is a single
+ concurrent object.
+ (Analyze_Refined_Depends_In_Decl_Part): Use the anonymous object when
+ the context is a single concurren type.
+ (Analyze_Refined_Global_In_Decl_Part): Use the
+ anonymous object when the context is a single concurren type.
+ (Check_Ghost_Constituent): Removed.
+ (Check_Matching_Constituent): Renamed to Match_Constituent.
+ (Check_Matching_State): Renamed to Match_State.
+ (Collect_Constituent): Update the comment
+ on usage. Verify various legality rules related to ghost and
+ synchronized entities.
+ (Find_Related_Declaration_Or_Body): A single task declaration is no
+ longer a valid context for a pragma.
+ (Fix_Msg): Moved to Sem_Util.
+ (Process_Overloadable): Add processing for single task objects.
+ (Process_Visible_Part): Add processing for single concurrent
+ types.
+ (Relocate_Pragmas_To_Anonymous_Object): New routine.
+ * sem_prag.ads Add new table Pragma_On_Anonymous_Object_OK.
+ (Analyze_Part_Of_In_Decl_Part): New routine.
+ (Relocate_Pragmas_To_Anonymous_Object): New routine.
+ * sem_util.adb (Defining_Entity): Code cleanup.
+ (Fix_Msg): Moved from Sem_Prag and augmented to handle
+ mode replacements.
+ (Has_Full_Default_Initialization): New routine.
+ (Is_Descendant_Of_Suspension_Object): Moved out of
+ Is_Effectively_Volatile.
+ (Is_Single_Concurrent_Object): New routine.
+ (Is_Single_Concurrent_Type): New routine.
+ (Is_Single_Concurrent_Type_Declaration): New routine.
+ (Is_Synchronized_Object): New routine.
+ (Yields_Synchronized_Object): New routine.
+ * sem_util.ads (Fix_Msg): Moved form Sem_Prag. Update the
+ comment on usage.
+ (Has_Full_Default_Initialization): New routine.
+ (Is_Single_Concurrent_Object): New routine.
+ (Is_Single_Concurrent_Type): New routine.
+ (Is_Single_Concurrent_Type_Declaration): New routine.
+ (Is_Synchronized_Object): New routine.
+ (Yields_Synchronized_Object): New routine.
+ * snames.ads-tmpl: Add name Synchronous.
+
2015-10-26 Jerome Lambourg <lambourg@adacore.com>
* sysdep.c (__gnat_get_task_options): Refine the workaround for
procedure Move_Or_Merge_Aspects (From : Node_Id; To : Node_Id) is
procedure Relocate_Aspect (Asp : Node_Id);
- -- Asp denotes an aspect specification of node From. Relocate the Asp to
- -- the aspect specifications of node To (if any).
+ -- Move aspect specification Asp to the aspect specifications of node To
---------------------
-- Relocate_Aspect --
Set_Has_Aspects (To);
end if;
- -- Remove the aspect from node From's aspect specifications and
- -- append it to node To.
+ -- Remove the aspect from its original owner and relocate it to node
+ -- To.
Remove (Asp);
Append (Asp, Asps);
Relocate_Aspect (Asp);
end if;
+ -- When moving or merging aspects from a single concurrent type
+ -- declaration, relocate only those aspects that may apply to the
+ -- anonymous object created for the type.
+
+ -- Note: It is better to use Is_Single_Concurrent_Type_Declaration
+ -- here, but Aspects and Sem_Util have incompatible licenses.
+
+ elsif Nkind_In
+ (Original_Node (From), N_Single_Protected_Declaration,
+ N_Single_Task_Declaration)
+ then
+ Asp_Id := Get_Aspect_Id (Asp);
+
+ if Aspect_On_Anonymous_Object_OK (Asp_Id) then
+ Relocate_Aspect (Asp);
+ end if;
+
-- Default case - relocate the aspect to its new owner
else
-- package body P with SPARK_Mode is ...;
-- The table should be synchronized with Pragma_On_Body_Or_Stub_OK in unit
- -- Sem_Prag if the aspects below are implemented by a pragma.
+ -- Sem_Prag.
Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean :=
(Aspect_Refined_Depends => True,
Aspect_Warnings => True,
others => False);
+ -------------------------------------------------------------------
+ -- Handling of Aspects Specifications on Single Concurrent Types --
+ -------------------------------------------------------------------
+
+ -- Certain aspects that appear on the following nodes
+
+ -- N_Single_Protected_Declaration
+ -- N_Single_Task_Declaration
+
+ -- are treated as if they apply to the anonymous object produced by the
+ -- analysis of a single concurrent type. The following table lists all
+ -- aspects that should apply to the anonymous object. The table should
+ -- be synchronized with Pragma_On_Anonymous_Object_OK in unit Sem_Prag.
+
+ Aspect_On_Anonymous_Object_OK : constant array (Aspect_Id) of Boolean :=
+ (Aspect_Depends => True,
+ Aspect_Global => True,
+ Aspect_Part_Of => True,
+ others => False);
+
---------------------------------------------------
-- Handling of Aspect Specifications in the Tree --
---------------------------------------------------
procedure Move_Or_Merge_Aspects (From : Node_Id; To : Node_Id);
-- Relocate the aspect specifications of node From to node To. If To has
- -- aspects, the aspects of From are added to the aspects of To. If From has
- -- no aspects, the routine has no effect. When From denotes a subprogram
- -- body stub that also acts as a spec, the only aspects relocated to node
- -- To are those from table Aspect_On_Body_Or_Stub_OK and preconditions.
+ -- aspects, the aspects of From are appended to the aspects of To. If From
+ -- has no aspects, the routine has no effect. Special behavior:
+ -- * When node From denotes a subprogram body stub without a previous
+ -- declaration, the only aspects relocated to node To are those found
+ -- in table Aspect_On_Body_Or_Stub_OK.
+ -- * When node From denotes a single synchronized type declaration, the
+ -- only aspects relocated to node To are those found in table
+ -- Aspect_On_Anonymous_Object_OK.
function Permits_Aspect_Specifications (N : Node_Id) return Boolean;
-- Returns True if the node N is a declaration node that permits aspect
end if;
end Elist26;
+ function Elist36 (N : Node_Id) return Elist_Id is
+ pragma Assert (Nkind (N) in N_Entity);
+ Value : constant Union_Id := Nodes.Table (N + 6).Field6;
+ begin
+ if Value = 0 then
+ return No_Elist;
+ else
+ return Elist_Id (Value);
+ end if;
+ end Elist36;
+
function Name1 (N : Node_Id) return Name_Id is
begin
pragma Assert (N <= Nodes.Last);
Nodes.Table (N + 4).Field8 := Union_Id (Val);
end Set_Elist26;
+ procedure Set_Elist36 (N : Node_Id; Val : Elist_Id) is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ Nodes.Table (N + 6).Field6 := Union_Id (Val);
+ end Set_Elist36;
+
procedure Set_Name1 (N : Node_Id; Val : Name_Id) is
begin
pragma Assert (N <= Nodes.Last);
function Elist26 (N : Node_Id) return Elist_Id;
pragma Inline (Elist26);
+ function Elist36 (N : Node_Id) return Elist_Id;
+ pragma Inline (Elist36);
+
function Name1 (N : Node_Id) return Name_Id;
pragma Inline (Name1);
procedure Set_Elist26 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist26);
+ procedure Set_Elist36 (N : Node_Id; Val : Elist_Id);
+ pragma Inline (Set_Elist36);
+
procedure Set_Name1 (N : Node_Id; Val : Name_Id);
pragma Inline (Set_Name1);
#define Elist24(N) Field24 (N)
#define Elist25(N) Field25 (N)
#define Elist26(N) Field26 (N)
+#define Elist36(N) Field36 (N)
#define Name1(N) Field1 (N)
#define Name2(N) Field2 (N)
raise Program_Error;
end if;
+ -- Protected units, the applicable pragmas are:
+ -- Part_Of
+
+ elsif Ekind (Id) = E_Protected_Type then
+ if Prag_Nam = Name_Part_Of then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
-- Subprogram bodies, the applicable pragmas are:
-- Postcondition
-- Precondition
-- Task units, the applicable pragmas are:
-- Depends
-- Global
+ -- Part_Of
elsif Ekind (Id) = E_Task_Type then
- if Nam_In (Prag_Nam, Name_Depends, Name_Global) then
+ if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then
Add_Classification;
-- The pragma is not a proper contract item
-- Async_Readers
-- Async_Writers
-- Constant_After_Elaboration
+ -- Depends
-- Effective_Reads
-- Effective_Writes
+ -- Global
-- Part_Of
elsif Ekind (Id) = E_Variable then
if Nam_In (Prag_Nam, Name_Async_Readers,
Name_Async_Writers,
Name_Constant_After_Elaboration,
+ Name_Depends,
Name_Effective_Reads,
Name_Effective_Writes,
+ Name_Global,
Name_Part_Of)
then
Add_Classification;
-----------------------------
procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
- Obj_Typ : constant Entity_Id := Etype (Obj_Id);
- AR_Val : Boolean := False;
- AW_Val : Boolean := False;
- ER_Val : Boolean := False;
- EW_Val : Boolean := False;
- Items : Node_Id;
- Prag : Node_Id;
- Seen : Boolean := False;
+ Obj_Typ : constant Entity_Id := Etype (Obj_Id);
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ Encap_Id : Entity_Id;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+ Items : Node_Id;
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Restore_Mode : Boolean := False;
+ Seen : Boolean := False;
begin
-- The loop parameter in an element iterator over a formal container
Error_Msg_N ("constant cannot be volatile", Obj_Id);
end if;
+ Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
+
+ -- Check whether the lack of indicator Part_Of agrees with the
+ -- placement of the constant with respect to the state space.
+
+ if No (Prag) then
+ Check_Missing_Part_Of (Obj_Id);
+ end if;
+
-- Variable-related checks
else pragma Assert (Ekind (Obj_Id) = E_Variable);
+ -- The anonymous object created for a single concurrent type inherits
+ -- the SPARK_Mode from the type. Due to the timing of contract
+ -- analysis, delayed pragmas may be subject to the wrong SPARK_Mode,
+ -- usually that of the enclosing context. To remedy this, restore the
+ -- original SPARK_Mode of the related variable.
+
+ if Is_Single_Concurrent_Object (Obj_Id)
+ and then Present (SPARK_Pragma (Obj_Id))
+ then
+ Restore_Mode := True;
+ Save_SPARK_Mode_And_Set (Obj_Id, Mode);
+ end if;
+
+ -- Analyze all external properties
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
+ Seen := True;
+ end if;
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
+ Seen := True;
+ end if;
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
+ Seen := True;
+ end if;
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
+ Seen := True;
+ end if;
+
+ -- Verify the mutual interaction of the various external properties
+
+ if Seen then
+ Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
+ end if;
+
+ -- The anonymous object created for a single concurrent type carries
+ -- pragmas Depends and Globat of the type.
+
+ if Is_Single_Concurrent_Object (Obj_Id) then
+
+ -- Analyze Global first, as Depends may mention items classified
+ -- in the global categorization.
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Global);
+
+ if Present (Prag) then
+ Analyze_Global_In_Decl_Part (Prag);
+ end if;
+
+ -- Depends must be analyzed after Global in order to see the modes
+ -- of all global items.
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Depends);
+
+ if Present (Prag) then
+ Analyze_Depends_In_Decl_Part (Prag);
+ end if;
+ end if;
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
+
+ -- Analyze indicator Part_Of
+
+ if Present (Prag) then
+ Analyze_Part_Of_In_Decl_Part (Prag);
+
+ -- Otherwise check whether the lack of indicator Part_Of agrees with
+ -- the placement of the variable with respect to the state space.
+
+ else
+ Check_Missing_Part_Of (Obj_Id);
+ end if;
+
-- The following checks are relevant only when SPARK_Mode is on, as
-- they are not standard Ada legality rules. Internally generated
-- temporaries are ignored.
Obj_Id);
end if;
end if;
+
+ -- A variable whose Part_Of pragma specifies a single concurrent
+ -- type as encapsulator must be (SPARK RM 9.4):
+ -- * Of a type that defines full default initialization, or
+ -- * Declared with a default value, or
+ -- * Imported
+
+ Encap_Id := Encapsulating_State (Obj_Id);
+
+ if Present (Encap_Id)
+ and then Is_Single_Concurrent_Object (Encap_Id)
+ and then not Has_Full_Default_Initialization (Etype (Obj_Id))
+ and then not Has_Initial_Value (Obj_Id)
+ and then not Is_Imported (Obj_Id)
+ then
+ Error_Msg_N ("& requires full default initialization", Obj_Id);
+
+ Error_Msg_Name_1 := Chars (Encap_Id);
+ Error_Msg_N
+ (Fix_Msg (Encap_Id, "\object acts as constituent of single "
+ & "protected type %"), Obj_Id);
+ end if;
end if;
if Is_Ghost_Entity (Obj_Id) then
end if;
end if;
- -- Analyze all external properties
-
- Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
- Seen := True;
+ if Restore_Mode then
+ Restore_SPARK_Mode (Mode);
end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
- Seen := True;
- end if;
-
- -- Verify the mutual interaction of the various external properties
-
- if Seen then
- Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
- end if;
- end if;
-
- -- Check whether the lack of indicator Part_Of agrees with the placement
- -- of the object with respect to the state space.
-
- Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
-
- if No (Prag) then
- Check_Missing_Part_Of (Obj_Id);
end if;
-- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
end if;
end Analyze_Package_Contract;
+ --------------------------------
+ -- Analyze_Protected_Contract --
+ --------------------------------
+
+ procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Prot_Id);
+ Mode : SPARK_Mode_Type;
+
+ begin
+ -- Do not analyze a contract multiple times
+
+ if Present (Items) then
+ if Analyzed (Items) then
+ return;
+ else
+ Set_Analyzed (Items);
+ end if;
+ end if;
+
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related protected unit.
+
+ Save_SPARK_Mode_And_Set (Prot_Id, Mode);
+
+ -- A protected type must define full default initialization
+ -- (SPARK RM 9.4). This check is relevant only when SPARK_Mode is on as
+ -- it is not a standard Ada legality rule.
+
+ if SPARK_Mode = On
+ and then not Has_Full_Default_Initialization (Prot_Id)
+ then
+ Error_Msg_N
+ ("protected type & must define full default initialization",
+ Prot_Id);
+ end if;
+
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
+ Restore_SPARK_Mode (Mode);
+ end Analyze_Protected_Contract;
+
-------------------------------------------
-- Analyze_Subprogram_Body_Stub_Contract --
-------------------------------------------
-- Due to the timing of contract analysis, delayed pragmas may be
-- subject to the wrong SPARK_Mode, usually that of the enclosing
-- context. To remedy this, restore the original SPARK_Mode of the
- -- related subprogram body.
+ -- related task unit.
Save_SPARK_Mode_And_Set (Task_Id, Mode);
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
-- Add pragma Prag to the contract of a constant, entry, entry family,
- -- [generic] package, package body, [generic] subprogram, subprogram body,
- -- variable or task unit denoted by Id. The following are valid pragmas:
+ -- [generic] package, package body, protected unit, [generic] subprogram,
+ -- subprogram body, variable or task unit denoted by Id. The following are
+ -- valid pragmas:
-- Abstract_State
-- Async_Readers
-- Async_Writers
-- considered are:
-- Async_Readers
-- Async_Writers
+ -- Depends (single concurrent object)
-- Effective_Reads
-- Effective_Writes
+ -- Global (single concurrent object)
-- Part_Of
procedure Analyze_Package_Body_Contract
-- Initializes
-- Part_Of
+ procedure Analyze_Protected_Contract (Prot_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of protected unit
+ -- Prot_Id if they appeared at the end of a declarative region. Currently
+ -- there are no such pragmas.
+
procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
- -- Analyze all delayed pragmas chained on the contract of a subprogram body
+ -- Analyze all delayed pragmas chained on the contract of subprogram body
-- stub Stub_Id as if they appeared at the end of a declarative region. The
-- pragmas in question are:
-- Contract_Cases
-- Test_Case
procedure Analyze_Task_Contract (Task_Id : Entity_Id);
- -- Analyze all delayed pragmas chained on the contract of a task unit
- -- Task_Id as if they appeared at the end of a declarative region. The
- -- pragmas in question are:
+ -- Analyze all delayed pragmas chained on the contract of task unit Task_Id
+ -- as if they appeared at the end of a declarative region. The pragmas in
+ -- question are:
-- Depends
-- Global
-- Class_Wide_Type Node9
-- Current_Value Node9
- -- Part_Of_Constituents Elist9
-- Renaming_Map Uint9
-- Direct_Primitive_Operations Elist10
-- Float_Rep Uint10 (but returns Float_Rep_Kind)
-- Handler_Records List10
-- Normalized_Position_Max Uint10
+ -- Part_Of_Constituents Elist10
-- Component_Bit_Offset Uint11
-- Full_View Node11
-- BIP_Initialization_Call Node29
-- Subprograms_For_Type Node29
+ -- Anonymous_Object Node30
-- Corresponding_Equality Node30
-- Last_Aggregate_Assignment Node30
-- Static_Initialization Node30
Opt := First (Expressions (Decl));
while Present (Opt) loop
-
- -- Currently the only simple option allowed is External
-
- if Nkind (Opt) = N_Identifier
- and then Chars (Opt) = Name_External
- and then Chars (Opt) = Option_Nam
- then
+ if Nkind (Opt) = N_Identifier and then Chars (Opt) = Option_Nam then
return True;
end if;
return Node36 (Id);
end Anonymous_Master;
+ function Anonymous_Object (Id : E) return E is
+ begin
+ pragma Assert (Ekind_In (Id, E_Protected_Type, E_Task_Type));
+ return Node30 (Id);
+ end Anonymous_Object;
+
function Associated_Entity (Id : E) return E is
begin
return Node37 (Id);
function Contract (Id : E) return N is
begin
pragma Assert
- (Ekind_In (Id, E_Constant, -- object variants
+ (Ekind_In (Id, E_Protected_Type, -- concurrent variants
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Constant, -- object variants
E_Variable)
or else
Ekind_In (Id, E_Entry, -- overloadable variants
E_Package,
E_Package_Body)
or else
- Ekind_In (Id, E_Task_Body, -- synchronized variants
- E_Task_Type,
- E_Void)); -- special purpose
+ Ekind (Id) = E_Void); -- special purpose
return Node34 (Id);
end Contract;
function Part_Of_Constituents (Id : E) return L is
begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- return Elist9 (Id);
+ pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
+ return Elist10 (Id);
end Part_Of_Constituents;
function Partial_View_Has_Unknown_Discr (Id : E) return B is
function SPARK_Aux_Pragma (Id : E) return N is
begin
pragma Assert
- (Ekind_In (Id, E_Generic_Package, -- package variants
- E_Package,
- E_Package_Body)
+ (Ekind_In (Id, E_Protected_Type, -- concurrent variants
+ E_Task_Type)
or else
- Ekind_In (Id, E_Protected_Type, -- synchronized variants
- E_Task_Type));
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
return Node41 (Id);
end SPARK_Aux_Pragma;
function SPARK_Aux_Pragma_Inherited (Id : E) return B is
begin
pragma Assert
- (Ekind_In (Id, E_Generic_Package, -- package variants
- E_Package,
- E_Package_Body)
+ (Ekind_In (Id, E_Protected_Type, -- concurrent variants
+ E_Task_Type)
or else
- Ekind_In (Id, E_Protected_Type, -- synchronized variants
- E_Task_Type));
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
return Flag266 (Id);
end SPARK_Aux_Pragma_Inherited;
function SPARK_Pragma (Id : E) return N is
begin
pragma Assert
- (Ekind_In (Id, E_Entry, -- overloadable variants
+ (Ekind_In (Id, E_Protected_Body, -- concurrent variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
E_Entry_Family,
E_Function,
E_Generic_Function,
E_Package,
E_Package_Body)
or else
- Ekind_In (Id, E_Protected_Body, -- synchronized variants
- E_Protected_Type,
- E_Task_Body,
- E_Task_Type));
+ Ekind (Id) = E_Variable); -- variable
return Node40 (Id);
end SPARK_Pragma;
function SPARK_Pragma_Inherited (Id : E) return B is
begin
pragma Assert
- (Ekind_In (Id, E_Entry, -- overloadable variants
+ (Ekind_In (Id, E_Protected_Body, -- concurrent variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
E_Entry_Family,
E_Function,
E_Generic_Function,
E_Package,
E_Package_Body)
or else
- Ekind_In (Id, E_Protected_Body, -- synchronized variants
- E_Protected_Type,
- E_Task_Body,
- E_Task_Type));
+ Ekind (Id) = E_Variable); -- variable
return Flag265 (Id);
end SPARK_Pragma_Inherited;
Set_Node36 (Id, V);
end Set_Anonymous_Master;
+ procedure Set_Anonymous_Object (Id : E; V : E) is
+ begin
+ pragma Assert (Ekind_In (Id, E_Protected_Type, E_Task_Type));
+ Set_Node30 (Id, V);
+ end Set_Anonymous_Object;
+
procedure Set_Associated_Entity (Id : E; V : E) is
begin
Set_Node37 (Id, V);
procedure Set_Contract (Id : E; V : N) is
begin
pragma Assert
- (Ekind_In (Id, E_Constant, -- object variants
+ (Ekind_In (Id, E_Protected_Type, -- concurrent variants
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Constant, -- object variants
E_Variable)
or else
Ekind_In (Id, E_Entry, -- overloadable variants
E_Package,
E_Package_Body)
or else
- Ekind_In (Id, E_Task_Body, -- synchronized variants
- E_Task_Type,
- E_Void)); -- special purpose
+ Ekind (Id) = E_Void); -- special purpose
Set_Node34 (Id, V);
end Set_Contract;
procedure Set_Part_Of_Constituents (Id : E; V : L) is
begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- Set_Elist9 (Id, V);
+ pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
+ Set_Elist10 (Id, V);
end Set_Part_Of_Constituents;
procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True) is
procedure Set_SPARK_Aux_Pragma (Id : E; V : N) is
begin
pragma Assert
- (Ekind_In (Id, E_Generic_Package, -- package variants
- E_Package,
- E_Package_Body)
+ (Ekind_In (Id, E_Protected_Type, -- concurrent variants
+ E_Task_Type)
or else
- Ekind_In (Id, E_Protected_Type, -- synchronized variants
- E_Task_Type));
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
Set_Node41 (Id, V);
end Set_SPARK_Aux_Pragma;
procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is
begin
pragma Assert
- (Ekind_In (Id, E_Generic_Package, -- package variants
- E_Package,
- E_Package_Body)
+ (Ekind_In (Id, E_Protected_Type, -- concurrent variants
+ E_Task_Type)
or else
- Ekind_In (Id, E_Protected_Type, -- synchronized variants
- E_Task_Type));
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
Set_Flag266 (Id, V);
end Set_SPARK_Aux_Pragma_Inherited;
procedure Set_SPARK_Pragma (Id : E; V : N) is
begin
pragma Assert
- (Ekind_In (Id, E_Entry, -- overloadable variants
+ (Ekind_In (Id, E_Protected_Body, -- concurrent variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
E_Entry_Family,
E_Function,
E_Generic_Function,
E_Package,
E_Package_Body)
or else
- Ekind_In (Id, E_Protected_Body, -- synchronized variants
- E_Protected_Type,
- E_Task_Body,
- E_Task_Type));
+ Ekind (Id) = E_Variable); -- variable
Set_Node40 (Id, V);
end Set_SPARK_Pragma;
procedure Set_SPARK_Pragma_Inherited (Id : E; V : B := True) is
begin
pragma Assert
- (Ekind_In (Id, E_Entry, -- overloadable variants
+ (Ekind_In (Id, E_Protected_Body, -- concurrent variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
E_Entry_Family,
E_Function,
E_Generic_Function,
E_Package,
E_Package_Body)
or else
- Ekind_In (Id, E_Protected_Body, -- synchronized variants
- E_Protected_Type,
- E_Task_Body,
- E_Task_Type));
+ Ekind (Id) = E_Variable); -- variable
Set_Flag265 (Id, V);
end Set_SPARK_Pragma_Inherited;
end if;
end Is_Synchronized_Interface;
+ ---------------------------
+ -- Is_Synchronized_State --
+ ---------------------------
+
+ function Is_Synchronized_State (Id : E) return B is
+ begin
+ return
+ Ekind (Id) = E_Abstract_State
+ and then Has_Option (Id, Name_Synchronous);
+ end Is_Synchronized_State;
+
-----------------------
-- Is_Task_Interface --
-----------------------
when Object_Kind =>
Write_Str ("Current_Value");
- when E_Abstract_State =>
- Write_Str ("Part_Of_Constituents");
-
when E_Function |
E_Generic_Function |
E_Generic_Package |
E_Discriminant =>
Write_Str ("Normalized_Position_Max");
+ when E_Abstract_State |
+ E_Variable =>
+ Write_Str ("Part_Of_Constituents");
+
when others =>
Write_Str ("Field10??");
end case;
procedure Write_Field30_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Protected_Type |
+ E_Task_Type =>
+ Write_Str ("Anonymous_Object");
+
when E_Function =>
Write_Str ("Corresponding_Equality");
E_Package |
E_Package_Body |
E_Procedure |
+ E_Protected_Type |
E_Subprogram_Body |
E_Task_Body |
E_Task_Type |
E_Protected_Type |
E_Subprogram_Body |
E_Task_Body |
- E_Task_Type =>
+ E_Task_Type |
+ E_Variable =>
Write_Str ("SPARK_Pragma");
when others =>
-- finalization master that services most anonymous access-to-controlled
-- allocations that occur within the unit.
+-- Anonymous_Object (Node30)
+-- Present in protected and task type entities. Contains the entity of
+-- the anonymous object created for a single protected or task type.
+
-- Associated_Entity (Node37)
-- Defined in all entities. This field is similar to Associated_Node, but
-- applied to entities. The attribute links an entity from the generic
-- Contract (Node34)
-- Defined in constant, entry, entry family, operator, [generic] package,
--- package body, [generic] subprogram, subprogram body, variable and task
--- type entities. Points to the contract of the entity, holding various
--- assertion items and data classifiers.
+-- package body, protected type, [generic] subprogram, subprogram body,
+-- variable and task type entities. Points to the contract of the entity,
+-- holding various assertion items and data classifiers.
-- Corresponding_Concurrent_Type (Node18)
-- Defined in record types that are constructed by the expander to
-- need to set the flag.
-- Encapsulating_State (Node32)
--- Defined in abstract states, constants and variables. Contains the
--- entity of an ancestor state whose refinement utilizes this item as
--- a constituent.
+-- Defined in abstract state, constant and variable entities. Contains
+-- the entity of an ancestor state or a single concurrent type whose
+-- refinement utilizes this item as a constituent.
-- Enclosing_Scope (Node18)
-- Defined in labels. Denotes the innermost enclosing construct that
-- synchronized, task, or protected, or is derived from a synchronized
-- interface.
+-- Is_Synchronized_State (synthesized)
+-- Applies to all entities, true for abstract states that are subject to
+-- option Synchronous.
+
-- Is_Tag (Flag78)
-- Defined in E_Component and E_Constant entities. For regular tagged
-- type this flag is set on the tag component (whose name is Name_uTag).
-- case it points to the subtype of the parent type. This is the type
-- that is used as the Etype of the _parent field.
--- Part_Of_Constituents (Elist9)
--- Present in abstract state entities. Contains all constituents that are
--- subject to indicator Part_Of (both aspect and option variants).
+-- Part_Of_Constituents (Elist10)
+-- Present in abstract state and variable entities. Contains all
+-- constituents that are subject to indicator Part_Of (both aspect and
+-- option variants).
-- Partial_View_Has_Unknown_Discr (Flag280)
-- Present in all types. Set to Indicate that the partial view of a type
-- as computed (as a power of two) by the compiler.
-- SPARK_Aux_Pragma (Node41)
--- Present in [generic] package specs, package bodies and synchronized
--- types. For package specs and synchronized types it refers to the SPARK
--- mode setting for the private part. This field points to the N_Pragma
--- node that either appears in the private part or is inherited from the
--- enclosing context. For package bodies, it refers to the SPARK mode of
--- the elaboration sequence after the BEGIN. The fields points to the
--- N_Pragma node that either appears in the statement sequence or is
+-- Present in concurrent type, [generic] package spec and package body
+-- entities. For concurrent types and package specs it refers to the
+-- SPARK mode setting for the private part. This field points to the
+-- N_Pragma node that either appears in the private part or is inherited
+-- from the enclosing context. For package bodies, it refers to the SPARK
+-- mode of the elaboration sequence after the BEGIN. The fields points to
+-- the N_Pragma node that either appears in the statement sequence or is
-- inherited from the enclosing context. In all cases, if the pragma is
-- inherited, then the SPARK_Aux_Pragma_Inherited flag is set.
-- SPARK_Aux_Pragma_Inherited (Flag266)
--- Present in [generic] package specs, package bodies and synchronized
--- types. Set if the SPARK_Aux_Pragma field points to a pragma that is
+-- Present in concurrent type, [generic] package spec and package body
+-- entities. Set if the SPARK_Aux_Pragma field points to a pragma that is
-- inherited, rather than a local one.
-- SPARK_Pragma (Node40)
--- Present in entries, operators, [generic] packages, package bodies,
--- [generic] subprograms, subprogram bodies and synchronized types.
--- Points to the N_Pragma node that applies to the spec or body. This
--- is either set by a local SPARK_Mode pragma or is inherited from the
--- context (from an outer scope for the spec case or from the spec for
--- the body case). In the case where it is inherited the flag
--- SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma is
--- applicable.
+-- Present in concurrent type, entry, operator, [generic] package,
+-- package body, [generic] subprogram, subprogram body and variable
+-- entities. Points to the N_Pragma node that applies to the initial
+-- declaration or body. This is either set by a local SPARK_Mode pragma
+-- or is inherited from the context (from an outer scope for the spec
+-- case or from the spec for the body case). In the case where it is
+-- inherited the flag SPARK_Pragma_Inherited is set. Empty if no
+-- SPARK_Mode pragma is applicable.
-- SPARK_Pragma_Inherited (Flag265)
--- Present in entries, operators, [generic] packages, package bodies,
--- [generic] subprograms, subprogram bodies and synchronized types. Set
--- if the SPARK_Pragma attribute points to a pragma that is inherited,
--- rather than a local one.
+-- Present in concurrent type, entry, operator, [generic] package,
+-- package body, [generic] subprogram, subprogram body and variable
+-- entities. Set if the SPARK_Pragma attribute points to a pragma that is
+-- inherited, rather than a local one.
-- Spec_Entity (Node19)
-- Defined in package body entities. Points to corresponding package
-- E_Abstract_State
-- Refinement_Constituents (Elist8)
- -- Part_Of_Constituents (Elist9)
+ -- Part_Of_Constituents (Elist10)
-- Body_References (Elist16)
-- Non_Limited_View (Node19)
-- Encapsulating_State (Node32)
-- Has_Null_Refinement (synth)
-- Is_External_State (synth)
-- Is_Null_State (synth)
+ -- Is_Synchronized_State (synth)
-- E_Access_Protected_Subprogram_Type
-- Equivalent_Type (Node18)
-- Discriminant_Constraint (Elist21)
-- Scope_Depth_Value (Uint22)
-- Stored_Constraint (Elist23)
+ -- Anonymous_Object (Node30)
+ -- Contract (Node34)
-- SPARK_Pragma (Node40)
-- SPARK_Aux_Pragma (Node41)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- Has_Interrupt_Handler (synth)
-- Number_Entries (synth)
-- Scope_Depth (synth)
+ -- (plus type attributes)
-- E_Record_Type
-- E_Record_Subtype
-- Last_Entity (Node20)
-- Discriminant_Constraint (Elist21)
-- Scope_Depth_Value (Uint22)
- -- Scope_Depth (synth)
-- Stored_Constraint (Elist23)
-- Task_Body_Procedure (Node25)
-- Storage_Size_Variable (Node26) (base type only)
-- Relative_Deadline_Variable (Node28) (base type only)
+ -- Anonymous_Object (Node30)
-- Contract (Node34)
-- SPARK_Pragma (Node40)
-- SPARK_Aux_Pragma (Node41)
-- First_Component_Or_Discriminant (synth)
-- Has_Entries (synth)
-- Number_Entries (synth)
+ -- Scope_Depth (synth)
-- (plus type attributes)
-- E_Variable
-- Hiding_Loop_Variable (Node8)
-- Current_Value (Node9)
+ -- Part_Of_Constituents (Elist10)
-- Esize (Uint12)
-- Extra_Accessibility (Node13)
-- Alignment (Uint14)
-- Encapsulating_State (Node32)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
+ -- SPARK_Pragma (Node40)
-- Has_Alignment_Clause (Flag46)
-- Has_Atomic_Components (Flag86)
-- Has_Biased_Representation (Flag139)
-- OK_To_Rename (Flag247)
-- Optimize_Alignment_Space (Flag241)
-- Optimize_Alignment_Time (Flag242)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Suppress_Initialization (Flag105)
-- Treat_As_Volatile (Flag41)
-- Address_Clause (synth)
function Alias (Id : E) return E;
function Alignment (Id : E) return U;
function Anonymous_Master (Id : E) return E;
+ function Anonymous_Object (Id : E) return E;
function Associated_Entity (Id : E) return E;
function Associated_Formal_Package (Id : E) return E;
function Associated_Node_For_Itype (Id : E) return N;
function Is_Standard_String_Type (Id : E) return B;
function Is_String_Type (Id : E) return B;
function Is_Synchronized_Interface (Id : E) return B;
+ function Is_Synchronized_State (Id : E) return B;
function Is_Task_Interface (Id : E) return B;
function Is_Task_Record_Type (Id : E) return B;
function Is_Wrapper_Package (Id : E) return B;
procedure Set_Alias (Id : E; V : E);
procedure Set_Alignment (Id : E; V : U);
procedure Set_Anonymous_Master (Id : E; V : E);
+ procedure Set_Anonymous_Object (Id : E; V : E);
procedure Set_Associated_Entity (Id : E; V : E);
procedure Set_Associated_Formal_Package (Id : E; V : E);
procedure Set_Associated_Node_For_Itype (Id : E; V : N);
pragma Inline (Alias);
pragma Inline (Alignment);
pragma Inline (Anonymous_Master);
+ pragma Inline (Anonymous_Object);
pragma Inline (Associated_Entity);
pragma Inline (Associated_Formal_Package);
pragma Inline (Associated_Node_For_Itype);
pragma Inline (Set_Alias);
pragma Inline (Set_Alignment);
pragma Inline (Set_Anonymous_Master);
+ pragma Inline (Set_Anonymous_Object);
pragma Inline (Set_Associated_Entity);
pragma Inline (Set_Associated_Formal_Package);
pragma Inline (Set_Associated_Node_For_Itype);
if Subp = Eq_Prim_Op then
- -- Mark the node as analyzed to avoid reanalizing this
+ -- Mark the node as analyzed to avoid reanalyzing this
-- dispatching call (which would cause a never-ending loop)
Prev_Call := Relocate_Node (Call_Node);
Prepend_To (Decls, Counter_Decl);
Prepend_To (Decls, Counter_Typ_Decl);
- -- The counter and its associated type must be manually analized
+ -- The counter and its associated type must be manually analyzed
-- since N has already been analyzed. Use the scope of the spec
-- when inserting in a package.
Next_Component (Comp);
end loop;
end if;
+
+ -- A type which does not yield a synchronized object cannot have
+ -- a component that yields a synchronized object (SPARK RM 9.5).
+
+ if not Yields_Synchronized_Object (Rec) then
+ Comp := First_Component (Rec);
+ while Present (Comp) loop
+ if Comes_From_Source (Comp)
+ and then Yields_Synchronized_Object (Etype (Comp))
+ then
+ Error_Msg_Name_1 := Chars (Rec);
+ Error_Msg_N
+ ("component & of non-synchronized type % cannot be "
+ & "synchronized", Comp);
+ end if;
+
+ Next_Component (Comp);
+ end loop;
+ end if;
end if;
-- Make sure that if we have an iterator aspect, then we have
Aux : Node_Id;
Decl : Node_Id;
Decls : List_Id;
+ Def : Node_Id;
begin
-- When the aspect appears on a package, protected unit, subprogram
-- pragma Prag;
elsif Nkind (N) = N_Protected_Type_Declaration then
- Decls := Visible_Declarations (Protected_Definition (N));
+ Def := Protected_Definition (N);
+
+ if No (Def) then
+ Def :=
+ Make_Protected_Definition (Sloc (N),
+ Visible_Declarations => New_List,
+ End_Label => Empty);
+
+ Set_Protected_Definition (N, Def);
+ end if;
+
+ Decls := Visible_Declarations (Def);
if No (Decls) then
Decls := New_List;
- Set_Visible_Declarations (Protected_Definition (N), Decls);
+ Set_Visible_Declarations (Def, Decls);
end if;
Prepend_To (Decls, Prag);
- -- When the aspect is associated with a task unit declaration with a
- -- definition, insert the generated pragma at the top of the visible
- -- declarations the emulate the behavior of a source pragma.
+ -- When the aspect is associated with a task unit declaration, insert
+ -- insert the generated pragma at the top of the visible declarations
+ -- the emulate the behavior of a source pragma.
-- task [type] Prot with Aspect is
-- task [type] Prot is
-- pragma Prag;
- elsif Nkind (N) = N_Task_Type_Declaration
- and then Present (Task_Definition (N))
- then
- Decls := Visible_Declarations (Task_Definition (N));
+ elsif Nkind (N) = N_Task_Type_Declaration then
+ Def := Task_Definition (N);
+
+ if No (Def) then
+ Def :=
+ Make_Task_Definition (Sloc (N),
+ Visible_Declarations => New_List,
+ End_Label => Empty);
+
+ Set_Task_Definition (N, Def);
+ end if;
+
+ Decls := Visible_Declarations (Def);
if No (Decls) then
Decls := New_List;
- Set_Visible_Declarations (Task_Definition (N), Decls);
+ Set_Visible_Declarations (Def, Decls);
end if;
Prepend_To (Decls, Prag);
when Aspect_Part_Of =>
if Nkind_In (N, N_Object_Declaration,
N_Package_Instantiation)
+ or else Is_Single_Concurrent_Type_Declaration (N)
then
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Part_Of);
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
else
Error_Msg_NE
- ("aspect & must apply to a variable or package "
- & "instantiation", Aspect, Id);
+ ("aspect & must apply to package instantiation, "
+ & "object, single protected type or single task type",
+ Aspect, Id);
end if;
-- SPARK_Mode
Analyze_Package_Body_Contract (Defining_Entity (Context));
end if;
- -- Analyze the contracts of all subprogram declarations, subprogram
- -- bodies and variables due to the delayed visibility needs of their
- -- aspects and pragmas.
+ -- Analyze the contracts of eligible constructs (see below) due to
+ -- the delayed visibility needs of their aspects and pragmas.
Decl := First (L);
while Present (Decl) loop
- if Nkind (Decl) = N_Object_Declaration then
- Analyze_Object_Contract (Defining_Entity (Decl));
- elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
- N_Entry_Declaration,
- N_Generic_Subprogram_Declaration,
- N_Subprogram_Declaration)
+ -- Entry or subprogram declarations
+
+ if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+ N_Entry_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
then
Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
+ -- Entry or subprogram bodies
+
elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity (Decl));
+ -- Objects
+
+ elsif Nkind (Decl) = N_Object_Declaration then
+ Analyze_Object_Contract (Defining_Entity (Decl));
+
+ -- Protected untis
+
+ elsif Nkind_In (Decl, N_Protected_Type_Declaration,
+ N_Single_Protected_Declaration)
+ then
+ Analyze_Protected_Contract (Defining_Entity (Decl));
+
+ -- Subprogram body stubs
+
elsif Nkind (Decl) = N_Subprogram_Body_Stub then
Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
+ -- Task units
+
elsif Nkind_In (Decl, N_Single_Task_Declaration,
N_Task_Type_Declaration)
then
with Sem_Ch8; use Sem_Ch8;
with Sem_Ch13; use Sem_Ch13;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
or else From_Aspect_Specification (Prio_Item)
then
Error_Msg_Name_1 := Chars (Identifier (Prio_Item));
- Error_Msg_NE ("aspect% for & has no effect when Lock_Free" &
- " given??", Prio_Item, Id);
+ Error_Msg_NE
+ ("aspect% for & has no effect when Lock_Free given??",
+ Prio_Item, Id);
-- Pragma case
else
Error_Msg_Name_1 := Pragma_Name (Prio_Item);
- Error_Msg_NE ("pragma% for & has no effect when Lock_Free" &
- " given??", Prio_Item, Id);
+ Error_Msg_NE
+ ("pragma% for & has no effect when Lock_Free given??",
+ Prio_Item, Id);
end if;
end if;
end;
- if not Allows_Lock_Free_Implementation (N, True) then
+ if not Allows_Lock_Free_Implementation (N, Lock_Free_Given => True)
+ then
return;
end if;
end if;
or else From_Aspect_Specification (Prio_Item))
and then Chars (Identifier (Prio_Item)) = Name_Priority
then
- Error_Msg_N ("aspect Interrupt_Priority is preferred "
- & "in presence of handlers??", Prio_Item);
+ Error_Msg_N
+ ("aspect Interrupt_Priority is preferred in presence of "
+ & "handlers??", Prio_Item);
-- Pragma case
elsif Nkind (Prio_Item) = N_Pragma
and then Pragma_Name (Prio_Item) = Name_Priority
then
- Error_Msg_N ("pragma Interrupt_Priority is preferred "
- & "in presence of handlers??", Prio_Item);
+ Error_Msg_N
+ ("pragma Interrupt_Priority is preferred in presence of "
+ & "handlers??", Prio_Item);
end if;
end if;
end;
------------------------------------------
procedure Analyze_Single_Protected_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Id : constant Node_Id := Defining_Identifier (N);
- T : Entity_Id;
- T_Decl : Node_Id;
- O_Decl : Node_Id;
- O_Name : constant Entity_Id := Id;
+ Loc : constant Source_Ptr := Sloc (N);
+ Obj_Id : constant Node_Id := Defining_Identifier (N);
+ Obj_Decl : Node_Id;
+ Typ : Entity_Id;
begin
- Generate_Definition (Id);
+ Generate_Definition (Obj_Id);
Tasking_Used := True;
- -- The node is rewritten as a protected type declaration, in exact
- -- analogy with what is done with single tasks.
+ -- A single protected declaration is transformed into a pair of an
+ -- anonymous protected type and an object of that type. Generate:
- T :=
- Make_Defining_Identifier (Sloc (Id),
- New_External_Name (Chars (Id), 'T'));
+ -- protected type Typ is ...;
- T_Decl :=
+ Typ :=
+ Make_Defining_Identifier (Sloc (Obj_Id),
+ Chars => New_External_Name (Chars (Obj_Id), 'T'));
+
+ Rewrite (N,
Make_Protected_Type_Declaration (Loc,
- Defining_Identifier => T,
+ Defining_Identifier => Typ,
Protected_Definition => Relocate_Node (Protected_Definition (N)),
- Interface_List => Interface_List (N));
+ Interface_List => Interface_List (N)));
+
+ -- Use the original defining identifier of the single protected
+ -- declaration in the generated object declaration to allow for debug
+ -- information to be attached to it when compiling with -gnatD. The
+ -- parent of the entity is the new object declaration. The single
+ -- protected declaration is not used in semantics or code generation,
+ -- but is scanned when generating debug information, and therefore needs
+ -- the updated Sloc information from the entity (see Sprint). Generate:
- O_Decl :=
+ -- Obj : Typ;
+
+ Obj_Decl :=
Make_Object_Declaration (Loc,
- Defining_Identifier => O_Name,
- Object_Definition => Make_Identifier (Loc, Chars (T)));
+ Defining_Identifier => Obj_Id,
+ Object_Definition => New_Occurrence_Of (Typ, Loc));
+
+ -- Relocate the aspects that appear on the original single protected
+ -- declaration to the object as the object is the visible name.
+
+ Set_Comes_From_Source (Obj_Decl, True);
+
+ Insert_After (N, Obj_Decl);
+ Mark_Rewrite_Insertion (Obj_Decl);
+
+ -- Relocate aspect Part_Of from the the original single protected
+ -- declaration to the anonymous object declaration. This emulates the
+ -- placement of an equivalent source pragma.
- Rewrite (N, T_Decl);
- Insert_After (N, O_Decl);
- Mark_Rewrite_Insertion (O_Decl);
+ Move_Or_Merge_Aspects (N, To => Obj_Decl);
- -- Enter names of type and object before analysis, because the name of
- -- the object may be used in its own body.
+ -- Relocate pragma Part_Of from the visible declarations of the original
+ -- single protected declaration to the anonymous object declaration. The
+ -- new placement better reflects the role of the pragma.
- Enter_Name (T);
- Set_Ekind (T, E_Protected_Type);
- Set_Etype (T, T);
+ Relocate_Pragmas_To_Anonymous_Object (N, Obj_Decl);
- Enter_Name (O_Name);
- Set_Ekind (O_Name, E_Variable);
- Set_Etype (O_Name, T);
+ -- Enter the names of the anonymous protected type and the object before
+ -- analysis takes places, because the name of the object may be used in
+ -- its own body.
+
+ Enter_Name (Typ);
+ Set_Ekind (Typ, E_Protected_Type);
+ Set_Etype (Typ, Typ);
+ Set_Anonymous_Object (Typ, Obj_Id);
+
+ Enter_Name (Obj_Id);
+ Set_Ekind (Obj_Id, E_Variable);
+ Set_Etype (Obj_Id, Typ);
+ Set_Part_Of_Constituents (Obj_Id, New_Elmt_List);
+ Set_SPARK_Pragma (Obj_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Obj_Id);
-- Instead of calling Analyze on the new node, call the proper analysis
-- procedure directly. Otherwise the node would be expanded twice, with
Analyze_Protected_Type_Declaration (N);
if Has_Aspects (N) then
- Analyze_Aspect_Specifications (N, Id);
+ Analyze_Aspect_Specifications (N, Obj_Id);
end if;
end Analyze_Single_Protected_Declaration;
-------------------------------------
procedure Analyze_Single_Task_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Id : constant Node_Id := Defining_Identifier (N);
- T : Entity_Id;
- T_Decl : Node_Id;
- O_Decl : Node_Id;
- O_Name : constant Entity_Id := Id;
+ Loc : constant Source_Ptr := Sloc (N);
+ Obj_Id : constant Node_Id := Defining_Identifier (N);
+ Obj_Decl : Node_Id;
+ Typ : Entity_Id;
begin
- Generate_Definition (Id);
+ Generate_Definition (Obj_Id);
Tasking_Used := True;
- -- The node is rewritten as a task type declaration, followed by an
- -- object declaration of that anonymous task type.
+ -- A single task declaration is transformed into a pait of an anonymous
+ -- task type and an object of that type. Generate:
+
+ -- task type Typ is ...;
- T :=
- Make_Defining_Identifier (Sloc (Id),
- New_External_Name (Chars (Id), Suffix => "TK"));
+ Typ :=
+ Make_Defining_Identifier (Sloc (Obj_Id),
+ Chars => New_External_Name (Chars (Obj_Id), Suffix => "TK"));
- T_Decl :=
+ Rewrite (N,
Make_Task_Type_Declaration (Loc,
- Defining_Identifier => T,
+ Defining_Identifier => Typ,
Task_Definition => Relocate_Node (Task_Definition (N)),
- Interface_List => Interface_List (N));
-
- -- We use the original defining identifier of the single task in the
- -- generated object declaration, so that debugging information can
- -- be attached to it when compiling with -gnatD. The parent of the
- -- entity is the new object declaration. The single_task_declaration
- -- is not used further in semantics or code generation, but is scanned
- -- when generating debug information, and therefore needs the updated
- -- Sloc information for the entity (see Sprint). Aspect specifications
- -- are moved from the single task node to the object declaration node.
-
- O_Decl :=
+ Interface_List => Interface_List (N)));
+
+ -- Use the original defining identifier of the single task declaration
+ -- in the generated object declaration to allow for debug information
+ -- to be attached to it when compiling with -gnatD. The parent of the
+ -- entity is the new object declaration. The single task declaration
+ -- is not used in semantics or code generation, but is scanned when
+ -- generating debug information, and therefore needs the updated Sloc
+ -- information from the entity (see Sprint). Generate:
+
+ -- Obj : Typ;
+
+ Obj_Decl :=
Make_Object_Declaration (Loc,
- Defining_Identifier => O_Name,
- Object_Definition => Make_Identifier (Loc, Chars (T)));
+ Defining_Identifier => Obj_Id,
+ Object_Definition => New_Occurrence_Of (Typ, Loc));
- Rewrite (N, T_Decl);
- Insert_After (N, O_Decl);
- Mark_Rewrite_Insertion (O_Decl);
+ -- Relocate the aspects that appear on the original single protected
+ -- declaration to the object as the object is the visible name.
- -- Enter names of type and object before analysis, because the name of
- -- the object may be used in its own body.
+ Set_Comes_From_Source (Obj_Decl, True);
- Enter_Name (T);
- Set_Ekind (T, E_Task_Type);
- Set_Etype (T, T);
+ Insert_After (N, Obj_Decl);
+ Mark_Rewrite_Insertion (Obj_Decl);
- Enter_Name (O_Name);
- Set_Ekind (O_Name, E_Variable);
- Set_Etype (O_Name, T);
+ -- Relocate aspects Depends, Global and Part_Of from the original single
+ -- task declaration to the anonymous object declaration. This emulates
+ -- the placement of an equivalent source pragma.
+
+ Move_Or_Merge_Aspects (N, To => Obj_Decl);
+
+ -- Relocate pragmas Depends, Global and Part_Of from the visible
+ -- declarations of the original single protected declaration to the
+ -- anonymous object declaration. The new placement better reflects the
+ -- role of the pragmas.
+
+ Relocate_Pragmas_To_Anonymous_Object (N, Obj_Decl);
+
+ -- Enter the names of the anonymous task type and the object before
+ -- analysis takes places, because the name of the object may be used
+ -- in its own body.
+
+ Enter_Name (Typ);
+ Set_Ekind (Typ, E_Task_Type);
+ Set_Etype (Typ, Typ);
+ Set_Anonymous_Object (Typ, Obj_Id);
+
+ Enter_Name (Obj_Id);
+ Set_Ekind (Obj_Id, E_Variable);
+ Set_Etype (Obj_Id, Typ);
+ Set_Part_Of_Constituents (Obj_Id, New_Elmt_List);
+ Set_SPARK_Pragma (Obj_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Obj_Id);
-- Instead of calling Analyze on the new node, call the proper analysis
-- procedure directly. Otherwise the node would be expanded twice, with
Analyze_Task_Type_Declaration (N);
if Has_Aspects (N) then
- Analyze_Aspect_Specifications (N, Id);
+ Analyze_Aspect_Specifications (N, Obj_Id);
end if;
end Analyze_Single_Task_Declaration;
Next_Entity (E);
end loop;
end Install_Declarations;
+
end Sem_Ch9;
-- Local variables
- Loc : constant Source_Ptr := Sloc (N);
- Ent : Entity_Id;
- Decl : Node_Id;
+ Loc : constant Source_Ptr := Sloc (N);
+
+ Inst_Case : constant Boolean := Nkind (N) in N_Generic_Instantiation;
+ -- Indicates if we have instantiation case
+
+ Ent : Entity_Id;
+ Callee_Unit_Internal : Boolean;
+ Caller_Unit_Internal : Boolean;
+ Decl : Node_Id;
+ Inst_Callee : Source_Ptr;
+ Inst_Caller : Source_Ptr;
+ Unit_Callee : Unit_Number_Type;
+ Unit_Caller : Unit_Number_Type;
+
+ Body_Acts_As_Spec : Boolean;
+ -- Set to true if call is to body acting as spec (no separate spec)
+
+ Cunit_SC : Boolean := False;
+ -- Set to suppress dynamic elaboration checks where one of the
+ -- enclosing scopes has Elaboration_Checks_Suppressed set, or else
+ -- if a pragma Elaborate[_All] applies to that scope, in which case
+ -- warnings on the scope are also suppressed. For the internal case,
+ -- we ignore this flag.
E_Scope : Entity_Id;
-- Top level scope of entity for called subprogram. This value includes
-- non-visible unit. This is the scope that is to be investigated to
-- see whether an elaboration check is required.
+ Issue_In_SPARK : Boolean;
+ -- Flag set when a source entity is called during elaboration in SPARK
+
W_Scope : Entity_Id;
-- Top level scope of directly called entity for subprogram. This
-- differs from E_Scope in the case where renamings or derivations
-- on this intermediate package. These special cases are handled in
-- Set_Elaboration_Constraint.
- Body_Acts_As_Spec : Boolean;
- -- Set to true if call is to body acting as spec (no separate spec)
-
- Inst_Case : constant Boolean := Nkind (N) in N_Generic_Instantiation;
- -- Indicates if we have instantiation case
-
- Caller_Unit_Internal : Boolean;
- Callee_Unit_Internal : Boolean;
-
- Inst_Caller : Source_Ptr;
- Inst_Callee : Source_Ptr;
-
- Unit_Caller : Unit_Number_Type;
- Unit_Callee : Unit_Number_Type;
-
- Cunit_SC : Boolean := False;
- -- Set to suppress dynamic elaboration checks where one of the
- -- enclosing scopes has Elaboration_Checks_Suppressed set, or else
- -- if a pragma Elaborate[_All] applies to that scope, in which case
- -- warnings on the scope are also suppressed. For the internal case,
- -- we ignore this flag.
-
-- Start of processing for Check_A_Call
begin
declare
Ent : constant Entity_Id := Get_Referenced_Ent (N);
begin
- if Is_Init_Proc (Ent)
- and then not In_Same_Extended_Unit (N, Ent)
- then
+ if Is_Init_Proc (Ent) and then not In_Same_Extended_Unit (N, Ent) then
W_Scope := Scope (Ent);
else
W_Scope := E;
return;
end if;
+ Issue_In_SPARK := SPARK_Mode = On and Comes_From_Source (Ent);
+
-- Now check if an Elaborate_All (or dynamic check) is needed
if not Suppress_Elaboration_Warnings (Ent)
-- Instantiation case
if Inst_Case then
- if SPARK_Mode = On then
+ if Issue_In_SPARK then
Error_Msg_NE
("instantiation of & during elaboration in SPARK", N, Ent);
-
else
Elab_Warning
("instantiation of & may raise Program_Error?l?",
-- Variable reference in SPARK mode
- elsif Variable_Case then
+ elsif Variable_Case and Issue_In_SPARK then
Error_Msg_NE
("reference to & during elaboration in SPARK", N, Ent);
"info: implicit call to & during elaboration?$?",
Ent);
- elsif SPARK_Mode = On then
+ elsif Issue_In_SPARK then
Error_Msg_NE ("call to & during elaboration in SPARK", N, Ent);
else
-- Case of Elaborate_All not present and required, for SPARK this
-- is an error, so give an error message.
- if SPARK_Mode = On then
+ if Issue_In_SPARK then
Error_Msg_NE ("\Elaborate_All pragma required for&", N, W_Scope);
-- Otherwise we generate an implicit pragma. For a subprogram
-- to Uppercase or Lowercase, then a new string literal with appropriate
-- casing is constructed.
+ procedure Analyze_Part_Of
+ (Indic : Node_Id;
+ Item_Id : Entity_Id;
+ Encap : Node_Id;
+ Encap_Id : out Entity_Id;
+ Legal : out Boolean);
+ -- Subsidiary to Analyze_Part_Of_In_Decl_Part, Analyze_Part_Of_Option and
+ -- Analyze_Pragma. Perform full analysis of indicator Part_Of. Indic is the
+ -- Part_Of indicator. Item_Id is the entity of an abstract state, object or
+ -- package instantiation. Encap denotes the encapsulating state or single
+ -- concurrent type. Encap_Id is the entity of Encap. Flag Legal is set when
+ -- the indicator is legal.
+
function Appears_In (List : Elist_Id; Item_Id : Entity_Id) return Boolean;
-- Subsidiary to analysis of pragmas Depends, Global and Refined_Depends.
-- Query whether a particular item appears in a mixed list of nodes and
-- Do_Checks is set, the routine reports duplicate pragmas. The routine
-- returns Empty when reaching the start of the node chain.
- function Fix_Msg (Id : Entity_Id; Msg : String) return String;
- -- Replace all occurrences of "subprogram" in string Msg with a specific
- -- word depending on the Ekind of Id as follows:
- -- * When Id is an entry [family], replace with "entry"
- -- * When Id is a task type, replace with "task unit"
-
function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
-- If Def_Id refers to a renamed subprogram, then the base subprogram (the
-- original one, following the renaming chain) is returned. Otherwise the
Subp_Outputs => Subp_Outputs,
Global_Seen => Global_Seen);
+ -- When pragma [Refined_]Depends appears on a single concurrent
+ -- type, it is relocated to the anonymous object.
+
+ if Is_Single_Concurrent_Object (Spec_Id) then
+ null;
+
-- Ensure that the formal parameters are visible when analyzing
-- all clauses. This falls out of the general rule of aspects
-- pertaining to subprogram declarations.
- if not In_Open_Scopes (Spec_Id) then
+ elsif not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
Push_Scope (Spec_Id);
-- messages.
else
+ -- When pragma [Refined_]Global appears on a single concurrent type,
+ -- it is relocated to the anonymous object.
+
+ if Is_Single_Concurrent_Object (Spec_Id) then
+ null;
+
-- Ensure that the formal parameters are visible when processing an
-- item. This falls out of the general rule of aspects pertaining to
-- subprogram declarations.
- if not In_Open_Scopes (Spec_Id) then
+ elsif not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
Push_Scope (Spec_Id);
Set_Is_Analyzed_Pragma (N);
end Analyze_Initializes_In_Decl_Part;
+ ---------------------
+ -- Analyze_Part_Of --
+ ---------------------
+
+ procedure Analyze_Part_Of
+ (Indic : Node_Id;
+ Item_Id : Entity_Id;
+ Encap : Node_Id;
+ Encap_Id : out Entity_Id;
+ Legal : out Boolean)
+ is
+ Encap_Typ : Entity_Id;
+ Item_Decl : Node_Id;
+ Pack_Id : Entity_Id;
+ Placement : State_Space_Kind;
+ Parent_Unit : Entity_Id;
+
+ begin
+ -- Assume that the indicator is illegal
+
+ Encap_Id := Empty;
+ Legal := False;
+
+ if Nkind_In (Encap, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
+ then
+ Analyze (Encap);
+ Resolve_State (Encap);
+
+ Encap_Id := Entity (Encap);
+
+ -- The encapsulator is an abstract state
+
+ if Ekind (Encap_Id) = E_Abstract_State then
+ null;
+
+ -- The encapsulator is a single concurrent type (SPARK RM 9.3)
+
+ elsif Is_Single_Concurrent_Object (Encap_Id) then
+ null;
+
+ -- Otherwise the encapsulator is not a legal choice
+
+ else
+ SPARK_Msg_N
+ ("indicator Part_Of must denote abstract state, single "
+ & "protected type or single task type", Encap);
+ return;
+ end if;
+
+ -- This is a syntax error, always report
+
+ else
+ Error_Msg_N
+ ("indicator Part_Of must denote abstract state, single protected "
+ & "type or single task type", Encap);
+ return;
+ end if;
+
+ -- Catch a case where indicator Part_Of denotes the abstract view of a
+ -- variable which appears as an abstract state (SPARK RM 10.1.2 2).
+
+ if From_Limited_With (Encap_Id)
+ and then Present (Non_Limited_View (Encap_Id))
+ and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable
+ then
+ SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap);
+ SPARK_Msg_N ("\& denotes abstract view of object", Encap);
+ return;
+ end if;
+
+ -- The encapsulator is an abstract state
+
+ if Ekind (Encap_Id) = E_Abstract_State then
+
+ -- Determine where the object, package instantiation or state lives
+ -- with respect to the enclosing packages or package bodies.
+
+ Find_Placement_In_State_Space
+ (Item_Id => Item_Id,
+ Placement => Placement,
+ Pack_Id => Pack_Id);
+
+ -- The item appears in a non-package construct with a declarative
+ -- part (subprogram, block, etc). As such, the item is not allowed
+ -- to be a part of an encapsulating state because the item is not
+ -- visible.
+
+ if Placement = Not_In_Package then
+ SPARK_Msg_N
+ ("indicator Part_Of cannot appear in this context "
+ & "(SPARK RM 7.2.6(5))", Indic);
+ Error_Msg_Name_1 := Chars (Scope (Encap_Id));
+ SPARK_Msg_NE
+ ("\& is not part of the hidden state of package %",
+ Indic, Item_Id);
+
+ -- The item appears in the visible state space of some package. In
+ -- general this scenario does not warrant Part_Of except when the
+ -- package is a private child unit and the encapsulating state is
+ -- declared in a parent unit or a public descendant of that parent
+ -- unit.
+
+ elsif Placement = Visible_State_Space then
+ if Is_Child_Unit (Pack_Id)
+ and then Is_Private_Descendant (Pack_Id)
+ then
+ -- A variable or state abstraction which is part of the visible
+ -- state of a private child unit (or one of its public
+ -- descendants) must have its Part_Of indicator specified. The
+ -- Part_Of indicator must denote a state abstraction declared
+ -- by either the parent unit of the private unit or by a public
+ -- descendant of that parent unit.
+
+ -- Find nearest private ancestor (which can be the current unit
+ -- itself).
+
+ Parent_Unit := Pack_Id;
+ while Present (Parent_Unit) loop
+ exit when
+ Private_Present
+ (Parent (Unit_Declaration_Node (Parent_Unit)));
+ Parent_Unit := Scope (Parent_Unit);
+ end loop;
+
+ Parent_Unit := Scope (Parent_Unit);
+
+ if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then
+ SPARK_Msg_NE
+ ("indicator Part_Of must denote abstract state or public "
+ & "descendant of & (SPARK RM 7.2.6(3))",
+ Indic, Parent_Unit);
+
+ elsif Scope (Encap_Id) = Parent_Unit
+ or else
+ (Is_Ancestor_Package (Parent_Unit, Scope (Encap_Id))
+ and then not Is_Private_Descendant (Scope (Encap_Id)))
+ then
+ null;
+
+ else
+ SPARK_Msg_NE
+ ("indicator Part_Of must denote abstract state or public "
+ & "descendant of & (SPARK RM 7.2.6(3))",
+ Indic, Parent_Unit);
+ end if;
+
+ -- Indicator Part_Of is not needed when the related package is not
+ -- a private child unit or a public descendant thereof.
+
+ else
+ SPARK_Msg_N
+ ("indicator Part_Of cannot appear in this context "
+ & "(SPARK RM 7.2.6(5))", Indic);
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ SPARK_Msg_NE
+ ("\& is declared in the visible part of package %",
+ Indic, Item_Id);
+ end if;
+
+ -- When the item appears in the private state space of a package, the
+ -- encapsulating state must be declared in the same package.
+
+ elsif Placement = Private_State_Space then
+ if Scope (Encap_Id) /= Pack_Id then
+ SPARK_Msg_NE
+ ("indicator Part_Of must designate an abstract state of "
+ & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ SPARK_Msg_NE
+ ("\& is declared in the private part of package %",
+ Indic, Item_Id);
+ end if;
+
+ -- Items declared in the body state space of a package do not need
+ -- Part_Of indicators as the refinement has already been seen.
+
+ else
+ SPARK_Msg_N
+ ("indicator Part_Of cannot appear in this context "
+ & "(SPARK RM 7.2.6(5))", Indic);
+
+ if Scope (Encap_Id) = Pack_Id then
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ SPARK_Msg_NE
+ ("\& is declared in the body of package %", Indic, Item_Id);
+ end if;
+ end if;
+
+ -- The encapsulator is a single concurrent type
+
+ else
+ Encap_Typ := Etype (Encap_Id);
+
+ -- Only abstract states and variables can act as constituents of an
+ -- encapsulating single concurrent type.
+
+ if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+ null;
+
+ -- The constituent is a constant
+
+ elsif Ekind (Item_Id) = E_Constant then
+ Error_Msg_Name_1 := Chars (Encap_Id);
+ SPARK_Msg_NE
+ (Fix_Msg (Encap_Typ, "consant & cannot act as constituent of "
+ & "single protected type %"), Indic, Item_Id);
+
+ -- The constituent is a package instantiation
+
+ else
+ Error_Msg_Name_1 := Chars (Encap_Id);
+ SPARK_Msg_NE
+ (Fix_Msg (Encap_Typ, "package instantiation & cannot act as "
+ & "constituent of single protected type %"), Indic, Item_Id);
+ end if;
+
+ -- When the item denotes an abstract state of a nested package, use
+ -- the declaration of the package to detect proper placement.
+
+ -- package Pack is
+ -- task T;
+ -- package Nested
+ -- with Abstract_State => (State with Part_Of => T)
+
+ if Ekind (Item_Id) = E_Abstract_State then
+ Item_Decl := Unit_Declaration_Node (Scope (Item_Id));
+ else
+ Item_Decl := Declaration_Node (Item_Id);
+ end if;
+
+ -- Both the item and its encapsulating single concurrent type must
+ -- appear in the same declarative region (SPARK RM 9.3). Note that
+ -- privacy is ignored.
+
+ if Parent (Item_Decl) /= Parent (Declaration_Node (Encap_Id)) then
+ Error_Msg_Name_1 := Chars (Encap_Id);
+ SPARK_Msg_NE
+ (Fix_Msg (Encap_Typ, "constituent & must be declared "
+ & "immediately within the same region as single protected "
+ & "type %"), Indic, Item_Id);
+ end if;
+ end if;
+
+ Legal := True;
+ end Analyze_Part_Of;
+
+ ----------------------------------
+ -- Analyze_Part_Of_In_Decl_Part --
+ ----------------------------------
+
+ procedure Analyze_Part_Of_In_Decl_Part (N : Node_Id) is
+ Var_Decl : constant Node_Id := Find_Related_Context (N);
+ Var_Id : constant Entity_Id := Defining_Entity (Var_Decl);
+ Encap_Id : Entity_Id;
+ Legal : Boolean;
+
+ begin
+ -- Detect any discrepancies between the placement of the variable with
+ -- respect to general state space and the encapsulating state or single
+ -- concurrent type.
+
+ Analyze_Part_Of
+ (Indic => N,
+ Item_Id => Var_Id,
+ Encap => Get_Pragma_Arg (First (Pragma_Argument_Associations (N))),
+ Encap_Id => Encap_Id,
+ Legal => Legal);
+
+ -- The Part_Of indicator turns the variable into a constituent of the
+ -- encapsulating state or single concurrent type.
+
+ if Legal then
+ pragma Assert (Present (Encap_Id));
+
+ Append_Elmt (Var_Id, Part_Of_Constituents (Encap_Id));
+ Set_Encapsulating_State (Var_Id, Encap_Id);
+ end if;
+ end Analyze_Part_Of_In_Decl_Part;
+
--------------------
-- Analyze_Pragma --
--------------------
-- Inspect the remainder of the list containing pragma N and look for
-- a pragma that matches Id. If found, analyze the pragma.
- procedure Analyze_Part_Of
- (Item_Id : Entity_Id;
- State : Node_Id;
- Indic : Node_Id;
- Legal : out Boolean);
- -- Subsidiary to the analysis of pragmas Abstract_State and Part_Of.
- -- Perform full analysis of indicator Part_Of. Item_Id is the entity of
- -- an abstract state, object, or package instantiation. State is the
- -- encapsulating state. Indic is the Part_Of indicator. Flag Legal is
- -- set when the indicator is legal.
-
procedure Analyze_Pre_Post_Condition;
-- Subsidiary to the analysis of pragmas Precondition and Postcondition
elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
null;
+ -- Object declaration of a single concurrent type
+
+ elsif Nkind (Subp_Decl) = N_Object_Declaration then
+ null;
+
+ -- Single task type
+
+ elsif Nkind (Subp_Decl) = N_Single_Task_Declaration then
+ null;
+
-- Subprogram body acts as spec
elsif Nkind (Subp_Decl) = N_Subprogram_Body
elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
null;
- -- Task unit
+ -- Task type
elsif Nkind (Subp_Decl) = N_Task_Type_Declaration then
null;
Legal := True;
Spec_Id := Unique_Defining_Entity (Subp_Decl);
- -- When the related context is an entry, it must be a protected entry
- -- (SPARK RM 6.1.4(6)).
+ -- When the related context is an entry, the entry must belong to a
+ -- protected unit (SPARK RM 6.1.4(6)).
if Is_Entry_Declaration (Spec_Id)
and then Ekind (Scope (Spec_Id)) /= E_Protected_Type
then
Pragma_Misplaced;
return;
+
+ -- When the related context is an anonymous object created for a
+ -- simple concurrent type, the type must be a task
+ -- (SPARK RM 6.1.4(6)).
+
+ elsif Is_Single_Concurrent_Object (Spec_Id)
+ and then Ekind (Etype (Spec_Id)) /= E_Task_Type
+ then
+ Pragma_Misplaced;
+ return;
end if;
-- A pragma that applies to a Ghost entity becomes Ghost for the
end loop;
end Analyze_If_Present;
- ---------------------
- -- Analyze_Part_Of --
- ---------------------
-
- procedure Analyze_Part_Of
- (Item_Id : Entity_Id;
- State : Node_Id;
- Indic : Node_Id;
- Legal : out Boolean)
- is
- Pack_Id : Entity_Id;
- Placement : State_Space_Kind;
- Parent_Unit : Entity_Id;
- State_Id : Entity_Id;
-
- begin
- -- Assume that the pragma/option is illegal
-
- Legal := False;
-
- if Nkind_In (State, N_Expanded_Name,
- N_Identifier,
- N_Selected_Component)
- then
- Analyze (State);
- Resolve_State (State);
-
- if Is_Entity_Name (State)
- and then Ekind (Entity (State)) = E_Abstract_State
- then
- State_Id := Entity (State);
-
- else
- SPARK_Msg_N
- ("indicator Part_Of must denote an abstract state", State);
- return;
- end if;
-
- -- This is a syntax error, always report
-
- else
- Error_Msg_N
- ("indicator Part_Of must denote an abstract state", State);
- return;
- end if;
-
- -- Catch a case where indicator Part_Of denotes the abstract view of
- -- a variable which appears as an abstract state (SPARK RM 10.1.2 2).
-
- if From_Limited_With (State_Id)
- and then Present (Non_Limited_View (State_Id))
- and then Ekind (Non_Limited_View (State_Id)) = E_Variable
- then
- SPARK_Msg_N
- ("indicator Part_Of must denote an abstract state", State);
- SPARK_Msg_N ("\& denotes abstract view of object", State);
- return;
- end if;
-
- -- 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.
-
- Find_Placement_In_State_Space
- (Item_Id => Item_Id,
- Placement => Placement,
- Pack_Id => Pack_Id);
-
- -- The item appears in a non-package construct with a declarative
- -- part (subprogram, block, etc). As such, the item is not allowed
- -- to be a part of an encapsulating state because the item is not
- -- visible.
-
- if Placement = Not_In_Package then
- SPARK_Msg_N
- ("indicator Part_Of cannot appear in this context "
- & "(SPARK RM 7.2.6(5))", Indic);
- Error_Msg_Name_1 := Chars (Scope (State_Id));
- SPARK_Msg_NE
- ("\& is not part of the hidden state of package %",
- Indic, Item_Id);
-
- -- The item appears in the visible state space of some package. In
- -- general this scenario does not warrant Part_Of except when the
- -- package is a private child unit and the encapsulating state is
- -- declared in a parent unit or a public descendant of that parent
- -- unit.
-
- elsif Placement = Visible_State_Space then
- if Is_Child_Unit (Pack_Id)
- and then Is_Private_Descendant (Pack_Id)
- then
- -- A variable or state abstraction which is part of the
- -- visible state of a private child unit (or one of its public
- -- descendants) must have its Part_Of indicator specified. The
- -- Part_Of indicator must denote a state abstraction declared
- -- by either the parent unit of the private unit or by a public
- -- descendant of that parent unit.
-
- -- Find nearest private ancestor (which can be the current unit
- -- itself).
-
- Parent_Unit := Pack_Id;
- while Present (Parent_Unit) loop
- exit when Private_Present
- (Parent (Unit_Declaration_Node (Parent_Unit)));
- Parent_Unit := Scope (Parent_Unit);
- end loop;
-
- Parent_Unit := Scope (Parent_Unit);
-
- if not Is_Child_Or_Sibling (Pack_Id, Scope (State_Id)) then
- SPARK_Msg_NE
- ("indicator Part_Of must denote an abstract state or "
- & "public descendant of & (SPARK RM 7.2.6(3))",
- Indic, Parent_Unit);
-
- elsif Scope (State_Id) = Parent_Unit
- or else (Is_Ancestor_Package (Parent_Unit, Scope (State_Id))
- and then
- not Is_Private_Descendant (Scope (State_Id)))
- then
- null;
-
- else
- SPARK_Msg_NE
- ("indicator Part_Of must denote an abstract state or "
- & "public descendant of & (SPARK RM 7.2.6(3))",
- Indic, Parent_Unit);
- end if;
-
- -- Indicator Part_Of is not needed when the related package is not
- -- a private child unit or a public descendant thereof.
-
- else
- SPARK_Msg_N
- ("indicator Part_Of cannot appear in this context "
- & "(SPARK RM 7.2.6(5))", Indic);
- Error_Msg_Name_1 := Chars (Pack_Id);
- SPARK_Msg_NE
- ("\& is declared in the visible part of package %",
- Indic, Item_Id);
- end if;
-
- -- When the item appears in the private state space of a package, the
- -- encapsulating state must be declared in the same package.
-
- elsif Placement = Private_State_Space then
- if Scope (State_Id) /= Pack_Id then
- SPARK_Msg_NE
- ("indicator Part_Of must designate an abstract state of "
- & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
- Error_Msg_Name_1 := Chars (Pack_Id);
- SPARK_Msg_NE
- ("\& is declared in the private part of package %",
- Indic, Item_Id);
- end if;
-
- -- Items declared in the body state space of a package do not need
- -- Part_Of indicators as the refinement has already been seen.
-
- else
- SPARK_Msg_N
- ("indicator Part_Of cannot appear in this context "
- & "(SPARK RM 7.2.6(5))", Indic);
-
- if Scope (State_Id) = Pack_Id then
- Error_Msg_Name_1 := Chars (Pack_Id);
- SPARK_Msg_NE
- ("\& is declared in the body of package %", Indic, Item_Id);
- end if;
- end if;
-
- Legal := True;
- end Analyze_Part_Of;
-
--------------------------------
-- Analyze_Pre_Post_Condition --
--------------------------------
-- SIMPLE_OPTION
-- | NAME_VALUE_OPTION
- -- SIMPLE_OPTION ::= Ghost
+ -- SIMPLE_OPTION ::= Ghost | Synchronous
-- NAME_VALUE_OPTION ::=
-- Part_Of => ABSTRACT_STATE
is
-- Flags used to verify the consistency of options
- AR_Seen : Boolean := False;
- AW_Seen : Boolean := False;
- ER_Seen : Boolean := False;
- EW_Seen : Boolean := False;
- External_Seen : Boolean := False;
- Others_Seen : Boolean := False;
- Part_Of_Seen : Boolean := False;
+ AR_Seen : Boolean := False;
+ AW_Seen : Boolean := False;
+ ER_Seen : Boolean := False;
+ EW_Seen : Boolean := False;
+ External_Seen : Boolean := False;
+ Ghost_Seen : Boolean := False;
+ Others_Seen : Boolean := False;
+ Part_Of_Seen : Boolean := False;
+ Synchronous_Seen : Boolean := False;
-- Flags used to store the static value of all external states'
-- expressions.
Props : Node_Id := Empty;
begin
- Check_Duplicate_Option (Opt, External_Seen);
-
if Nkind (Opt) = N_Component_Association then
Props := Expression (Opt);
end if;
----------------------------
procedure Analyze_Part_Of_Option (Opt : Node_Id) is
- Encaps : constant Node_Id := Expression (Opt);
- Encaps_Id : Entity_Id;
- Legal : Boolean;
+ Encap : constant Node_Id := Expression (Opt);
+ Encap_Id : Entity_Id;
+ Legal : Boolean;
begin
Check_Duplicate_Option (Opt, Part_Of_Seen);
Analyze_Part_Of
- (Item_Id => State_Id,
- State => Encaps,
- Indic => First (Choices (Opt)),
- Legal => Legal);
+ (Indic => First (Choices (Opt)),
+ Item_Id => State_Id,
+ Encap => Encap,
+ Encap_Id => Encap_Id,
+ Legal => Legal);
- -- The Part_Of indicator turns an abstract state into a
- -- constituent of the encapsulating state.
+ -- The Part_Of indicator transforms the abstract state into
+ -- a constituent of the encapsulating state or single
+ -- concurrent type.
if Legal then
- Encaps_Id := Entity (Encaps);
+ pragma Assert (Present (Encap_Id));
- Append_Elmt (State_Id, Part_Of_Constituents (Encaps_Id));
- Set_Encapsulating_State (State_Id, Encaps_Id);
+ Append_Elmt (State_Id, Part_Of_Constituents (Encap_Id));
+ Set_Encapsulating_State (State_Id, Encap_Id);
end if;
end Analyze_Part_Of_Option;
Ancestor_Part (State));
end if;
- -- Options External and Ghost appear as expressions
+ -- Options External, Ghost and Synchronous appear as
+ -- expressions.
Opt := First (Expressions (State));
while Present (Opt) loop
if Nkind (Opt) = N_Identifier then
+
+ -- External
+
if Chars (Opt) = Name_External then
+ Check_Duplicate_Option (Opt, External_Seen);
Analyze_External_Option (Opt);
+ -- Ghost
+
elsif Chars (Opt) = Name_Ghost then
+ Check_Duplicate_Option (Opt, Ghost_Seen);
+
if Present (State_Id) then
Set_Is_Ghost_Entity (State_Id);
end if;
+ -- Synchronous
+
+ elsif Chars (Opt) = Name_Synchronous then
+ Check_Duplicate_Option (Opt, Synchronous_Seen);
+
-- Option Part_Of without an encapsulating state is
- -- illegal. (SPARK RM 7.1.4(9)).
+ -- illegal (SPARK RM 7.1.4(9)).
elsif Chars (Opt) = Name_Part_Of then
SPARK_Msg_N
- ("indicator Part_Of must denote an abstract "
- & "state", Opt);
+ ("indicator Part_Of must denote abstract state, "
+ & "single protected type or single task type",
+ Opt);
-- Do not emit an error message when a previous state
-- declaration with options was not parenthesized as
-- Local variables
+ Encap : Node_Id;
+ Encap_Id : Entity_Id;
Item_Id : Entity_Id;
Legal : Boolean;
- State : Node_Id;
- State_Id : Entity_Id;
Stmt : Node_Id;
-- Start of processing for Part_Of
elsif Nkind (Stmt) = N_Package_Instantiation then
null;
+ -- Single concurrent type declaration
+
+ elsif Is_Single_Concurrent_Type_Declaration (Stmt) then
+ null;
+
-- Otherwise the pragma is associated with an illegal construct
else
end if;
Item_Id := Defining_Entity (Stmt);
- State := Get_Pragma_Arg (Arg1);
+ Encap := Get_Pragma_Arg (Arg1);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
Mark_Pragma_As_Ghost (N, Item_Id);
- -- Detect any discrepancies between the placement of the object
- -- or package instantiation with respect to state space and the
- -- encapsulating state.
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Part_Of_In_Decl_Part or for completeness.
- Analyze_Part_Of
- (Item_Id => Item_Id,
- State => State,
- Indic => N,
- Legal => Legal);
+ Add_Contract_Item (N, Item_Id);
- if Legal then
+ -- A variable may act as consituent of a single concurrent type
+ -- which in turn could be declared after the variable. Due to this
+ -- discrepancy, the full analysis of indicator Part_Of is delayed
+ -- until the end of the enclosing declarative region (see routine
+ -- Analyze_Part_Of_In_Decl_Part).
- -- Add the pragma to the contract of the item. This aids with
- -- the detection of a missing but required Part_Of indicator.
+ if Ekind (Item_Id) = E_Variable then
+ null;
- Add_Contract_Item (N, Item_Id);
+ -- Otherwise indicator Part_Of applies to a constant or a package
+ -- instantiation.
- -- The Part_Of indicator turns an object into a constituent of
- -- the encapsulating state.
+ else
+ -- Detect any discrepancies between the placement of the
+ -- constant or package instantiation with respect to state
+ -- space and the encapsulating state.
- State_Id := Entity (State);
+ Analyze_Part_Of
+ (Indic => N,
+ Item_Id => Item_Id,
+ Encap => Encap,
+ Encap_Id => Encap_Id,
+ Legal => Legal);
- 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);
+ if Legal then
+ pragma Assert (Present (Encap_Id));
- -- Propagate the Part_Of indicator to the visible state space
- -- of the package instantiation.
+ if Ekind (Item_Id) = E_Constant then
+ Append_Elmt (Item_Id, Part_Of_Constituents (Encap_Id));
+ Set_Encapsulating_State (Item_Id, Encap_Id);
- else
- Propagate_Part_Of
- (Pack_Id => Item_Id,
- State_Id => State_Id,
- Instance => Stmt);
+ -- Propagate the Part_Of indicator to the visible state
+ -- space of the package instantiation.
+
+ else
+ Propagate_Part_Of
+ (Pack_Id => Item_Id,
+ State_Id => Encap_Id,
+ Instance => Stmt);
+ end if;
end if;
end if;
end Part_Of;
--------------------------
procedure Process_Overloadable (Decl : Node_Id) is
- Spec_Id : constant Entity_Id := Defining_Entity (Decl);
+ Spec_Id : constant Entity_Id := Defining_Entity (Decl);
+ Spec_Typ : constant Entity_Id := Etype (Spec_Id);
begin
Check_Library_Level_Entity (Spec_Id);
Set_SPARK_Pragma (Spec_Id, N);
Set_SPARK_Pragma_Inherited (Spec_Id, False);
+
+ -- When the pragma applies to the anonymous object created for
+ -- a single task type, decorate the type as well. This scenario
+ -- arises when the single task type lacks a task definition,
+ -- therefore there is no issue with respect to a potential
+ -- pragma SPARK_Mode in the private part.
+
+ -- task type Anon_Task_Typ;
+ -- Obj : Anon_Task_Typ;
+ -- pragma SPARK_Mode ...;
+
+ if Is_Single_Concurrent_Object (Spec_Id)
+ and then Ekind (Spec_Typ) = E_Task_Type
+ then
+ Set_SPARK_Pragma (Spec_Typ, N);
+ Set_SPARK_Pragma_Inherited (Spec_Typ, False);
+ Set_SPARK_Aux_Pragma (Spec_Typ, N);
+ Set_SPARK_Aux_Pragma_Inherited (Spec_Typ, True);
+ end if;
end Process_Overloadable;
--------------------------
procedure Process_Visible_Part (Decl : Node_Id) is
Spec_Id : constant Entity_Id := Defining_Entity (Decl);
+ Obj_Id : Entity_Id;
begin
Check_Library_Level_Entity (Spec_Id);
Set_SPARK_Pragma_Inherited (Spec_Id, False);
Set_SPARK_Aux_Pragma (Spec_Id, N);
Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+
+ -- When the pragma applies to a single protected or task type,
+ -- decorate the corresponding anonymous object as well.
+
+ -- protected Anon_Prot_Typ is
+ -- pragma SPARK_Mode ...;
+ -- ...
+ -- end Anon_Prot_Typ;
+
+ -- Obj : Anon_Prot_Typ;
+
+ if Is_Single_Concurrent_Type (Spec_Id) then
+ Obj_Id := Anonymous_Object (Spec_Id);
+
+ Set_SPARK_Pragma (Obj_Id, N);
+ Set_SPARK_Pragma_Inherited (Obj_Id, False);
+ end if;
end Process_Visible_Part;
-----------------------
Process_Overloadable (Stmt);
return;
- -- The pragma applies to a task unit without a definition.
- -- This also handles the case where a single task unit is
- -- rewritten into a task type declaration.
-
- -- task [type] Tsk;
- -- pragma SPARK_Mode ...;
-
- elsif Nkind_In (Stmt, N_Single_Task_Declaration,
- N_Task_Type_Declaration)
- then
- Process_Visible_Part (Stmt);
- return;
-
-- Skip internally generated code
elsif not Comes_From_Source (Stmt) then
Process_Overloadable (Stmt);
return;
+ -- The pragma applies to the anonymous object created for a
+ -- single concurrent type.
+
+ -- protected type Anon_Prot_Typ ...;
+ -- Obj : Anon_Prot_Typ;
+ -- pragma SPARK_Mode ...;
+
+ elsif Nkind (Stmt) = N_Object_Declaration
+ and then Is_Single_Concurrent_Object
+ (Defining_Entity (Stmt))
+ then
+ Process_Overloadable (Stmt);
+ return;
+
-- Otherwise the pragma does not apply to a legal construct
-- or it does not appear at the top of a declarative or a
-- statement list. Issue an error and stop the analysis.
end if;
Spec_Id := Unique_Defining_Entity (Body_Decl);
+
+ -- Use the anonymous object as the proper spec when Refined_Depends
+ -- applies to the body of a single task type. The object carries the
+ -- proper Chars as well as all non-refined versions of pragmas.
+
+ if Is_Single_Concurrent_Type (Spec_Id) then
+ Spec_Id := Anonymous_Object (Spec_Id);
+ end if;
+
Depends := Get_Pragma (Spec_Id, Pragma_Depends);
-- Subprogram declarations lacks pragma Depends. Refined_Depends is
end if;
Spec_Id := Unique_Defining_Entity (Body_Decl);
- Global := Get_Pragma (Spec_Id, Pragma_Global);
- Items := Expression (Get_Argument (N, Spec_Id));
+
+ -- Use the anonymous object as the proper spec when Refined_Global
+ -- applies to the body of a single task type. The object carries the
+ -- proper Chars as well as all non-refined versions of pragmas.
+
+ if Is_Single_Concurrent_Type (Spec_Id) then
+ Spec_Id := Anonymous_Object (Spec_Id);
+ end if;
+
+ Global := Get_Pragma (Spec_Id, Pragma_Global);
+ Items := Expression (Get_Argument (N, Spec_Id));
-- The subprogram declaration lacks pragma Global. This renders
-- Refined_Global useless as there is nothing to refine.
-- should be set when the property applies to the refined state. If
-- this is not the case, emit an error message.
- procedure Check_Matching_State;
+ procedure Match_State;
-- Determine whether the state being refined appears in list
-- Available_States. Emit an error when attempting to re-refine the
-- state or when the state is not defined in the package declaration,
-------------------------
procedure Analyze_Constituent (Constit : Node_Id) is
- procedure Check_Ghost_Constituent (Constit_Id : Entity_Id);
- -- Verify that the constituent Constit_Id is a Ghost entity if the
- -- abstract state being refined is also Ghost. If this is the case
- -- verify that the Ghost policy in effect at the point of state
- -- and constituent declaration is the same.
-
- procedure Check_Matching_Constituent (Constit_Id : Entity_Id);
+ procedure Match_Constituent (Constit_Id : Entity_Id);
-- Determine whether constituent Constit denoted by its entity
-- Constit_Id appears in Body_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 Body_States.
- --------------------------------
- -- Check_Matching_Constituent --
- --------------------------------
+ -----------------------
+ -- Match_Constituent --
+ -----------------------
- procedure Check_Matching_Constituent (Constit_Id : Entity_Id) is
+ procedure Match_Constituent (Constit_Id : Entity_Id) is
procedure Collect_Constituent;
- -- Add constituent Constit_Id to the refinements of State_Id
+ -- Verify the legality of constituent Constit_Id and add it to
+ -- the refinements of State_Id.
-------------------------
-- Collect_Constituent --
procedure Collect_Constituent is
begin
+ if Is_Ghost_Entity (State_Id) then
+ if Is_Ghost_Entity (Constit_Id) then
+
+ -- The Ghost policy in effect at the point of abstract
+ -- state declaration and constituent must match
+ -- (SPARK RM 6.9(16)).
+
+ if Is_Checked_Ghost_Entity (State_Id)
+ and then Is_Ignored_Ghost_Entity (Constit_Id)
+ then
+ Error_Msg_Sloc := Sloc (Constit);
+
+ SPARK_Msg_N
+ ("incompatible ghost policies in effect", State);
+ SPARK_Msg_NE
+ ("\abstract state & declared with ghost policy "
+ & "Check", State, State_Id);
+ SPARK_Msg_NE
+ ("\constituent & declared # with ghost policy "
+ & "Ignore", State, Constit_Id);
+
+ elsif Is_Ignored_Ghost_Entity (State_Id)
+ and then Is_Checked_Ghost_Entity (Constit_Id)
+ then
+ Error_Msg_Sloc := Sloc (Constit);
+
+ SPARK_Msg_N
+ ("incompatible ghost policies in effect", State);
+ SPARK_Msg_NE
+ ("\abstract state & declared with ghost policy "
+ & "Ignore", State, State_Id);
+ SPARK_Msg_NE
+ ("\constituent & declared # with ghost policy "
+ & "Check", State, Constit_Id);
+ end if;
+
+ -- A constituent of a Ghost abstract state must be a
+ -- Ghost entity (SPARK RM 7.2.2(12)).
+
+ else
+ SPARK_Msg_NE
+ ("constituent of ghost state & must be ghost",
+ Constit, State_Id);
+ end if;
+ end if;
+
+ -- A synchronized state must be refined by a synchronized
+ -- object or another synchronized state (SPARK RM 9.6).
+
+ if Is_Synchronized_State (State_Id)
+ and then not Is_Synchronized_Object (Constit_Id)
+ and then not Is_Synchronized_State (Constit_Id)
+ then
+ SPARK_Msg_NE
+ ("constituent of synchronized state & must be "
+ & "synchronized", Constit, State_Id);
+ end if;
+
-- Add the constituent to the list of processed items to aid
-- with the detection of duplicates.
State_Elmt : Elmt_Id;
- -- Start of processing for Check_Matching_Constituent
+ -- Start of processing for Match_Constituent
begin
-- Detect a duplicate use of a constituent
if Present (Encapsulating_State (Constit_Id)) then
if Encapsulating_State (Constit_Id) = State_Id then
- Check_Ghost_Constituent (Constit_Id);
Remove (Part_Of_Constits, Constit_Id);
Collect_Constituent;
("& cannot act as constituent of state %",
Constit, Constit_Id);
SPARK_Msg_NE
- ("\Part_Of indicator specifies & as encapsulating "
- & "state", Constit, Encapsulating_State (Constit_Id));
+ ("\Part_Of indicator specifies encapsulator &",
+ Constit, Encapsulating_State (Constit_Id));
end if;
-- The only other source of legal constituents is the body
-- been encountered.
if Node (State_Elmt) = Constit_Id then
- Check_Ghost_Constituent (Constit_Id);
Remove_Elmt (Body_States, State_Elmt);
Collect_Constituent;
return;
& "hidden state of package %", Constit, Constit_Id);
end if;
end if;
- end Check_Matching_Constituent;
-
- -----------------------------
- -- Check_Ghost_Constituent --
- -----------------------------
-
- procedure Check_Ghost_Constituent (Constit_Id : Entity_Id) is
- begin
- if Is_Ghost_Entity (State_Id) then
- if Is_Ghost_Entity (Constit_Id) then
-
- -- The Ghost policy in effect at the point of abstract
- -- state declaration and constituent must match
- -- (SPARK RM 6.9(16)).
-
- if Is_Checked_Ghost_Entity (State_Id)
- and then Is_Ignored_Ghost_Entity (Constit_Id)
- then
- Error_Msg_Sloc := Sloc (Constit);
-
- SPARK_Msg_N
- ("incompatible ghost policies in effect", State);
- SPARK_Msg_NE
- ("\abstract state & declared with ghost policy "
- & "Check", State, State_Id);
- SPARK_Msg_NE
- ("\constituent & declared # with ghost policy "
- & "Ignore", State, Constit_Id);
-
- elsif Is_Ignored_Ghost_Entity (State_Id)
- and then Is_Checked_Ghost_Entity (Constit_Id)
- then
- Error_Msg_Sloc := Sloc (Constit);
-
- SPARK_Msg_N
- ("incompatible ghost policies in effect", State);
- SPARK_Msg_NE
- ("\abstract state & declared with ghost policy "
- & "Ignore", State, State_Id);
- SPARK_Msg_NE
- ("\constituent & declared # with ghost policy "
- & "Check", State, Constit_Id);
- end if;
-
- -- A constituent of a Ghost abstract state must be a Ghost
- -- entity (SPARK RM 7.2.2(12)).
-
- else
- SPARK_Msg_NE
- ("constituent of ghost state & must be ghost",
- Constit, State_Id);
- end if;
- end if;
- end Check_Ghost_Constituent;
+ end Match_Constituent;
-- Local variables
E_Constant,
E_Variable)
then
- Check_Matching_Constituent (Constit_Id);
+ Match_Constituent (Constit_Id);
-- Otherwise the constituent is illegal
end if;
end Check_External_Property;
- --------------------------
- -- Check_Matching_State --
- --------------------------
+ -----------------
+ -- Match_State --
+ -----------------
- procedure Check_Matching_State is
+ procedure Match_State is
State_Elmt : Elmt_Id;
begin
SPARK_Msg_NE
("cannot refine state, & is not defined in package %",
State, State_Id);
- end Check_Matching_State;
+ end Match_State;
--------------------------------
-- Report_Unused_Constituents --
-- is not defined in the package declaration.
elsif Ekind (State_Id) = E_Abstract_State then
- Check_Matching_State;
+ Match_State;
else
- SPARK_Msg_NE
- ("& must denote an abstract state", State, State_Id);
+ SPARK_Msg_NE ("& must denote abstract state", State, State_Id);
return;
end if;
begin
-- Since a constituent may be part of a larger constituent set, climb
- -- the encapsulated state chain looking for a state that appears in
+ -- the encapsulating state chain looking for a state that appears in
-- the same context.
State_Id := Encapsulating_State (Constit_Id);
elsif Present (Generic_Parent (Specification (Stmt))) then
return Stmt;
end if;
-
- -- The pragma applies to a single task declaration rewritten as a
- -- task type.
-
- elsif Nkind (Stmt) = N_Task_Type_Declaration
- and then Nkind (Original_Node (Stmt)) = N_Single_Task_Declaration
- then
- return Stmt;
end if;
-- Return the current construct which is either a subprogram body,
end if;
end Find_Related_Package_Or_Body;
- -------------
- -- Fix_Msg --
- -------------
-
- function Fix_Msg (Id : Entity_Id; Msg : String) return String is
- Msg_Last : constant Natural := Msg'Last;
- Msg_Index : Natural;
- Res : String (Msg'Range) := (others => ' ');
- Res_Index : Natural;
-
- begin
- -- Copy all characters from the input message Msg to result Res with
- -- suitable replacements.
-
- Msg_Index := Msg'First;
- Res_Index := Res'First;
- while Msg_Index <= Msg_Last loop
-
- -- Replace "subprogram" with a different word
-
- if Msg_Index <= Msg_Last - 10
- and then Msg (Msg_Index .. Msg_Index + 9) = "subprogram"
- then
- if Ekind_In (Id, E_Entry, E_Entry_Family) then
- Res (Res_Index .. Res_Index + 4) := "entry";
- Res_Index := Res_Index + 5;
-
- elsif Ekind_In (Id, E_Task_Body, E_Task_Type) then
- Res (Res_Index .. Res_Index + 8) := "task unit";
- Res_Index := Res_Index + 9;
-
- else
- Res (Res_Index .. Res_Index + 9) := "subprogram";
- Res_Index := Res_Index + 10;
- end if;
-
- Msg_Index := Msg_Index + 10;
-
- -- Otherwise copy the character
-
- else
- Res (Res_Index) := Msg (Msg_Index);
- Msg_Index := Msg_Index + 1;
- Res_Index := Res_Index + 1;
- end if;
- end loop;
-
- return Res (Res'First .. Res_Index - 1);
- end Fix_Msg;
-
------------------
-- Get_Argument --
------------------
end loop;
end Record_Possible_Body_Reference;
+ ------------------------------------------
+ -- Relocate_Pragmas_To_Anonymous_Object --
+ ------------------------------------------
+
+ procedure Relocate_Pragmas_To_Anonymous_Object
+ (Typ_Decl : Node_Id;
+ Obj_Decl : Node_Id)
+ is
+ Decl : Node_Id;
+ Def : Node_Id;
+ Next_Decl : Node_Id;
+
+ begin
+ if Nkind (Typ_Decl) = N_Protected_Type_Declaration then
+ Def := Protected_Definition (Typ_Decl);
+ else
+ pragma Assert (Nkind (Typ_Decl) = N_Task_Type_Declaration);
+ Def := Task_Definition (Typ_Decl);
+ end if;
+
+ -- The concurrent definition has a visible declaration list. Inspect it
+ -- and relocate all canidate pragmas.
+
+ if Present (Def) and then Present (Visible_Declarations (Def)) then
+ Decl := First (Visible_Declarations (Def));
+ while Present (Decl) loop
+
+ -- Preserve the following declaration for iteration purposes due
+ -- to possible relocation of a pragma.
+
+ Next_Decl := Next (Decl);
+
+ if Nkind (Decl) = N_Pragma
+ and then Pragma_On_Anonymous_Object_OK (Get_Pragma_Id (Decl))
+ then
+ Remove (Decl);
+ Insert_After (Obj_Decl, Decl);
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Decl) then
+ null;
+
+ -- No candidate pragmas are available for relocation
+
+ else
+ exit;
+ end if;
+
+ Decl := Next_Decl;
+ end loop;
+ end if;
+ end Relocate_Pragmas_To_Anonymous_Object;
+
------------------------------
-- Relocate_Pragmas_To_Body --
------------------------------
Pragma_Type_Invariant_Class => True,
others => False);
+ -- The following table lists all the implementation-defined pragmas that
+ -- should apply to the anonymous object produced by the analysis of a
+ -- single protected or task type. The table should be synchronized with
+ -- Aspect_On_Anonymous_Object_OK in unit Aspects.
+
+ Pragma_On_Anonymous_Object_OK : constant array (Pragma_Id) of Boolean :=
+ (Pragma_Depends => True,
+ Pragma_Global => True,
+ Pragma_Part_Of => True,
+ others => False);
+
-- The following table lists all the implementation-defined pragmas that
-- may apply to a body stub (no language defined pragmas apply). The table
- -- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects if
- -- the pragmas below implement an aspect.
+ -- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects.
Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean :=
(Pragma_Refined_Depends => True,
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initializes
+ procedure Analyze_Part_Of_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Part_Of
+
procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id);
- -- Perform preanalysis of [refined] precondition or postcondition pragma
- -- N that appears on a subprogram declaration or body [stub].
+ -- Perform full analysis of pragmas Precondition and Postcondition
procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
-- Preform full analysis of delayed pragma Refined_Depends. This routine
-- Suppress_All at this stage, since it can appear after the unit instead
-- of before (actually we allow it to appear anywhere).
+ procedure Relocate_Pragmas_To_Anonymous_Object
+ (Typ_Decl : Node_Id;
+ Obj_Decl : Node_Id);
+ -- Relocate all pragmas that appear in the visible declarations of task or
+ -- protected type declaration Typ_Decl after the declaration of anonymous
+ -- object Obj_Decl. Table Pragmas_On_Anonymous_Object_OK contains the list
+ -- of candidate pragmas.
+
procedure Relocate_Pragmas_To_Body
(Subp_Body : Node_Id;
Target_Body : Node_Id := Empty);
---------------------
function Defining_Entity (N : Node_Id) return Entity_Id is
- K : constant Node_Kind := Nkind (N);
Err : Entity_Id := Empty;
begin
- case K is
- when
- N_Subprogram_Declaration |
- N_Abstract_Subprogram_Declaration |
- N_Subprogram_Body |
- N_Package_Declaration |
- N_Subprogram_Renaming_Declaration |
- N_Subprogram_Body_Stub |
- N_Generic_Subprogram_Declaration |
- N_Generic_Package_Declaration |
- N_Formal_Subprogram_Declaration |
- N_Expression_Function
+ case Nkind (N) is
+ when N_Abstract_Subprogram_Declaration |
+ N_Expression_Function |
+ N_Formal_Subprogram_Declaration |
+ N_Generic_Package_Declaration |
+ N_Generic_Subprogram_Declaration |
+ N_Package_Declaration |
+ N_Subprogram_Body |
+ N_Subprogram_Body_Stub |
+ N_Subprogram_Declaration |
+ N_Subprogram_Renaming_Declaration
=>
return Defining_Entity (Specification (N));
- when
- N_Component_Declaration |
- N_Defining_Program_Unit_Name |
- N_Discriminant_Specification |
- N_Entry_Body |
- N_Entry_Declaration |
- N_Entry_Index_Specification |
- N_Exception_Declaration |
- N_Exception_Renaming_Declaration |
- N_Formal_Object_Declaration |
- N_Formal_Package_Declaration |
- N_Formal_Type_Declaration |
- N_Full_Type_Declaration |
- N_Implicit_Label_Declaration |
- N_Incomplete_Type_Declaration |
- N_Loop_Parameter_Specification |
- N_Number_Declaration |
- N_Object_Declaration |
- N_Object_Renaming_Declaration |
- N_Package_Body_Stub |
- N_Parameter_Specification |
- N_Private_Extension_Declaration |
- N_Private_Type_Declaration |
- N_Protected_Body |
- N_Protected_Body_Stub |
- N_Protected_Type_Declaration |
- N_Single_Protected_Declaration |
- N_Single_Task_Declaration |
- N_Subtype_Declaration |
- N_Task_Body |
- N_Task_Body_Stub |
- N_Task_Type_Declaration
+ when N_Component_Declaration |
+ N_Defining_Program_Unit_Name |
+ N_Discriminant_Specification |
+ N_Entry_Body |
+ N_Entry_Declaration |
+ N_Entry_Index_Specification |
+ N_Exception_Declaration |
+ N_Exception_Renaming_Declaration |
+ N_Formal_Object_Declaration |
+ N_Formal_Package_Declaration |
+ N_Formal_Type_Declaration |
+ N_Full_Type_Declaration |
+ N_Implicit_Label_Declaration |
+ N_Incomplete_Type_Declaration |
+ N_Loop_Parameter_Specification |
+ N_Number_Declaration |
+ N_Object_Declaration |
+ N_Object_Renaming_Declaration |
+ N_Package_Body_Stub |
+ N_Parameter_Specification |
+ N_Private_Extension_Declaration |
+ N_Private_Type_Declaration |
+ N_Protected_Body |
+ N_Protected_Body_Stub |
+ N_Protected_Type_Declaration |
+ N_Single_Protected_Declaration |
+ N_Single_Task_Declaration |
+ N_Subtype_Declaration |
+ N_Task_Body |
+ N_Task_Body_Stub |
+ N_Task_Type_Declaration
=>
return Defining_Identifier (N);
when N_Subunit =>
return Defining_Entity (Proper_Body (N));
- when
- N_Function_Instantiation |
- N_Function_Specification |
- N_Generic_Function_Renaming_Declaration |
- N_Generic_Package_Renaming_Declaration |
- N_Generic_Procedure_Renaming_Declaration |
- N_Package_Body |
- N_Package_Instantiation |
- N_Package_Renaming_Declaration |
- N_Package_Specification |
- N_Procedure_Instantiation |
- N_Procedure_Specification
+ when N_Function_Instantiation |
+ N_Function_Specification |
+ N_Generic_Function_Renaming_Declaration |
+ N_Generic_Package_Renaming_Declaration |
+ N_Generic_Procedure_Renaming_Declaration |
+ N_Package_Body |
+ N_Package_Instantiation |
+ N_Package_Renaming_Declaration |
+ N_Package_Specification |
+ N_Procedure_Instantiation |
+ N_Procedure_Specification
=>
declare
Nam : constant Node_Id := Defining_Unit_Name (N);
if Nkind (Nam) in N_Entity then
return Nam;
- -- For Error, make up a name and attach to declaration
- -- so we can continue semantic analysis
+ -- For Error, make up a name and attach to declaration so we
+ -- can continue semantic analysis.
elsif Nam = Error then
Err := Make_Temporary (Sloc (N), 'T');
end if;
end;
- when
- N_Block_Statement |
- N_Loop_Statement
- =>
+ when N_Block_Statement |
+ N_Loop_Statement =>
return Entity (Identifier (N));
when others =>
end if;
end First_Actual;
+ -------------
+ -- Fix_Msg --
+ -------------
+
+ function Fix_Msg (Id : Entity_Id; Msg : String) return String is
+ Is_Task : constant Boolean :=
+ Ekind_In (Id, E_Task_Body, E_Task_Type)
+ or else (Is_Single_Concurrent_Object (Id)
+ and then Ekind (Etype (Id)) = E_Task_Type);
+ Msg_Last : constant Natural := Msg'Last;
+ Msg_Index : Natural;
+ Res : String (Msg'Range) := (others => ' ');
+ Res_Index : Natural;
+
+ begin
+ -- Copy all characters from the input message Msg to result Res with
+ -- suitable replacements.
+
+ Msg_Index := Msg'First;
+ Res_Index := Res'First;
+ while Msg_Index <= Msg_Last loop
+
+ -- Replace "subprogram" with a different word
+
+ if Msg_Index <= Msg_Last - 10
+ and then Msg (Msg_Index .. Msg_Index + 9) = "subprogram"
+ then
+ if Ekind_In (Id, E_Entry, E_Entry_Family) then
+ Res (Res_Index .. Res_Index + 4) := "entry";
+ Res_Index := Res_Index + 5;
+
+ elsif Is_Task then
+ Res (Res_Index .. Res_Index + 8) := "task unit";
+ Res_Index := Res_Index + 9;
+
+ else
+ Res (Res_Index .. Res_Index + 9) := "subprogram";
+ Res_Index := Res_Index + 10;
+ end if;
+
+ Msg_Index := Msg_Index + 10;
+
+ -- Replace "protected" with a different word
+
+ elsif Msg_Index <= Msg_Last - 9
+ and then Msg (Msg_Index .. Msg_Index + 8) = "protected"
+ and then Is_Task
+ then
+ Res (Res_Index .. Res_Index + 3) := "task";
+ Res_Index := Res_Index + 4;
+ Msg_Index := Msg_Index + 9;
+
+ -- Otherwise copy the character
+
+ else
+ Res (Res_Index) := Msg (Msg_Index);
+ Msg_Index := Msg_Index + 1;
+ Res_Index := Res_Index + 1;
+ end if;
+ end loop;
+
+ return Res (Res'First .. Res_Index - 1);
+ end Fix_Msg;
+
-----------------------
-- Gather_Components --
-----------------------
end if;
end Has_Enabled_Property;
+ -------------------------------------
+ -- Has_Full_Default_Initialization --
+ -------------------------------------
+
+ function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
+ Comp : Entity_Id;
+
+ begin
+ -- A scalar type is fully default initialized if it is subjec to aspect
+ -- Default_Value.
+
+ if Is_Scalar_Type (Typ) then
+ return Has_Default_Aspect (Typ);
+
+ -- An array type is fully default initialized if its element type is
+ -- scalar and the array type carries aspect Default_Component_Value or
+ -- the element type is fully default initialized.
+
+ elsif Is_Array_Type (Typ) then
+ return
+ Has_Default_Aspect (Typ)
+ or else Has_Full_Default_Initialization (Component_Type (Typ));
+
+ -- A protected type, record type or type extension is fully default
+ -- initialized if all its components either carry an initialization
+ -- expression or have a type that is fully default initialized. The
+ -- parent type of a type extension must be fully default initialized.
+
+ elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then
+
+ -- Inspect all entities defined in the scope of the type, looking for
+ -- uninitialized components.
+
+ Comp := First_Entity (Typ);
+ while Present (Comp) loop
+ if Ekind (Comp) = E_Component
+ and then Comes_From_Source (Comp)
+ and then No (Expression (Parent (Comp)))
+ and then not Has_Full_Default_Initialization (Etype (Comp))
+ then
+ return False;
+ end if;
+
+ Next_Entity (Comp);
+ end loop;
+
+ -- Ensure that the parent type of a type extension is fully default
+ -- initialized.
+
+ if Etype (Typ) /= Typ
+ and then not Has_Full_Default_Initialization (Etype (Typ))
+ then
+ return False;
+ end if;
+
+ -- If we get here, then all components and parent portion are fully
+ -- default initialized.
+
+ return True;
+
+ -- A task type is fully default initialized by default
+
+ elsif Is_Task_Type (Typ) then
+ return True;
+ end if;
+
+ -- A private type and by extension its full view is fully default
+ -- initialized if it is subject to pragma Default_Initial_Condition
+ -- with a non-null argument or inherits the pragma from a parent type.
+ -- Since any type can act as the full view of a private type, this check
+ -- is separated from the circuitry above.
+
+ if Has_Default_Init_Cond (Typ)
+ or else Has_Inherited_Default_Init_Cond (Typ)
+ then
+ return
+ Nkind (First (Pragma_Argument_Associations (Get_Pragma
+ (Typ, Pragma_Default_Initial_Condition)))) /= N_Null;
+
+ -- Otherwise the type is not fully default initialized
+
+ else
+ return False;
+ end if;
+ end Has_Full_Default_Initialization;
+
--------------------
-- Has_Infinities --
--------------------
end if;
end Is_Descendent_Of;
+ ----------------------------------------
+ -- Is_Descendant_Of_Suspension_Object --
+ ----------------------------------------
+
+ function Is_Descendant_Of_Suspension_Object
+ (Typ : Entity_Id) return Boolean
+ is
+ Cur_Typ : Entity_Id;
+ Par_Typ : Entity_Id;
+
+ begin
+ -- Climb the type derivation chain checking each parent type against
+ -- Suspension_Object.
+
+ Cur_Typ := Base_Type (Typ);
+ while Present (Cur_Typ) loop
+ Par_Typ := Etype (Cur_Typ);
+
+ -- The current type is a match
+
+ if Is_Suspension_Object (Cur_Typ) then
+ return True;
+
+ -- Stop the traversal once the root of the derivation chain has been
+ -- reached. In that case the current type is its own base type.
+
+ elsif Cur_Typ = Par_Typ then
+ exit;
+ end if;
+
+ Cur_Typ := Base_Type (Par_Typ);
+ end loop;
+
+ return False;
+ end Is_Descendant_Of_Suspension_Object;
+
---------------------------------------------
-- Is_Double_Precision_Floating_Point_Type --
---------------------------------------------
-----------------------------
function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is
- function Is_Descendant_Of_Suspension_Object
- (Typ : Entity_Id) return Boolean;
- -- Determine whether type Typ is a descendant of type Suspension_Object
- -- defined in Ada.Synchronous_Task_Control.
-
- ----------------------------------------
- -- Is_Descendant_Of_Suspension_Object --
- ----------------------------------------
-
- function Is_Descendant_Of_Suspension_Object
- (Typ : Entity_Id) return Boolean
- is
- Cur_Typ : Entity_Id;
- Par_Typ : Entity_Id;
-
- begin
- -- Climb the type derivation chain checking each parent type against
- -- Suspension_Object.
-
- Cur_Typ := Base_Type (Typ);
- while Present (Cur_Typ) loop
- Par_Typ := Etype (Cur_Typ);
-
- -- The current type is a match
-
- if Is_Suspension_Object (Cur_Typ) then
- return True;
-
- -- Stop the traversal once the root of the derivation chain has
- -- been reached. In that case the current type is its own base
- -- type.
-
- elsif Cur_Typ = Par_Typ then
- exit;
- end if;
-
- Cur_Typ := Base_Type (Par_Typ);
- end loop;
-
- return False;
- end Is_Descendant_Of_Suspension_Object;
-
- -- Start of processing for Is_Effectively_Volatile
-
begin
if Is_Type (Id) then
end if;
end Is_Selector_Name;
+ ---------------------------------
+ -- Is_Single_Concurrent_Object --
+ ---------------------------------
+
+ function Is_Single_Concurrent_Object (Id : Entity_Id) return Boolean is
+ begin
+ return
+ Ekind (Id) = E_Variable
+ and then Is_Single_Concurrent_Type (Etype (Id));
+ end Is_Single_Concurrent_Object;
+
+ -------------------------------
+ -- Is_Single_Concurrent_Type --
+ -------------------------------
+
+ function Is_Single_Concurrent_Type (Id : Entity_Id) return Boolean is
+ begin
+ return
+ Ekind_In (Id, E_Protected_Type, E_Task_Type)
+ and then Is_Single_Concurrent_Type_Declaration
+ (Declaration_Node (Id));
+ end Is_Single_Concurrent_Type;
+
+ -------------------------------------------
+ -- Is_Single_Concurrent_Type_Declaration --
+ -------------------------------------------
+
+ function Is_Single_Concurrent_Type_Declaration
+ (N : Node_Id) return Boolean
+ is
+ begin
+ return Nkind_In (Original_Node (N), N_Single_Protected_Declaration,
+ N_Single_Task_Declaration);
+ end Is_Single_Concurrent_Type_Declaration;
+
---------------------------------------------
-- Is_Single_Precision_Floating_Point_Type --
---------------------------------------------
and then Scope (Scope (Scope (Id))) = Standard_Standard;
end Is_Suspension_Object;
+ ----------------------------
+ -- Is_Synchronized_Object --
+ ----------------------------
+
+ function Is_Synchronized_Object (Id : Entity_Id) return Boolean is
+ Prag : Node_Id;
+
+ begin
+ if Is_Object (Id) then
+
+ -- The object is synchronized if it is of a type that yields a
+ -- synchronized object.
+
+ if Yields_Synchronized_Object (Etype (Id)) then
+ return True;
+
+ -- The object is synchronized if it is atomic and Async_Writers is
+ -- enabled.
+
+ elsif Is_Atomic (Id) and then Async_Writers_Enabled (Id) then
+ return True;
+
+ -- A constant is a synchronized object by default
+
+ elsif Ekind (Id) = E_Constant then
+ return True;
+
+ -- A variable is a synchronized object if it is subject to pragma
+ -- Constant_After_Elaboration.
+
+ elsif Ekind (Id) = E_Variable then
+ Prag := Get_Pragma (Id, Pragma_Constant_After_Elaboration);
+
+ return Present (Prag) and then Is_Enabled_Pragma (Prag);
+ end if;
+ end if;
+
+ -- Otherwise the input is not an object or it does not qualify as a
+ -- synchronized object.
+
+ return False;
+ end Is_Synchronized_Object;
+
---------------------------------
-- Is_Synchronized_Tagged_Type --
---------------------------------
end if;
end Wrong_Type;
+ --------------------------------
+ -- Yields_Synchronized_Object --
+ --------------------------------
+
+ function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean is
+ Id : Entity_Id;
+
+ begin
+ -- An array type yields a synchronized object if its component type
+ -- yields a synchronized object.
+
+ if Is_Array_Type (Typ) then
+ return Yields_Synchronized_Object (Component_Type (Typ));
+
+ -- A descendant of type Ada.Synchronous_Task_Control.Suspension_Object
+ -- yields a synchronized object by default.
+
+ elsif Is_Descendant_Of_Suspension_Object (Typ) then
+ return True;
+
+ -- A protected type yields a synchronized object by default
+
+ elsif Is_Protected_Type (Typ) then
+ return True;
+
+ -- A record type or type extension yields a synchronized object when its
+ -- discriminants (if any) lack default values and all components are of
+ -- a type that yelds a synchronized object.
+
+ elsif Is_Record_Type (Typ) then
+
+ -- Inspect all entities defined in the scope of the type, looking for
+ -- components of a type that does not yeld a synchronized object or
+ -- for discriminants with default values.
+
+ Id := First_Entity (Typ);
+ while Present (Id) loop
+ if Comes_From_Source (Id) then
+ if Ekind (Id) = E_Component
+ and then not Yields_Synchronized_Object (Etype (Id))
+ then
+ return False;
+
+ elsif Ekind (Id) = E_Discriminant
+ and then Present (Expression (Parent (Id)))
+ then
+ return False;
+ end if;
+ end if;
+
+ Next_Entity (Id);
+ end loop;
+
+ -- Ensure that the parent type of a type extension yields a
+ -- synchronized object.
+
+ if Etype (Typ) /= Typ
+ and then not Yields_Synchronized_Object (Etype (Typ))
+ then
+ return False;
+ end if;
+
+ -- If we get here, then all discriminants lack default values and all
+ -- components are of a type that yields a synchronized object.
+
+ return True;
+
+ -- A synchronized interface type yields a synchronized object by default
+
+ elsif Is_Synchronized_Interface (Typ) then
+ return True;
+
+ -- A task type yelds a synchronized object by default
+
+ elsif Is_Task_Type (Typ) then
+ return True;
+
+ -- Otherwise the type does not yield a synchronized object
+
+ else
+ return False;
+ end if;
+ end Yields_Synchronized_Object;
+
end Sem_Util;
-- Note that the value returned is always the expression (not the
-- N_Parameter_Association nodes, even if named association is used).
+ function Fix_Msg (Id : Entity_Id; Msg : String) return String;
+ -- Replace all occurrences of a particular word in string Msg depending on
+ -- the Ekind of Id as follows:
+ -- * Replace "subprogram" with
+ -- - "entry" when Id is an entry [family]
+ -- - "task unit" when Id is a single task object, task type or task
+ -- body.
+ -- * Replace "protected" with
+ -- - "task" when Id is a single task object, task type or task body
+ -- All other non-matching words remain as is
+
procedure Gather_Components
(Typ : Entity_Id;
Comp_List : Node_Id;
-- as an access type internally, this function tests only for access types
-- known to the programmer. See also Has_Tagged_Component.
- function Has_Defaulted_Discriminants (Typ : Entity_Id) return Boolean;
- -- Simple predicate to test for defaulted discriminants
-
type Alignment_Result is (Known_Compatible, Unknown, Known_Incompatible);
-- Result of Has_Compatible_Alignment test, description found below. Note
-- that the values are arranged in increasing order of problematicness.
function Has_Declarations (N : Node_Id) return Boolean;
-- Determines if the node can have declarations
+ function Has_Defaulted_Discriminants (Typ : Entity_Id) return Boolean;
+ -- Simple predicate to test for defaulted discriminants
+
function Has_Denormals (E : Entity_Id) return Boolean;
-- Determines if the floating-point type E supports denormal numbers.
-- Returns False if E is not a floating-point type.
-- Determine whether subprogram Subp_Id has an effectively volatile formal
-- parameter or returns an effectively volatile value.
+ function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ defines "full default initialization" as
+ -- specified by SPARK RM 3.1. To qualify as such, the type must be
+ -- * A scalar type with specified Default_Value
+ -- * An array-of-scalar type with specified Default_Component_Value
+ -- * An array type whose element type defines full default initialization
+ -- * A protected type, record type or type extension whose components
+ -- either include a default expression or have a type which defines
+ -- full default initialization. In the case of type extensions, the
+ -- parent type defines full default initialization.
+ -- * A task type
+ -- * A private type whose Default_Initial_Condition is non-null
+
function Has_Infinities (E : Entity_Id) return Boolean;
-- Determines if the range of the floating-point type E includes
-- infinities. Returns False if E is not a floating-point type.
-- This is the RM definition, a type is a descendent of another type if it
-- is the same type or is derived from a descendent of the other type.
+ function Is_Descendant_Of_Suspension_Object
+ (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ is a descendant of type Suspension_Object
+ -- defined in Ada.Synchronous_Task_Control. This version is different from
+ -- Is_Descendent_Of as the detection of Suspension_Object does not involve
+ -- an entity and by extension a call to RTSfind.
+
function Is_Double_Precision_Floating_Point_Type
(E : Entity_Id) return Boolean;
-- Return whether E is a double precision floating point type,
-- represent use of the N_Identifier node for a true identifier, when
-- normally such nodes represent a direct name.
+ function Is_Single_Concurrent_Object (Id : Entity_Id) return Boolean;
+ -- Determine whether arbitrary entity Id denotes the anonymous object
+ -- created for a single protected or single task type.
+
+ function Is_Single_Concurrent_Type (Id : Entity_Id) return Boolean;
+ -- Determine whether arbitrary entity Id denotes a single protected or
+ -- single task type.
+
+ function Is_Single_Concurrent_Type_Declaration (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes the declaration of a single
+ -- protected type or single task type.
+
function Is_Single_Precision_Floating_Point_Type
(E : Entity_Id) return Boolean;
-- Return whether E is a single precision floating point type,
-- Determine whether arbitrary entity Id denotes Suspension_Object defined
-- in Ada.Synchronous_Task_Control.
+ function Is_Synchronized_Object (Id : Entity_Id) return Boolean;
+ -- Determine whether entity Id denotes an object and if it does, whether
+ -- this object is synchronized as specified in SPARK RM 9.1. To qualify as
+ -- such, the object must be
+ -- * Of a type that yields a synchronized object
+ -- * An atomic object with enabled Async_Writers
+ -- * A constant
+ -- * A variable subject to pragma Constant_After_Elaboration
+
function Is_Synchronized_Tagged_Type (E : Entity_Id) return Boolean;
-- Returns True if E is a synchronized tagged type (AARM 3.9.4 (6/2))
-- does not have to be a subexpression, anything with an Etype field may
-- be used.
+ function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ "yields synchronized object" as specified by
+ -- SPARK RM 9.1. To qualify as such, a type must be
+ -- * An array type whose element type yields a synchronized object
+ -- * A descendant of type Ada.Synchronous_Task_Control.Suspension_Object
+ -- * A protected type
+ -- * A record type or type extension without defaulted discriminants
+ -- whose components are of a type that yields a synchronized object.
+ -- * A synchronized interface type
+ -- * A task type
+
end Sem_Util;
Name_Strict : constant Name_Id := N + $;
Name_Subunit_File_Name : constant Name_Id := N + $;
Name_Suppressed : constant Name_Id := N + $;
+ Name_Synchronous : constant Name_Id := N + $;
Name_Task_Stack_Size_Default : constant Name_Id := N + $;
Name_Task_Type : constant Name_Id := N + $;
Name_Time_Slicing_Enabled : constant Name_Id := N + $;
projects / thirdparty / gcc.git / commitdiff
