+2015-10-26 Claire Dross <dross@adacore.com>
+
+ * sem_aux.ads (Number_Components): Can return 0 when called on
+ an empty record.
+
+2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * contracts.adb (Analyze_Subprogram_Body_Contract): Use
+ Unique_Defining_Entity instead of Corresponding_Spec_Of.
+ * einfo.adb SPARK_Pragma and SPARK_Aux_Pragma are now Node40 and
+ Node41 respectively.
+ (SPARK_Aux_Pragma): Update the assertion and node querry.
+ (SPARK_Aux_Pragma_Inherited): Update the assertion and node query.
+ (SPARK_Pragma): Update the assertion and node query.
+ (SPARK_Pragma_Inherited): Update the assertion and node query.
+ (Set_SPARK_Aux_Pragma): Update the assertion and node setting.
+ (Set_SPARK_Aux_Pragma_Inherited): Update the assertion and node setting.
+ (Set_SPARK_Pragma): Update the assertion and node setting.
+ (Set_SPARK_Pragma_Inherited): Update the assertion and node setting.
+ (Write_Field32_Name): Remove the output for SPARK_Pragma.
+ (Write_Field33_Name): Remove the output for SPARK_Aux_Pragma.
+ (Write_Field40_Name): Add output for SPARK_Pragma.
+ (Write_Field41_Name): Add output for SPARK_Aux_Pragma.
+ * einfo.ads Rewrite the documentation on attributes
+ SPARK_Pragma, SPARK_Aux_Pragma, SPARK_Pragma_Inherited and
+ SPARK_Aux_Pragma_Inherited. Update their uses in nodes.
+ * exp_ch4.adb (Create_Anonymous_Master): Use
+ Unique_Defining_Entity instead of Corresponding_Spec_Of.
+ * exp_ch9.adb (Expand_Entry_Declaration): Mark the barrier
+ function as such.
+ (Expand_N_Task_Body): Mark the task body as such.
+ (Expand_N_Task_Type_Declaration): Mark the task body as such.
+ * exp_unst.adb (Visit_Node): Use Unique_Defining_Entity instead
+ of Corresponding_Spec_Of.
+ * sem_attr.adb (Analyze_Attribute_Old_Result): Use
+ Unique_Defining_Entity instead of Corresponding_Spec_Of.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Entry barrier
+ functions do not inherit the SPARK_Mode from the context.
+ (Build_Subprogram_Declaration): The matching spec is now marked
+ as a source construct to mimic the original stand alone body.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Code cleanup.
+ * sem_ch9.adb Add with and use clauses for Contracts.
+ (Analyze_Entry_Body): An entry body freezes the contract of
+ the nearest enclosing package body. The entry body now inherits
+ the SPARK_Mode from the context.
+ (Analyze_Entry_Declaration): A protected entry declaration now inherits
+ the SPARK_Mode from the context.
+ (Analyze_Protected_Body): A protected body freezes
+ the contract of the nearest enclosing package body. Set the
+ Etype of a protected body as this is neede for proper aspect
+ analysis. Protected bodies can now carry meaningful aspects and
+ those are now analyzed.
+ (Analyze_Protected_Type_Declaration): A protected type now inherits the
+ SPARK_Mode from the context.
+ (Analyze_Task_Body): A task body freezes the contract of the
+ nearest enclosing package body. Set the Etype of a task body
+ as this is needed for proper aspect analysis. A task body
+ now inherits the SPARK_Mode from the context. Task bodies
+ can now carry meaningful aspects and those are now analyzed.
+ (Analyze_Task_Type_Declaration): A task type declaration now
+ inherits the SPARK_Mode of from the context.
+ * sem_ch10.adb (Analyze_Protected_Body_Stub): Protected body
+ stubs can now carry meaningful aspects.
+ (Analyze_Task_Body_Stub): Task body stubs can now carry meaningful
+ aspects.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Aspects SPARK_Mode
+ Warnings now use routine Insert_Pragma as means of insertion into
+ the tree.
+ (Insert_After_SPARK_Mode): Clean up documentation.
+ (Insert_Pragma): Clean up documentation. The routine is now
+ capable of operating on synchronized units.
+ * sem_prag.adb (Add_Entity_To_Name_Buffer): New routine.
+ (Analyze_Contract_Cases_In_Decl_Part): Use
+ Unique_Defining_Entity instead of Corresponding_Spec_Of.
+ (Analyze_Depends_Global): Use Unique_Defining_Entity instead
+ of Corresponding_Spec_Of.
+ (Analyze_Depends_In_Decl_Part): Use Unique_Defining_Entity instead of
+ Corresponding_Spec_Of.
+ (Analyze_Global_In_Decl_Part): Use Unique_Defining_Entity instead of
+ Corresponding_Spec_Of.
+ (Analyze_Pragma): Use Unique_Defining_Entity instead of
+ Corresponding_Spec_Of.
+ Update the detection of an illegal pragma Ghost when it applies
+ to a task or protected unit. Reimplement the handling of
+ pragma SPARK_Mode.
+ (Analyze_Pre_Post_Condition_In_Decl_Part): Use Unique_Defining_Entity
+ instead of Corresponding_Spec_Of.
+ (Analyze_Test_Case_In_Decl_Part): Use Unique_Defining_Entity instead of
+ Corresponding_Spec_Of.
+ (Check_Library_Level_Entity): Update the comment on usage.
+ Reimplemented to offer a more specialized errror context.
+ (Check_Pragma_Conformance): Update profile and comment on usage.
+ Handle error message output on single protected or task units.
+ (Collect_Subprogram_Inputs_Outputs): Use Unique_Defining_Entity
+ instead of Corresponding_Spec_Of.
+ (Process_Body): New routine.
+ (Process_Overloadable): New routine.
+ (Process_Private_Part): New routine.
+ (Process_Statement_Part): New routine.
+ (Process_Visible_Part): New routine.
+ (Set_SPARK_Context): New routine.
+ (Set_SPARK_Flags): Removed.
+ * sem_util.adb (Corresponding_Spec_Of): Removed.
+ (Unique_Entity): Reimplemented to handle many more cases.
+ * sem_util.ads (Corresponding_Spec_Of): Removed.
+ (Unique_Defining_Entity): Update the comment on usage.
+ * sinfo.ads (Is_Entry_Barrier_Function): Update the assertion.
+ (Is_Task_Body_Procedure): New routine.
+ (Set_Is_Entry_Barrier_Function): Update the assertion.
+ (Set_Is_Task_Body_Procedure): New routine.
+ * sinfo.adb Update the documentation of attribute
+ Is_Entry_Barrier_Function along with use in nodes. Add new
+ attribute Is_Task_Body_Procedure along with use in nodes.
+ (Is_Task_Body_Procedure): New routine along with pragma Inline.
+ (Set_Is_Task_Body_Procedure): New routine along with pragma Inline.
+
2015-10-26 Gary Dismukes <dismukes@adacore.com>
* sem_ch13.adb: Minor reformatting.
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
Items : constant Node_Id := Contract (Body_Id);
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Body_Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
Mode : SPARK_Mode_Type;
Prag : Node_Id;
Prag_Nam : Name_Id;
-- Activation_Record_Component Node31
-- Encapsulating_State Node32
- -- SPARK_Pragma Node32
-- No_Tagged_Streams_Pragma Node32
-- Linker_Section_Pragma Node33
- -- SPARK_Aux_Pragma Node33
-- Contract Node34
-- Anonymous_Master Node36
- -- (Class_Wide_Preconds) List38
+ -- Class_Wide_Preconds List38
- -- (Class_Wide_Postconds) List39
+ -- Class_Wide_Postconds List39
- -- (unused) Node40
- -- (unused) Node41
+ -- SPARK_Pragma Node40
+
+ -- SPARK_Aux_Pragma Node41
---------------------------------------------
-- Usage of Flags in Defining Entity Nodes --
pragma Assert
(Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body));
- return Node33 (Id);
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Protected_Type, -- synchronized variants
+ E_Task_Type));
+ return Node41 (Id);
end SPARK_Aux_Pragma;
function SPARK_Aux_Pragma_Inherited (Id : E) return B is
pragma Assert
(Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body));
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Protected_Type, -- synchronized variants
+ E_Task_Type));
return Flag266 (Id);
end SPARK_Aux_Pragma_Inherited;
function SPARK_Pragma (Id : E) return N is
begin
pragma Assert
- (Ekind_In (Id, E_Function, -- subprogram variants
+ (Ekind_In (Id, E_Entry, -- overloadable variants
+ E_Entry_Family,
+ E_Function,
E_Generic_Function,
E_Generic_Procedure,
E_Procedure,
or else
Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body));
- return Node32 (Id);
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Protected_Body, -- synchronized variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type));
+ return Node40 (Id);
end SPARK_Pragma;
function SPARK_Pragma_Inherited (Id : E) return B is
begin
pragma Assert
- (Ekind_In (Id, E_Function, -- subprogram variants
+ (Ekind_In (Id, E_Entry, -- overloadable variants
+ E_Entry_Family,
+ E_Function,
E_Generic_Function,
E_Generic_Procedure,
E_Procedure,
or else
Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body));
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Protected_Body, -- synchronized variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type));
return Flag265 (Id);
end SPARK_Pragma_Inherited;
pragma Assert
(Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body));
-
- Set_Node33 (Id, V);
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Protected_Type, -- synchronized variants
+ E_Task_Type));
+ Set_Node41 (Id, V);
end Set_SPARK_Aux_Pragma;
procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is
pragma Assert
(Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body));
-
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Protected_Type, -- synchronized variants
+ E_Task_Type));
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_Function, -- subprogram variants
+ (Ekind_In (Id, E_Entry, -- overloadable variants
+ E_Entry_Family,
+ E_Function,
E_Generic_Function,
E_Generic_Procedure,
E_Procedure,
or else
Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body));
-
- Set_Node32 (Id, V);
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Protected_Body, -- synchronized variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type));
+ 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_Function, -- subprogram variants
+ (Ekind_In (Id, E_Entry, -- overloadable variants
+ E_Entry_Family,
+ E_Function,
E_Generic_Function,
E_Generic_Procedure,
E_Procedure,
or else
Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body));
-
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Protected_Body, -- synchronized variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type));
Set_Flag265 (Id, V);
end Set_SPARK_Pragma_Inherited;
E_Variable =>
Write_Str ("Encapsulating_State");
- when E_Function |
- E_Generic_Function |
- E_Generic_Package |
- E_Generic_Procedure |
- E_Package |
- E_Package_Body |
- E_Procedure |
- E_Subprogram_Body =>
- Write_Str ("SPARK_Pragma");
-
when Type_Kind =>
Write_Str ("No_Tagged_Streams_Pragma");
procedure Write_Field33_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
- when E_Generic_Package |
- E_Package |
- E_Package_Body =>
- Write_Str ("SPARK_Aux_Pragma");
-
when E_Constant |
E_Variable |
Subprogram_Kind |
procedure Write_Field38_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
- when E_Function | E_Procedure =>
+ when E_Function |
+ E_Procedure =>
Write_Str ("Class-wide preconditions");
when others =>
procedure Write_Field39_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
- when E_Function | E_Procedure =>
+ when E_Function |
+ E_Procedure =>
Write_Str ("Class-wide postcondition");
when others =>
procedure Write_Field40_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Entry |
+ E_Entry_Family |
+ E_Function |
+ E_Generic_Function |
+ E_Generic_Package |
+ E_Generic_Procedure |
+ E_Package |
+ E_Package_Body |
+ E_Procedure |
+ E_Protected_Body |
+ E_Protected_Type |
+ E_Subprogram_Body |
+ E_Task_Body |
+ E_Task_Type =>
+ Write_Str ("SPARK_Pragma");
+
when others =>
Write_Str ("Field40??");
end case;
procedure Write_Field41_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Generic_Package |
+ E_Package |
+ E_Package_Body |
+ E_Protected_Type |
+ E_Task_Type =>
+ Write_Str ("SPARK_Aux_Pragma");
+
when others =>
Write_Str ("Field41??");
end case;
-- Small of the type, either as given in a representation clause, or
-- as computed (as a power of two) by the compiler.
--- SPARK_Aux_Pragma (Node33)
--- Present in package spec and body entities. For a package spec entity
--- it relates to the SPARK mode setting for the private part. This field
--- points to the N_Pragma node that applies to the private part. This is
--- either set with a local SPARK_Mode pragma in the private part or it is
--- inherited from the SPARK mode that applies to the rest of the spec.
--- For a package body, it similarly applies to the SPARK mode setting for
--- the elaboration sequence after the BEGIN. In the case where the pragma
--- is inherited, the SPARK_Aux_Pragma_Inherited flag is set in the
--- package spec or body entity.
+-- 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
+-- 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 the entities of subprogram specs and bodies as well as
--- in package specs and bodies. Set if the SPARK_Aux_Pragma field
--- points to a pragma that is inherited, rather than a local one.
-
--- SPARK_Pragma (Node32)
--- Present in the entities of subprogram specs and bodies as well as in
--- package specs and bodies. 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 [generic] package specs, package bodies and synchronized
+-- types. 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, [generic] package specs, package bodies, [generic]
+-- subprogram specs, 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.
-- SPARK_Pragma_Inherited (Flag265)
--- Present in the entities of subprogram specs and bodies as well as in
--- package specs and bodies. Set if the SPARK_Pragma field points to a
--- pragma that is inherited, rather than a local one.
+-- Present in entries, [generic] package specs, package bodies, [generic]
+-- subprogram specs, subprogram bodies and synchronized types. 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
-- PPC_Wrapper (Node25)
-- Extra_Formals (Node28)
-- Contract (Node34)
+ -- SPARK_Pragma (Node40) (protected kind)
-- Needs_No_Actuals (Flag22)
-- Uses_Sec_Stack (Flag95)
-- Default_Expressions_Processed (Flag108)
-- Entry_Accepted (Flag152)
-- Sec_Stack_Needed_For_Return (Flag167)
-- Has_Expanded_Contract (Flag240)
+ -- SPARK_Pragma_Inherited (Flag265) (protected kind)
-- Address_Clause (synth)
-- Entry_Index_Type (synth)
-- First_Formal (synth)
-- Subprograms_For_Type (Node29)
-- Corresponding_Equality (Node30) (implicit /= only)
-- Thunk_Entity (Node31) (thunk case only)
- -- SPARK_Pragma (Node32)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35) (non-generic case only)
-- Anonymous_Master (Node36) (non-generic case only)
-- Class_Wide_Preconds (List38)
-- Class_Wide_Postconds (List39)
+ -- SPARK_Pragma (Node40)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Default_Expressions_Processed (Flag108)
-- Package_Instantiation (Node26)
-- Current_Use_Clause (Node27)
-- Finalizer (Node28) (non-generic case only)
- -- SPARK_Pragma (Node32)
- -- SPARK_Aux_Pragma (Node33)
-- Contract (Node34)
-- Anonymous_Master (Node36) (non-generic case only)
+ -- SPARK_Pragma (Node40)
+ -- SPARK_Aux_Pragma (Node41)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
-- Finalizer (Node28) (non-generic case only)
- -- SPARK_Pragma (Node32)
- -- SPARK_Aux_Pragma (Node33)
-- Contract (Node34)
-- Anonymous_Master (Node36)
+ -- SPARK_Pragma (Node40)
+ -- SPARK_Aux_Pragma (Node41)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Subprogram_Descriptors (Flag50)
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- Extra_Formals (Node28)
-- Static_Initialization (Node30) (init_proc only)
-- Thunk_Entity (Node31) (thunk case only)
- -- SPARK_Pragma (Node32)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35) (non-generic case only)
-- Anonymous_Master (Node36) (non-generic case only)
-- Class_Wide_Preconds (List38)
-- Class_Wide_Postconds (List39)
+ -- SPARK_Pragma (Node40)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Cleanups (Flag114)
-- Number_Formals (synth)
-- E_Protected_Body
+ -- SPARK_Pragma (Node40)
+ -- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
-- E_Protected_Object
-- Last_Entity (Node20)
-- Discriminant_Constraint (Elist21)
-- Scope_Depth_Value (Uint22)
- -- Scope_Depth (synth)
-- Stored_Constraint (Elist23)
- -- Has_Interrupt_Handler (synth)
+ -- SPARK_Pragma (Node40)
+ -- SPARK_Aux_Pragma (Node41)
-- Sec_Stack_Needed_For_Return (Flag167) ???
+ -- SPARK_Aux_Pragma_Inherited (Flag266)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Uses_Lock_Free (Flag188)
-- Uses_Sec_Stack (Flag95) ???
-- Has_Entries (synth)
+ -- Has_Interrupt_Handler (synth)
-- Number_Entries (synth)
+ -- Scope_Depth (synth)
-- E_Record_Type
-- E_Record_Subtype
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
-- Extra_Formals (Node28)
- -- SPARK_Pragma (Node32)
-- Contract (Node34)
-- Anonymous_Master (Node36)
+ -- SPARK_Pragma (Node40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- SPARK_Pragma_Inherited (Flag265)
-- Scope_Depth (synth)
-- (plus type attributes)
-- E_Task_Body
+ -- SPARK_Pragma (Node40)
+ -- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
-- E_Task_Type
-- Task_Body_Procedure (Node25)
-- Storage_Size_Variable (Node26) (base type only)
-- Relative_Deadline_Variable (Node28) (base type only)
+ -- SPARK_Pragma (Node40)
+ -- SPARK_Aux_Pragma (Node41)
-- Delay_Cleanups (Flag114)
-- Has_Master_Entity (Flag21)
-- Has_Storage_Size_Clause (Flag23) (base type only)
- -- Uses_Sec_Stack (Flag95) ???
-- Sec_Stack_Needed_For_Return (Flag167) ???
+ -- SPARK_Aux_Pragma_Inherited (Flag266)
+ -- SPARK_Pragma_Inherited (Flag265)
+ -- Uses_Sec_Stack (Flag95) ???
-- Has_Entries (synth)
-- Number_Entries (synth)
-- (plus type attributes)
-- Local variables
Loc : constant Source_Ptr := Sloc (Unit_Id);
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Unit_Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Unit_Decl);
Decls : List_Id;
FM_Id : Entity_Id;
Pref : Character;
-- (whether coming from this routine, or directly from source).
if Opt.Suppress_Control_Flow_Optimizations then
- Stmt := Make_Implicit_If_Statement (Cond,
- Condition => Cond,
- Then_Statements => New_List (
- Make_Simple_Return_Statement (Loc,
- New_Occurrence_Of (Standard_True, Loc))),
- Else_Statements => New_List (
- Make_Simple_Return_Statement (Loc,
- New_Occurrence_Of (Standard_False, Loc))));
+ Stmt :=
+ Make_Implicit_If_Statement (Cond,
+ Condition => Cond,
+ Then_Statements => New_List (
+ Make_Simple_Return_Statement (Loc,
+ New_Occurrence_Of (Standard_True, Loc))),
+
+ Else_Statements => New_List (
+ Make_Simple_Return_Statement (Loc,
+ New_Occurrence_Of (Standard_False, Loc))));
else
Stmt := Make_Simple_Return_Statement (Loc, Cond);
begin
Set_Debug_Info_Needed (Def_Id);
- return Make_Function_Specification (Loc,
- Defining_Unit_Name => Def_Id,
- Parameter_Specifications => New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier (Loc, Name_uO),
- Parameter_Type =>
- New_Occurrence_Of (RTE (RE_Address), Loc)),
-
- Make_Parameter_Specification (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier (Loc, Name_uE),
- Parameter_Type =>
- New_Occurrence_Of (RTE (RE_Protected_Entry_Index), Loc))),
-
- Result_Definition => New_Occurrence_Of (Standard_Boolean, Loc));
+ return
+ Make_Function_Specification (Loc,
+ Defining_Unit_Name => Def_Id,
+ Parameter_Specifications => New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier =>
+ Make_Defining_Identifier (Loc, Name_uO),
+ Parameter_Type =>
+ New_Occurrence_Of (RTE (RE_Address), Loc)),
+
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier =>
+ Make_Defining_Identifier (Loc, Name_uE),
+ Parameter_Type =>
+ New_Occurrence_Of (RTE (RE_Protected_Entry_Index), Loc))),
+
+ Result_Definition =>
+ New_Occurrence_Of (Standard_Boolean, Loc));
end Build_Barrier_Function_Specification;
--------------------------
-- version of it because it is never called.
if Expander_Active then
- B_F := Build_Barrier_Function (N, Ent, Prot);
+ B_F := Build_Barrier_Function (N, Ent, Prot);
Func := Barrier_Function (Ent);
Set_Corresponding_Spec (B_F, Func);
-- the specs refer to this type.
procedure Expand_N_Protected_Type_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Prot_Typ : constant Entity_Id := Defining_Identifier (N);
+ Discr_Map : constant Elist_Id := New_Elmt_List;
+ Loc : constant Source_Ptr := Sloc (N);
+ Prot_Typ : constant Entity_Id := Defining_Identifier (N);
Lock_Free_Active : constant Boolean := Uses_Lock_Free (Prot_Typ);
-- This flag indicates whether the lock free implementation is active
Pdef : constant Node_Id := Protected_Definition (N);
-- This contains two lists; one for visible and one for private decls
- Rec_Decl : Node_Id;
+ Body_Arr : Node_Id;
+ Body_Id : Entity_Id;
Cdecls : List_Id;
- Discr_Map : constant Elist_Id := New_Elmt_List;
- Priv : Node_Id;
- New_Priv : Node_Id;
Comp : Node_Id;
Comp_Id : Entity_Id;
- Sub : Node_Id;
Current_Node : Node_Id := N;
- Entries_Aggr : Node_Id;
- Body_Id : Entity_Id;
- Body_Arr : Node_Id;
E_Count : Int;
+ Entries_Aggr : Node_Id;
+ New_Priv : Node_Id;
Object_Comp : Node_Id;
+ Priv : Node_Id;
+ Rec_Decl : Node_Id;
+ Sub : Node_Id;
procedure Check_Inlining (Subp : Entity_Id);
-- If the original operation has a pragma Inline, propagate the flag
Make_Subprogram_Declaration (Loc,
Specification =>
Build_Barrier_Function_Specification (Loc, Bdef));
+ Set_Is_Entry_Barrier_Function (Sub);
Insert_After (Current_Node, Sub);
Analyze (Sub);
elsif Restriction_Active (No_Implicit_Heap_Allocations) then
if not Discriminated_Size (Defining_Identifier (Priv))
then
-
-- Any object of the type will be non-static.
Error_Msg_N ("component has non-static size??", Priv);
Error_Msg_NE
- ("\creation of protected object of type& will"
- & " violate restriction "
+ ("\creation of protected object of type& will "
+ & "violate restriction "
& "No_Implicit_Heap_Allocations??", Priv, Prot_Typ);
else
then
if not Discriminated_Size (Defining_Identifier (Priv))
then
-
-- Any object of the type will be non-static.
Error_Msg_N ("component has non-static size??", Priv);
Error_Msg_NE
- ("\creation of protected object of type& will"
- & " violate restriction "
+ ("\creation of protected object of type& will "
+ & "violate restriction "
& "No_Implicit_Protected_Object_Allocations??",
Priv, Prot_Typ);
else
-
-- Object will be non-static if discriminants are.
Error_Msg_NE
("creation of protected object of type& with "
- & "non-static discriminants will violate "
- & " restriction"
- & " No_Implicit_Protected_Object_Allocations??",
+ & "non-static discriminants will violate "
+ & "restriction "
+ & "No_Implicit_Protected_Object_Allocations??",
Priv, Prot_Typ);
end if;
end if;
declare
Old_Comp : constant Node_Id := Component_Definition (Priv);
Oent : constant Entity_Id := Defining_Identifier (Priv);
- New_Comp : Node_Id;
Nent : constant Entity_Id :=
Make_Defining_Identifier (Sloc (Oent),
Chars => Chars (Oent));
+ New_Comp : Node_Id;
begin
if Present (Subtype_Indication (Old_Comp)) then
Make_Component_Definition (Sloc (Oent),
Aliased_Present => False,
Subtype_Indication =>
- New_Copy_Tree (Subtype_Indication (Old_Comp),
- Discr_Map));
+ New_Copy_Tree
+ (Subtype_Indication (Old_Comp), Discr_Map));
else
New_Comp :=
Make_Component_Definition (Sloc (Oent),
Aliased_Present => False,
Access_Definition =>
- New_Copy_Tree (Access_Definition (Old_Comp),
- Discr_Map));
+ New_Copy_Tree
+ (Access_Definition (Old_Comp), Discr_Map));
end if;
New_Priv :=
if not Lock_Free_Active then
declare
- Ritem : Node_Id;
- Num_Attach_Handler : Int := 0;
- Protection_Subtype : Node_Id;
Entry_Count_Expr : constant Node_Id :=
Build_Entry_Count_Expression
(Prot_Typ, Cdecls, Loc);
+ Num_Attach_Handler : Int := 0;
+ Protection_Subtype : Node_Id;
+ Ritem : Node_Id;
begin
if Has_Attach_Handler (Prot_Typ) then
end if;
elsif Nkind (Comp) = N_Entry_Declaration then
-
Expand_Entry_Declaration (Comp);
-
end if;
Next (Comp);
case Corresponding_Runtime_Package (Prot_Typ) is
when System_Tasking_Protected_Objects_Entries =>
- Body_Arr := Make_Object_Declaration (Loc,
- Defining_Identifier => Body_Id,
- Aliased_Present => True,
- Object_Definition =>
- Make_Subtype_Indication (Loc,
- Subtype_Mark => New_Occurrence_Of (
- RTE (RE_Protected_Entry_Body_Array), Loc),
- Constraint =>
- Make_Index_Or_Discriminant_Constraint (Loc,
- Constraints => New_List (
- Make_Range (Loc,
- Make_Integer_Literal (Loc, 1),
- Make_Integer_Literal (Loc, E_Count))))),
- Expression => Entries_Aggr);
+ Body_Arr :=
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Body_Id,
+ Aliased_Present => True,
+ Object_Definition =>
+ Make_Subtype_Indication (Loc,
+ Subtype_Mark =>
+ New_Occurrence_Of
+ (RTE (RE_Protected_Entry_Body_Array), Loc),
+ Constraint =>
+ Make_Index_Or_Discriminant_Constraint (Loc,
+ Constraints => New_List (
+ Make_Range (Loc,
+ Make_Integer_Literal (Loc, 1),
+ Make_Integer_Literal (Loc, E_Count))))),
+ Expression => Entries_Aggr);
when System_Tasking_Protected_Objects_Single_Entry =>
- Body_Arr := Make_Object_Declaration (Loc,
- Defining_Identifier => Body_Id,
- Aliased_Present => True,
- Object_Definition => New_Occurrence_Of
- (RTE (RE_Entry_Body), Loc),
- Expression => Remove_Head (Expressions (Entries_Aggr)));
+ Body_Arr :=
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Body_Id,
+ Aliased_Present => True,
+ Object_Definition =>
+ New_Occurrence_Of (RTE (RE_Entry_Body), Loc),
+ Expression => Remove_Head (Expressions (Entries_Aggr)));
when others =>
raise Program_Error;
Specification => Build_Task_Proc_Specification (Ttyp),
Declarations => Declarations (N),
Handled_Statement_Sequence => Handled_Statement_Sequence (N));
+ Set_Is_Task_Body_Procedure (New_N);
-- If the task contains generic instantiations, cleanup actions are
-- delayed until after instantiation. Transfer the activation chain to
Body_Decl :=
Make_Subprogram_Declaration (Loc,
Specification => Proc_Spec);
+ Set_Is_Task_Body_Procedure (Body_Decl);
Insert_After (Rec_Decl, Body_Decl);
-- of no corresponding body being available is ignored for now.
elsif Nkind (N) = N_Subprogram_Body then
- Ent := Corresponding_Spec_Of (N);
+ Ent := Unique_Defining_Entity (N);
-- Ignore generic subprogram
-- If we get here, then the attribute is legal
Legal := True;
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
end Analyze_Attribute_Old_Result;
---------------------------------
-- Number_Components --
-----------------------
- function Number_Components (Typ : Entity_Id) return Pos is
+ function Number_Components (Typ : Entity_Id) return Nat is
N : Int;
Comp : Entity_Id;
-- The result returned is the next _Tag field in this record, or Empty
-- if this is the last such field.
- function Number_Components (Typ : Entity_Id) return Pos;
+ function Number_Components (Typ : Entity_Id) return Nat;
-- Typ is a record type, yields number of components (including
-- discriminants) in type.
Error_Msg_N ("missing specification for Protected body", N);
else
- -- Currently there are no language-defined aspects that can apply to
- -- a protected body stub. Issue an error and remove the aspects to
- -- prevent cascaded errors.
-
- if Has_Aspects (N) then
- Error_Msg_N
- ("aspects on protected bodies are not allowed",
- First (Aspect_Specifications (N)));
- Remove_Aspects (N);
- end if;
-
Set_Scope (Defining_Entity (N), Current_Scope);
Set_Has_Completion (Etype (Nam));
Set_Corresponding_Spec_Of_Stub (N, Nam);
Error_Msg_N ("missing specification for task body", N);
else
- -- Currently there are no language-defined aspects that can apply to
- -- a task body stub. Issue an error and remove the aspects to prevent
- -- cascaded errors.
-
- if Has_Aspects (N) then
- Error_Msg_N
- ("aspects on task bodies are not allowed",
- First (Aspect_Specifications (N)));
- Remove_Aspects (N);
- end if;
-
Set_Scope (Defining_Entity (N), Current_Scope);
Generate_Reference (Nam, Defining_Identifier (N), 'b');
Set_Corresponding_Spec_Of_Stub (N, Nam);
if Expander_Active then
Insert_After (N,
Make_Assignment_Statement (Loc,
- Name =>
+ Name =>
Make_Identifier (Loc,
Chars => New_External_Name (Chars (Etype (Nam)), 'E')),
Expression => New_Occurrence_Of (Standard_True, Loc)));
(Prag : Node_Id;
Ins_Nod : Node_Id;
Decls : List_Id);
- -- Subsidiary to the analysis of aspects Abstract_State, Ghost,
- -- Initializes, Initial_Condition and Refined_State. Insert node Prag
- -- before node Ins_Nod. If Ins_Nod is for pragma SPARK_Mode, then skip
- -- SPARK_Mode. Decls is the associated declarative list where Prag is to
- -- reside.
+ -- Subsidiary to the analysis of aspects
+ -- Abstract_State
+ -- Ghost
+ -- Initializes
+ -- Initial_Condition
+ -- Refined_State
+ -- Insert node Prag before node Ins_Nod. If Ins_Nod is for pragma
+ -- SPARK_Mode, then skip SPARK_Mode. Decls is the associated declarative
+ -- list where Prag is to reside.
procedure Insert_Pragma (Prag : Node_Id);
- -- Subsidiary to the analysis of aspects Attach_Handler, Contract_Cases,
- -- Depends, Global, Post, Pre, Refined_Depends and Refined_Global.
+ -- Subsidiary to the analysis of aspects
+ -- Attach_Handler
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Post
+ -- Pre
+ -- Refined_Depends
+ -- Refined_Global
+ -- SPARK_Mode
+ -- Warnings
-- Insert pragma Prag such that it mimics the placement of a source
-- pragma of the same kind.
--
-------------------
procedure Insert_Pragma (Prag : Node_Id) is
- Aux : Node_Id;
- Decl : Node_Id;
+ Aux : Node_Id;
+ Decl : Node_Id;
+ Decls : List_Id;
begin
- if Nkind (N) = N_Subprogram_Body then
- if Present (Declarations (N)) then
-
- -- Skip other internally generated pragmas from aspects to find
- -- the proper insertion point. As a result the order of pragmas
- -- is the same as the order of aspects.
-
- -- As precondition pragmas generated from conjuncts in the
- -- precondition aspect are presented in reverse order to
- -- Insert_Pragma, insert them in the correct order here by not
- -- skipping previously inserted precondition pragmas when the
- -- current pragma is a precondition.
-
- Decl := First (Declarations (N));
- while Present (Decl) loop
- if Nkind (Decl) = N_Pragma
- and then From_Aspect_Specification (Decl)
- and then not (Get_Pragma_Id (Decl) = Pragma_Precondition
- and then
- Get_Pragma_Id (Prag) = Pragma_Precondition)
- then
- Next (Decl);
- else
- exit;
- end if;
- end loop;
+ -- When the aspect appears on a package, protected unit, subprogram
+ -- or task unit body, insert the generated pragma at the top of the
+ -- body declarations to emulate the behavior of a source pragma.
+
+ -- package body Pack with Aspect is
- if Present (Decl) then
- Insert_Before (Decl, Prag);
+ -- package body Pack is
+ -- pragma Prag;
+
+ if Nkind_In (N, N_Package_Body,
+ N_Protected_Body,
+ N_Subprogram_Body,
+ N_Task_Body)
+ then
+ Decls := Declarations (N);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (N, Decls);
+ end if;
+
+ -- Skip other internally generated pragmas from aspects to find
+ -- the proper insertion point. As a result the order of pragmas
+ -- is the same as the order of aspects.
+
+ -- As precondition pragmas generated from conjuncts in the
+ -- precondition aspect are presented in reverse order to
+ -- Insert_Pragma, insert them in the correct order here by not
+ -- skipping previously inserted precondition pragmas when the
+ -- current pragma is a precondition.
+
+ Decl := First (Decls);
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Pragma
+ and then From_Aspect_Specification (Decl)
+ and then not (Get_Pragma_Id (Decl) = Pragma_Precondition
+ and then
+ Get_Pragma_Id (Prag) = Pragma_Precondition)
+ then
+ Next (Decl);
else
- Append (Prag, Declarations (N));
+ exit;
end if;
+ end loop;
+
+ if Present (Decl) then
+ Insert_Before (Decl, Prag);
else
- Set_Declarations (N, New_List (Prag));
+ Append_To (Decls, Prag);
+ end if;
+
+ -- When the aspect is associated with a [generic] package declaration
+ -- insert the generated pragma at the top of the visible declarations
+ -- to emulate the behavior of a source pragma.
+
+ -- package Pack with Aspect is
+
+ -- package Pack is
+ -- pragma Prag;
+
+ elsif Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Decls := Visible_Declarations (Specification (N));
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Visible_Declarations (Specification (N), Decls);
+ end if;
+
+ Prepend_To (Decls, Prag);
+
+ -- When the aspect is associated with a protected unit declaration,
+ -- insert the generated pragma at the top of the visible declarations
+ -- the emulate the behavior of a source pragma.
+
+ -- protected [type] Prot with Aspect is
+
+ -- protected [type] Prot is
+ -- pragma Prag;
+
+ elsif Nkind (N) = N_Protected_Type_Declaration then
+ Decls := Visible_Declarations (Protected_Definition (N));
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Visible_Declarations (Protected_Definition (N), 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.
+
+ -- 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));
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Visible_Declarations (Task_Definition (N), Decls);
+ end if;
+
+ Prepend_To (Decls, Prag);
+
-- When the context is a library unit, the pragma is added to the
-- Pragmas_After list.
Prepend (Prag, Pragmas_After (Aux));
- -- Default
+ -- Default, the pragma is inserted after the context
else
Insert_After (N, Prag);
goto Continue;
- -- For tasks
+ -- For tasks pass the aspect as an attribute
else
- -- Pass the aspect as an attribute
-
Aitem :=
Make_Attribute_Definition_Clause (Loc,
Name => Ent,
Expression => New_Occurrence_Of (E, Loc))),
Pragma_Name => Chars (Id));
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
-- Case 2c: Aspects corresponding to pragmas with three
-- arguments.
-- SPARK_Mode
- when Aspect_SPARK_Mode => SPARK_Mode : declare
- Decls : List_Id;
-
- begin
+ when Aspect_SPARK_Mode =>
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_SPARK_Mode);
- -- When the aspect appears on a package or a subprogram
- -- body, insert the generated pragma at the top of the body
- -- declarations to emulate the behavior of a source pragma.
-
- if Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
- Decorate (Aspect, Aitem);
-
- Decls := Declarations (N);
-
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (N, Decls);
- end if;
-
- Prepend_To (Decls, Aitem);
- goto Continue;
-
- -- When the aspect is associated with a [generic] package
- -- declaration, insert the generated pragma at the top of
- -- the visible declarations to emulate the behavior of a
- -- source pragma.
-
- elsif Nkind_In (N, N_Generic_Package_Declaration,
- N_Package_Declaration)
- then
- Decorate (Aspect, Aitem);
-
- Decls := Visible_Declarations (Specification (N));
-
- if No (Decls) then
- Decls := New_List;
- Set_Visible_Declarations (Specification (N), Decls);
- end if;
-
- Prepend_To (Decls, Aitem);
- goto Continue;
- end if;
- end SPARK_Mode;
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
-- Refined_Depends
Subp_Decl :=
Make_Subprogram_Declaration (Loc,
Specification => Copy_Subprogram_Spec (Body_Spec));
+ Set_Comes_From_Source (Subp_Decl, True);
-- Relocate the aspects of the subprogram body to the new subprogram
-- spec because it acts as the initial declaration.
Generate_Reference_To_Formals (Body_Id);
end if;
- -- Set SPARK_Mode from context
+ -- Set the SPARK_Mode from the current context (may be overwritten later
+ -- with explicit pragma). This is not done for entry barrier functions
+ -- because they are generated outside the protected type and should not
+ -- carry the mode of the enclosing context.
- Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Body_Id);
+ if Nkind (N) = N_Subprogram_Body
+ and then Is_Entry_Barrier_Function (N)
+ then
+ null;
+ else
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id);
+ end if;
-- If the return type is an anonymous access type whose designated type
-- is the limited view of a class-wide type and the non-limited view is
Generate_Definition (Designator);
- -- Set SPARK mode from current context (may be overwritten later with
- -- explicit pragma).
+ -- Set the SPARK mode from the current context (may be overwritten later
+ -- with explicit pragma). This is not done for entry barrier functions
+ -- because they are generated outside the protected type and should not
+ -- carry the mode of the enclosing context.
- Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Designator);
+ if Nkind (N) = N_Subprogram_Declaration
+ and then Is_Entry_Barrier_Function (N)
+ then
+ null;
+ else
+ Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Designator);
+ end if;
-- A subprogram declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
-- Set SPARK_Mode only for non-generic package
if Ekind (Spec_Id) = E_Package then
-
- -- Set SPARK_Mode from context
-
- Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Body_Id);
-
- -- Set elaboration code SPARK mode the same for now
-
- Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id);
Set_SPARK_Aux_Pragma_Inherited (Body_Id);
end if;
-- --
------------------------------------------------------------------------------
-with Aspects; use Aspects;
-with Atree; use Atree;
-with Checks; use Checks;
-with Debug; use Debug;
-with Einfo; use Einfo;
-with Errout; use Errout;
-with Exp_Ch9; use Exp_Ch9;
-with Elists; use Elists;
-with Freeze; use Freeze;
-with Layout; use Layout;
-with Lib.Xref; use Lib.Xref;
-with Namet; use Namet;
-with Nlists; use Nlists;
-with Nmake; use Nmake;
-with Opt; use Opt;
-with Restrict; use Restrict;
-with Rident; use Rident;
-with Rtsfind; use Rtsfind;
-with Sem; use Sem;
-with Sem_Aux; use Sem_Aux;
-with Sem_Ch3; use Sem_Ch3;
-with Sem_Ch5; use Sem_Ch5;
-with Sem_Ch6; use Sem_Ch6;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Eval; use Sem_Eval;
-with Sem_Res; use Sem_Res;
-with Sem_Type; use Sem_Type;
-with Sem_Util; use Sem_Util;
-with Sem_Warn; use Sem_Warn;
-with Snames; use Snames;
-with Stand; use Stand;
-with Sinfo; use Sinfo;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Checks; use Checks;
+with Contracts; use Contracts;
+with Debug; use Debug;
+with Einfo; use Einfo;
+with Errout; use Errout;
+with Exp_Ch9; use Exp_Ch9;
+with Elists; use Elists;
+with Freeze; use Freeze;
+with Layout; use Layout;
+with Lib.Xref; use Lib.Xref;
+with Namet; use Namet;
+with Nlists; use Nlists;
+with Nmake; use Nmake;
+with Opt; use Opt;
+with Restrict; use Restrict;
+with Rident; use Rident;
+with Rtsfind; use Rtsfind;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Ch3; use Sem_Ch3;
+with Sem_Ch5; use Sem_Ch5;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch13; use Sem_Ch13;
+with Sem_Eval; use Sem_Eval;
+with Sem_Res; use Sem_Res;
+with Sem_Type; use Sem_Type;
+with Sem_Util; use Sem_Util;
+with Sem_Warn; use Sem_Warn;
+with Snames; use Snames;
+with Stand; use Stand;
+with Sinfo; use Sinfo;
with Style;
-with Tbuild; use Tbuild;
-with Uintp; use Uintp;
+with Tbuild; use Tbuild;
+with Uintp; use Uintp;
package body Sem_Ch9 is
Entry_Name : Entity_Id;
begin
+ -- An entry body "freezes" the contract of the nearest enclosing
+ -- package body. This ensures that any annotations referenced by the
+ -- contract of an entry or subprogram body declared within the current
+ -- protected body are available.
+
+ Analyze_Enclosing_Package_Body_Contract (N);
+
Tasking_Used := True;
-- Entry_Name is initialized to Any_Id. It should get reset to the
Set_Etype (Id, Standard_Void_Type);
Set_Accept_Address (Id, New_Elmt_List);
+ -- Set the SPARK_Mode from the current context (may be overwritten later
+ -- with an explicit pragma).
+
+ Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Id);
+
E := First_Entity (P_Type);
while Present (E) loop
if Chars (E) = Chars (Id)
then
Entry_Name := E;
Set_Convention (Id, Convention (E));
- Set_Corresponding_Body (Parent (Entry_Name), Id);
+ Set_Corresponding_Body (Parent (E), Id);
Check_Fully_Conformant (Id, E, N);
if Ekind (Id) = E_Entry_Family then
Set_Convention (Def_Id, Convention_Entry);
Set_Accept_Address (Def_Id, New_Elmt_List);
+ -- Set the SPARK_Mode from the current context (may be overwritten later
+ -- with an explicit pragma). Task entries are excluded because they are
+ -- not completed by entry bodies.
+
+ if Ekind (Current_Scope) = E_Protected_Type then
+ Set_SPARK_Pragma (Def_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Def_Id);
+ end if;
+
-- Process formals
if Present (Formals) then
-- Start of processing for Analyze_Protected_Body
begin
+ -- A protected body "freezes" the contract of the nearest enclosing
+ -- package body. This ensures that any annotations referenced by the
+ -- contract of an entry or subprogram body declared within the current
+ -- protected body are available.
+
+ Analyze_Enclosing_Package_Body_Contract (N);
+
Tasking_Used := True;
Set_Ekind (Body_Id, E_Protected_Body);
+ Set_Etype (Body_Id, Standard_Void_Type);
Spec_Id := Find_Concurrent_Spec (Body_Id);
- -- Protected bodies are currently removed by the expander. Since there
- -- are no language-defined aspects that apply to a protected body, it is
- -- not worth changing the whole expansion to accomodate implementation-
- -- defined aspects. Plus we cannot possibly known the semantics of such
- -- future implementation-defined aspects in order to plan ahead.
-
- if Has_Aspects (N) then
- Error_Msg_N
- ("aspects on protected bodies are not allowed",
- First (Aspect_Specifications (N)));
-
- -- Remove illegal aspects to prevent cascaded errors later on
-
- Remove_Aspects (N);
- end if;
-
- if Present (Spec_Id)
- and then Ekind (Spec_Id) = E_Protected_Type
- then
+ if Present (Spec_Id) and then Ekind (Spec_Id) = E_Protected_Type then
null;
elsif Present (Spec_Id)
Spec_Id := Etype (Spec_Id);
end if;
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Body_Id);
+ end if;
+
Push_Scope (Spec_Id);
Set_Corresponding_Spec (N, Spec_Id);
Set_Corresponding_Body (Parent (Spec_Id), Body_Id);
Set_Etype (T, T);
Set_Has_Delayed_Freeze (T, True);
Set_Stored_Constraint (T, No_Elist);
+
+ -- Set the SPARK_Mode from the current context (may be overwritten later
+ -- with an explicit pragma).
+
+ Set_SPARK_Pragma (T, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (T, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (T);
+ Set_SPARK_Aux_Pragma_Inherited (T);
+
Push_Scope (T);
if Ada_Version >= Ada_2005 then
-- a single task, since Spec_Id is set to the task type).
begin
+ -- A task body "freezes" the contract of the nearest enclosing package
+ -- body. This ensures that any annotations referenced by the contract
+ -- of an entry or subprogram body declared within the current protected
+ -- body are available.
+
+ Analyze_Enclosing_Package_Body_Contract (N);
+
Tasking_Used := True;
- Set_Ekind (Body_Id, E_Task_Body);
Set_Scope (Body_Id, Current_Scope);
+ Set_Ekind (Body_Id, E_Task_Body);
+ Set_Etype (Body_Id, Standard_Void_Type);
Spec_Id := Find_Concurrent_Spec (Body_Id);
- -- Task bodies are transformed into a subprogram spec and body pair by
- -- the expander. Since there are no language-defined aspects that apply
- -- to a task body, it is not worth changing the whole expansion to
- -- accomodate implementation-defined aspects. Plus we cannot possibly
- -- know semantics of such aspects in order to plan ahead.
-
- if Has_Aspects (N) then
- Error_Msg_N
- ("aspects on task bodies are not allowed",
- First (Aspect_Specifications (N)));
-
- -- Remove illegal aspects to prevent cascaded errors later on
-
- Remove_Aspects (N);
- end if;
-
-- The spec is either a task type declaration, or a single task
-- declaration for which we have created an anonymous type.
- if Present (Spec_Id)
- and then Ekind (Spec_Id) = E_Task_Type
- then
+ if Present (Spec_Id) and then Ekind (Spec_Id) = E_Task_Type then
null;
elsif Present (Spec_Id)
Spec_Id := Etype (Spec_Id);
end if;
+ -- Set the SPARK_Mode from the current context (may be overwritten later
+ -- with an explicit pragma).
+
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id);
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Body_Id);
+ end if;
+
Push_Scope (Spec_Id);
Set_Corresponding_Spec (N, Spec_Id);
Set_Corresponding_Body (Parent (Spec_Id), Body_Id);
Set_Etype (T, T);
Set_Has_Delayed_Freeze (T, True);
Set_Stored_Constraint (T, No_Elist);
+
+ -- Set the SPARK_Mode from the current context (may be overwritten later
+ -- with an explicit pragma).
+
+ Set_SPARK_Pragma (T, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (T, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (T);
+ Set_SPARK_Aux_Pragma_Inherited (T);
+
Push_Scope (T);
if Ada_Version >= Ada_2005 then
-- Local variables
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
All_Inputs_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all the inputs processed so far.
procedure Analyze_Global_In_Decl_Part (N : Node_Id) is
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl);
Constits_Seen : Elist_Id := No_Elist;
return;
end if;
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
return;
end if;
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
return;
end if;
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
-- Mark the pragma as Ghost if the related subprogram is also
-- Ghost. This also ensures that any expansion performed further
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
- Context := Parent (N);
-
- -- Handle compilation units
-
- if Nkind (Context) = N_Compilation_Unit_Aux then
- Context := Unit (Parent (Context));
- end if;
-
Id := Empty;
Stmt := Prev (N);
while Present (Stmt) loop
Error_Msg_N ("pragma % duplicates pragma declared#", N);
end if;
- -- Protected and task types cannot be subject to pragma Ghost
- -- (SPARK RM 6.9(19)).
+ -- Task unit declared without a definition cannot be subject to
+ -- pragma Ghost (SPARK RM 6.9(19)).
- elsif Nkind (Stmt) = N_Protected_Type_Declaration then
- Error_Pragma ("pragma % cannot apply to a protected type");
- return;
-
- elsif Nkind (Stmt) = N_Task_Type_Declaration then
+ elsif Nkind_In (Stmt, N_Single_Task_Declaration,
+ N_Task_Type_Declaration)
+ then
Error_Pragma ("pragma % cannot apply to a task type");
return;
Stmt := Prev (Stmt);
end loop;
+ Context := Parent (N);
+
+ -- Handle compilation units
+
+ if Nkind (Context) = N_Compilation_Unit_Aux then
+ Context := Unit (Parent (Context));
+ end if;
+
+ -- Protected and task types cannot be subject to pragma Ghost
+ -- (SPARK RM 6.9(19)).
+
+ if Nkind_In (Context, N_Protected_Body, N_Protected_Definition)
+ then
+ Error_Pragma ("pragma % cannot apply to a protected type");
+ return;
+
+ elsif Nkind_In (Context, N_Task_Body, N_Task_Definition) then
+ Error_Pragma ("pragma % cannot apply to a task type");
+ return;
+ end if;
+
if No (Id) then
-- When pragma Ghost is associated with a [generic] package, it
procedure Check_Pragma_Conformance
(Context_Pragma : Node_Id;
- Entity_Pragma : Node_Id;
- Entity : Entity_Id);
- -- If Context_Pragma is not Empty, verify that the new pragma N
- -- is compatible with the pragma Context_Pragma that was inherited
+ Entity : Entity_Id;
+ Entity_Pragma : Node_Id);
+ -- Subsidiary to routines Process_xxx. Verify the SPARK_Mode
+ -- conformance of pragma N depending the following scenarios:
+ --
+ -- If pragma Context_Pragma is not Empty, verify that pragma N is
+ -- compatible with the pragma Context_Pragma that was inherited
-- from the context:
- -- . if Context_Pragma is ON, then the new mode can be anything
- -- . if Context_Pragma is OFF, then the only allowed new mode is
- -- also OFF.
+ -- * If the mode of Context_Pragma is ON, then the new mode can
+ -- be anything.
+ -- * If the mode of Context_Pragma is OFF, then the only allowed
+ -- new mode is also OFF. Emit error if this is not the case.
--
- -- If Entity is not Empty, verify that the new pragma N is
- -- compatible with Entity_Pragma, the SPARK_Mode previously set
- -- for Entity (which may be Empty):
- -- . if Entity_Pragma is ON, then the new mode can be anything
- -- . if Entity_Pragma is OFF, then the only allowed new mode is
- -- also OFF.
- -- . if Entity_Pragma is Empty, we always issue an error, as this
- -- corresponds to a case where a previous section of Entity
- -- had no SPARK_Mode set.
+ -- If Entity is not Empty, verify that pragma N is compatible with
+ -- pragma Entity_Pragma that belongs to Entity.
+ -- * If Entity_Pragma is Empty, always issue an error as this
+ -- corresponds to the case where a previous section of Entity
+ -- has no SPARK_Mode set.
+ -- * If the mode of Entity_Pragma is ON, then the new mode can
+ -- be anything.
+ -- * If the mode of Entity_Pragma is OFF, then the only allowed
+ -- new mode is also OFF. Emit error if this is not the case.
procedure Check_Library_Level_Entity (E : Entity_Id);
- -- Verify that pragma is applied to library-level entity E
-
- procedure Set_SPARK_Flags;
- -- Sets SPARK_Mode from Mode_Id and SPARK_Mode_Pragma from N,
- -- and ensures that Dynamic_Elaboration_Checks are off if the
- -- call sets SPARK_Mode On.
+ -- Subsidiary to routines Process_xxx. Verify that the related
+ -- entity E subject to pragma SPARK_Mode is library-level.
+
+ procedure Process_Body (Decl : Node_Id);
+ -- Verify the legality of pragma SPARK_Mode when it appears as the
+ -- top of the body declarations of entry, package, protected unit,
+ -- subprogram or task unit body denoted by Decl.
+
+ procedure Process_Overloadable (Decl : Node_Id);
+ -- Verify the legality of pragma SPARK_Mode when it applies to an
+ -- entry or [generic] subprogram declaration denoted by Decl.
+
+ procedure Process_Private_Part (Decl : Node_Id);
+ -- Verify the legality of pragma SPARK_Mode when it appears at the
+ -- top of the private declarations of a package spec, protected or
+ -- task unit declaration denoted by Decl.
+
+ procedure Process_Statement_Part (Decl : Node_Id);
+ -- Verify the legality of pragma SPARK_Mode when it appears at the
+ -- top of the statement sequence of a package body denoted by node
+ -- Decl.
+
+ procedure Process_Visible_Part (Decl : Node_Id);
+ -- Verify the legality of pragma SPARK_Mode when it appears at the
+ -- top of the visible declarations of a package spec, protected or
+ -- task unit declaration denoted by Decl. The routine is also used
+ -- on protected or task units declared without a definition.
+
+ procedure Set_SPARK_Context;
+ -- Subsidiary to routines Process_xxx. Set the global variables
+ -- which represent the mode of the context from pragma N. Ensure
+ -- that Dynamic_Elaboration_Checks are off if the new mode is On.
------------------------------
-- Check_Pragma_Conformance --
procedure Check_Pragma_Conformance
(Context_Pragma : Node_Id;
- Entity_Pragma : Node_Id;
- Entity : Entity_Id)
+ Entity : Entity_Id;
+ Entity_Pragma : Node_Id)
is
- Arg : Node_Id := Arg1;
+ Err_Id : Entity_Id;
+ Err_N : Node_Id;
begin
-- The current pragma may appear without an argument. If this
-- is the case, associate all error messages with the pragma
-- itself.
- if No (Arg) then
- Arg := N;
+ if Present (Arg1) then
+ Err_N := Arg1;
+ else
+ Err_N := N;
end if;
-- The mode of the current pragma is compared against that of
and then Get_SPARK_Mode_From_Pragma (N) = On
then
Error_Msg_N
- ("cannot change SPARK_Mode from Off to On", Arg);
+ ("cannot change SPARK_Mode from Off to On", Err_N);
Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
- Error_Msg_N ("\SPARK_Mode was set to Off#", Arg);
+ Error_Msg_N ("\SPARK_Mode was set to Off#", Err_N);
raise Pragma_Exit;
end if;
end if;
-- The mode of the current pragma is compared against that of
- -- an initial package/subprogram declaration.
+ -- an initial package, protected type, subprogram or task type
+ -- declaration.
if Present (Entity) then
+ -- A simple protected or task type is transformed into an
+ -- anonymous type whose name cannot be used to issue error
+ -- messages. Recover the original entity of the type.
+
+ if Ekind_In (Entity, E_Protected_Type, E_Task_Type) then
+ Err_Id :=
+ Defining_Entity
+ (Original_Node (Unit_Declaration_Node (Entity)));
+ else
+ Err_Id := Entity;
+ end if;
+
-- Both the initial declaration and the completion carry
-- SPARK_Mode pragmas.
if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
and then Get_SPARK_Mode_From_Pragma (N) = On
then
- Error_Msg_N ("incorrect use of SPARK_Mode", Arg);
+ Error_Msg_N ("incorrect use of SPARK_Mode", Err_N);
Error_Msg_Sloc := Sloc (Entity_Pragma);
Error_Msg_NE
("\value Off was set for SPARK_Mode on&#",
- Arg, Entity);
+ Err_N, Err_Id);
raise Pragma_Exit;
end if;
-- it cannot "complete".
else
- Error_Msg_N ("incorrect use of SPARK_Mode", Arg);
- Error_Msg_Sloc := Sloc (Entity);
+ Error_Msg_N ("incorrect use of SPARK_Mode", Err_N);
+ Error_Msg_Sloc := Sloc (Err_Id);
Error_Msg_NE
("\no value was set for SPARK_Mode on&#",
- Arg, Entity);
+ Err_N, Err_Id);
raise Pragma_Exit;
end if;
end if;
--------------------------------
procedure Check_Library_Level_Entity (E : Entity_Id) is
- MsgF : constant String := "incorrect placement of pragma%";
+ procedure Add_Entity_To_Name_Buffer;
+ -- Add the E_Kind of entity E to the name buffer
- begin
- if not Is_Library_Level_Entity (E) then
- Error_Msg_Name_1 := Pname;
- Error_Msg_N (Fix_Error (MsgF), N);
+ -------------------------------
+ -- Add_Entity_To_Name_Buffer --
+ -------------------------------
- if Ekind_In (E, E_Generic_Package,
- E_Package,
- E_Package_Body)
+ procedure Add_Entity_To_Name_Buffer is
+ begin
+ if Ekind_In (E, E_Entry, E_Entry_Family) then
+ Add_Str_To_Name_Buffer ("entry");
+
+ elsif Ekind_In (E, E_Generic_Package,
+ E_Package,
+ E_Package_Body)
then
- Error_Msg_NE
- ("\& is not a library-level package", N, E);
+ Add_Str_To_Name_Buffer ("package");
+
+ elsif Ekind_In (E, E_Protected_Body, E_Protected_Type) then
+ Add_Str_To_Name_Buffer ("protected unit");
+
+ elsif Ekind_In (E, E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Procedure,
+ E_Subprogram_Body)
+ then
+ Add_Str_To_Name_Buffer ("subprogram");
+
else
- Error_Msg_NE
- ("\& is not a library-level subprogram", N, E);
+ pragma Assert (Ekind_In (E, E_Task_Body, E_Task_Type));
+ Add_Str_To_Name_Buffer ("task unit");
end if;
+ end Add_Entity_To_Name_Buffer;
+
+ -- Local variables
+
+ Msg_1 : constant String := "incorrect placement of pragma%";
+ Msg_2 : Name_Id;
+
+ -- Start of processing for Check_Library_Level_Entity
+
+ begin
+ if not Is_Library_Level_Entity (E) then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N (Fix_Error (Msg_1), N);
+
+ Name_Len := 0;
+ Add_Str_To_Name_Buffer ("\& is not a library-level ");
+ Add_Entity_To_Name_Buffer;
+
+ Msg_2 := Name_Find;
+ Error_Msg_NE (Get_Name_String (Msg_2), N, E);
raise Pragma_Exit;
end if;
end Check_Library_Level_Entity;
- ---------------------
- -- Set_SPARK_Flags --
- ---------------------
+ ------------------
+ -- Process_Body --
+ ------------------
+
+ procedure Process_Body (Decl : Node_Id) is
+ Body_Id : constant Entity_Id := Defining_Entity (Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Decl);
- procedure Set_SPARK_Flags is
+ begin
+ -- Ignore pragma when applied to the special body created for
+ -- inlining, recognized by its internal name _Parent.
+
+ if Chars (Body_Id) = Name_uParent then
+ return;
+ end if;
+
+ Check_Library_Level_Entity (Body_Id);
+
+ -- For entry bodies, verify the legality against:
+ -- * The mode of the context
+ -- * The mode of the spec (if any)
+
+ if Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
+
+ -- A stand alone subprogram body
+
+ if Body_Id = Spec_Id then
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity => Empty,
+ Entity_Pragma => Empty);
+
+ -- An entry or subprogram body that completes a previous
+ -- declaration.
+
+ else
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity => Spec_Id,
+ Entity_Pragma => SPARK_Pragma (Spec_Id));
+ end if;
+
+ Set_SPARK_Context;
+ Set_SPARK_Pragma (Body_Id, N);
+ Set_SPARK_Pragma_Inherited (Body_Id, False);
+
+ -- For package bodies, verify the legality against:
+ -- * The mode of the context
+ -- * The mode of the private part
+
+ -- This case is separated from protected and task bodies
+ -- because the statement part of the package body inherits
+ -- the mode of the body declarations.
+
+ elsif Nkind (Decl) = N_Package_Body then
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity => Spec_Id,
+ Entity_Pragma => SPARK_Aux_Pragma (Spec_Id));
+
+ Set_SPARK_Context;
+ Set_SPARK_Pragma (Body_Id, N);
+ Set_SPARK_Pragma_Inherited (Body_Id, False);
+ Set_SPARK_Aux_Pragma (Body_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+
+ -- For protected and task bodies, verify the legality against:
+ -- * The mode of the context
+ -- * The mode of the private part
+
+ else
+ pragma Assert
+ (Nkind_In (Decl, N_Protected_Body, N_Task_Body));
+
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity => Spec_Id,
+ Entity_Pragma => SPARK_Aux_Pragma (Spec_Id));
+
+ Set_SPARK_Context;
+ Set_SPARK_Pragma (Body_Id, N);
+ Set_SPARK_Pragma_Inherited (Body_Id, False);
+ end if;
+ end Process_Body;
+
+ --------------------------
+ -- Process_Overloadable --
+ --------------------------
+
+ procedure Process_Overloadable (Decl : Node_Id) is
+ Spec_Id : constant Entity_Id := Defining_Entity (Decl);
+
+ begin
+ Check_Library_Level_Entity (Spec_Id);
+
+ -- Verify the legality against:
+ -- * The mode of the context
+
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity => Empty,
+ Entity_Pragma => Empty);
+
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
+ end Process_Overloadable;
+
+ --------------------------
+ -- Process_Private_Part --
+ --------------------------
+
+ procedure Process_Private_Part (Decl : Node_Id) is
+ Spec_Id : constant Entity_Id := Defining_Entity (Decl);
+
+ begin
+ Check_Library_Level_Entity (Spec_Id);
+
+ -- Verify the legality against:
+ -- * The mode of the visible declarations
+
+ Check_Pragma_Conformance
+ (Context_Pragma => Empty,
+ Entity => Spec_Id,
+ Entity_Pragma => SPARK_Pragma (Spec_Id));
+
+ Set_SPARK_Context;
+ Set_SPARK_Aux_Pragma (Spec_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False);
+ end Process_Private_Part;
+
+ ----------------------------
+ -- Process_Statement_Part --
+ ----------------------------
+
+ procedure Process_Statement_Part (Decl : Node_Id) is
+ Body_Id : constant Entity_Id := Defining_Entity (Decl);
+
+ begin
+ Check_Library_Level_Entity (Body_Id);
+
+ -- Verify the legality against:
+ -- * The mode of the body declarations
+
+ Check_Pragma_Conformance
+ (Context_Pragma => Empty,
+ Entity => Body_Id,
+ Entity_Pragma => SPARK_Pragma (Body_Id));
+
+ Set_SPARK_Context;
+ Set_SPARK_Aux_Pragma (Body_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
+ end Process_Statement_Part;
+
+ --------------------------
+ -- Process_Visible_Part --
+ --------------------------
+
+ procedure Process_Visible_Part (Decl : Node_Id) is
+ Spec_Id : constant Entity_Id := Defining_Entity (Decl);
+
+ begin
+ Check_Library_Level_Entity (Spec_Id);
+
+ -- Verify the legality against:
+ -- * The mode of the context
+
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity => Empty,
+ Entity_Pragma => Empty);
+
+ -- A task unit declared without a definition does not set the
+ -- SPARK_Mode of the context because the task does not have any
+ -- entries that could inherit the mode.
+
+ if not Nkind_In (Decl, N_Single_Task_Declaration,
+ N_Task_Type_Declaration)
+ then
+ Set_SPARK_Context;
+ end if;
+
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
+ Set_SPARK_Aux_Pragma (Spec_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+ end Process_Visible_Part;
+
+ -----------------------
+ -- Set_SPARK_Context --
+ -----------------------
+
+ procedure Set_SPARK_Context is
begin
SPARK_Mode := Mode_Id;
SPARK_Mode_Pragma := N;
if SPARK_Mode = On then
Dynamic_Elaboration_Checks := False;
end if;
- end Set_SPARK_Flags;
+ end Set_SPARK_Context;
-- Local variables
- Body_Id : Entity_Id;
Context : Node_Id;
Mode : Name_Id;
- Spec_Id : Entity_Id;
Stmt : Node_Id;
-- Start of processing for Do_SPARK_Mode
raise Pragma_Exit;
end if;
- Set_SPARK_Flags;
+ Set_SPARK_Context;
-- The pragma acts as a configuration pragma in a compilation unit
and then List_Containing (N) = Context_Items (Context)
then
Check_Valid_Configuration_Pragma;
- Set_SPARK_Flags;
+ Set_SPARK_Context;
-- Otherwise the placement of the pragma within the tree dictates
-- its associated construct. Inspect the declarative list where
Stmt := Prev (N);
while Present (Stmt) loop
- -- Skip prior pragmas, but check for duplicates
+ -- Skip prior pragmas, but check for duplicates. Note that
+ -- this also takes care of pragmas generated for aspects.
if Nkind (Stmt) = N_Pragma then
if Pragma_Name (Stmt) = Pname then
raise Pragma_Exit;
end if;
- -- The pragma applies to a [generic] subprogram declaration.
- -- Note that this case covers an internally generated spec
- -- for a stand alone body.
+ -- The pragma applies to an expression function that has
+ -- already been rewritten into a subprogram declaration.
- -- [generic]
- -- procedure Proc ...;
- -- pragma SPARK_Mode ..;
+ -- function Expr_Func return ... is (...);
+ -- pragma SPARK_Mode ...;
- elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
- N_Subprogram_Declaration)
+ elsif Nkind (Stmt) = N_Subprogram_Declaration
+ and then Nkind (Original_Node (Stmt)) =
+ N_Expression_Function
then
- Spec_Id := Defining_Entity (Stmt);
- Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Pragma (Spec_Id),
- Entity_Pragma => Empty,
- Entity => Empty);
+ 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 ...;
- Set_SPARK_Pragma (Spec_Id, N);
- Set_SPARK_Pragma_Inherited (Spec_Id, False);
+ 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
null;
+ -- The pragma applies to an entry or [generic] subprogram
+ -- declaration.
+
+ -- entry Ent ...;
+ -- pragma SPARK_Mode ...;
+
+ -- [generic]
+ -- procedure Proc ...;
+ -- pragma SPARK_Mode ...;
+
+ elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ or else (Nkind (Stmt) = N_Entry_Declaration
+ and then Is_Protected_Type
+ (Scope (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.
Context := Unit (Parent (Context));
end if;
- -- The pragma appears within package declarations
-
- if Nkind (Context) = N_Package_Specification then
- Spec_Id := Defining_Entity (Context);
- Check_Library_Level_Entity (Spec_Id);
-
- -- The pragma is at the top of the visible declarations
-
- -- package Pack is
- -- pragma SPARK_Mode ...;
+ -- The pragma appears at the top of entry, package, protected
+ -- unit, subprogram or task unit body declarations.
- if List_Containing (N) = Visible_Declarations (Context) then
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Pragma (Spec_Id),
- Entity_Pragma => Empty,
- Entity => Empty);
- Set_SPARK_Flags;
-
- Set_SPARK_Pragma (Spec_Id, N);
- Set_SPARK_Pragma_Inherited (Spec_Id, False);
- Set_SPARK_Aux_Pragma (Spec_Id, N);
- Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+ -- entry Ent when ... is
+ -- pragma SPARK_Mode ...;
- -- The pragma is at the top of the private declarations
+ -- package body Pack is
+ -- pragma SPARK_Mode ...;
- -- package Pack is
- -- private
- -- pragma SPARK_Mode ...;
+ -- procedure Proc ... is
+ -- pragma SPARK_Mode;
- else
- Check_Pragma_Conformance
- (Context_Pragma => Empty,
- Entity_Pragma => SPARK_Pragma (Spec_Id),
- Entity => Spec_Id);
- Set_SPARK_Flags;
+ -- protected body Prot is
+ -- pragma SPARK_Mode ...;
- Set_SPARK_Aux_Pragma (Spec_Id, N);
- Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False);
- end if;
+ if Nkind_In (Context, N_Entry_Body,
+ N_Package_Body,
+ N_Protected_Body,
+ N_Subprogram_Body,
+ N_Task_Body)
+ then
+ Process_Body (Context);
- -- The pragma appears at the top of package body declarations
+ -- The pragma appears at the top of the visible or private
+ -- declaration of a package spec, protected or task unit.
- -- package body Pack is
+ -- package Pack is
+ -- pragma SPARK_Mode ...;
+ -- private
-- pragma SPARK_Mode ...;
- elsif Nkind (Context) = N_Package_Body then
- Spec_Id := Corresponding_Spec (Context);
- Body_Id := Defining_Entity (Context);
- Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Pragma (Body_Id),
- Entity_Pragma => SPARK_Aux_Pragma (Spec_Id),
- Entity => Spec_Id);
- Set_SPARK_Flags;
+ -- protected [type] Prot is
+ -- pragma SPARK_Mode ...;
+ -- private
+ -- pragma SPARK_Mode ...;
- Set_SPARK_Pragma (Body_Id, N);
- Set_SPARK_Pragma_Inherited (Body_Id, False);
- Set_SPARK_Aux_Pragma (Body_Id, N);
- Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+ elsif Nkind_In (Context, N_Package_Specification,
+ N_Protected_Definition,
+ N_Task_Definition)
+ then
+ if List_Containing (N) = Visible_Declarations (Context) then
+ Process_Visible_Part (Parent (Context));
+ else
+ Process_Private_Part (Parent (Context));
+ end if;
-- The pragma appears at the top of package body statements
elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
and then Nkind (Parent (Context)) = N_Package_Body
then
- Context := Parent (Context);
- Spec_Id := Corresponding_Spec (Context);
- Body_Id := Defining_Entity (Context);
- Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance
- (Context_Pragma => Empty,
- Entity_Pragma => SPARK_Pragma (Body_Id),
- Entity => Body_Id);
- Set_SPARK_Flags;
-
- Set_SPARK_Aux_Pragma (Body_Id, N);
- Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
+ Process_Statement_Part (Parent (Context));
-- The pragma appeared as an aspect of a [generic] subprogram
-- declaration that acts as a compilation unit.
elsif Nkind_In (Context, N_Generic_Subprogram_Declaration,
N_Subprogram_Declaration)
then
- Spec_Id := Defining_Entity (Context);
- Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Pragma (Spec_Id),
- Entity_Pragma => Empty,
- Entity => Empty);
-
- Set_SPARK_Pragma (Spec_Id, N);
- Set_SPARK_Pragma_Inherited (Spec_Id, False);
-
- -- The pragma appears at the top of subprogram body
- -- declarations.
-
- -- procedure Proc ... is
- -- pragma SPARK_Mode;
-
- elsif Nkind (Context) = N_Subprogram_Body then
- Spec_Id := Corresponding_Spec (Context);
- Context := Specification (Context);
- Body_Id := Defining_Entity (Context);
-
- -- Ignore pragma when applied to the special body created
- -- for inlining, recognized by its internal name _Parent.
-
- if Chars (Body_Id) = Name_uParent then
- return;
- end if;
-
- Check_Library_Level_Entity (Body_Id);
-
- -- The body is a completion of a previous declaration
-
- if Present (Spec_Id) then
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Pragma (Body_Id),
- Entity_Pragma => SPARK_Pragma (Spec_Id),
- Entity => Spec_Id);
-
- -- The body acts as spec
-
- else
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Pragma (Body_Id),
- Entity_Pragma => Empty,
- Entity => Empty);
- end if;
-
- Set_SPARK_Flags;
-
- Set_SPARK_Pragma (Body_Id, N);
- Set_SPARK_Pragma_Inherited (Body_Id, False);
+ Process_Overloadable (Context);
-- The pragma does not apply to a legal construct, issue error
return;
end if;
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
if not Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
Pragma_Misplaced;
-- Local variables
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id);
-- Preanalyze one of the optional arguments "Requires" or "Ensures"
-- Local variables
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Clause : Node_Id;
Clauses : Node_Id;
Depends : Node_Id;
end if;
end Corresponding_Generic_Type;
- ---------------------------
- -- Corresponding_Spec_Of --
- ---------------------------
-
- function Corresponding_Spec_Of (Decl : Node_Id) return Entity_Id is
- begin
- if Nkind_In (Decl, N_Package_Body, N_Subprogram_Body)
- and then Present (Corresponding_Spec (Decl))
- then
- return Corresponding_Spec (Decl);
-
- elsif Nkind_In (Decl, N_Package_Body_Stub, N_Subprogram_Body_Stub)
- and then Present (Corresponding_Spec_Of_Stub (Decl))
- then
- return Corresponding_Spec_Of_Stub (Decl);
-
- else
- return Defining_Entity (Decl);
- end if;
- end Corresponding_Spec_Of;
-
--------------------
-- Current_Entity --
--------------------
U := Full_View (E);
end if;
- when Type_Kind =>
- if Present (Full_View (E)) then
- U := Full_View (E);
+ when Entry_Kind =>
+ if Nkind (Parent (E)) = N_Entry_Body then
+ declare
+ Prot_Item : Entity_Id;
+ begin
+ -- Traverse the entity list of the protected type and locate
+ -- an entry declaration which matches the entry body.
+
+ Prot_Item := First_Entity (Scope (E));
+ while Present (Prot_Item) loop
+ if Ekind (Prot_Item) = E_Entry
+ and then Corresponding_Body (Parent (Prot_Item)) = E
+ then
+ U := Prot_Item;
+ exit;
+ end if;
+
+ Next_Entity (Prot_Item);
+ end loop;
+ end;
+ end if;
+
+ when Formal_Kind =>
+ if Present (Spec_Entity (E)) then
+ U := Spec_Entity (E);
end if;
when E_Package_Body =>
P := Parent (P);
end if;
- U := Corresponding_Spec (P);
+ if Nkind (P) = N_Package_Body
+ and then Present (Corresponding_Spec (P))
+ then
+ U := Corresponding_Spec (P);
+
+ elsif Nkind (P) = N_Package_Body_Stub
+ and then Present (Corresponding_Spec_Of_Stub (P))
+ then
+ U := Corresponding_Spec_Of_Stub (P);
+ end if;
+
+ when E_Protected_Body =>
+ P := Parent (E);
+
+ if Nkind (P) = N_Protected_Body
+ and then Present (Corresponding_Spec (P))
+ then
+ U := Corresponding_Spec (P);
+
+ elsif Nkind (P) = N_Protected_Body_Stub
+ and then Present (Corresponding_Spec_Of_Stub (P))
+ then
+ U := Corresponding_Spec_Of_Stub (P);
+ end if;
when E_Subprogram_Body =>
P := Parent (E);
P := Parent (P);
- if Nkind (P) = N_Subprogram_Body_Stub then
- if Present (Library_Unit (P)) then
-
- -- Get to the function or procedure (generic) entity through
- -- the body entity.
-
- U :=
- Unique_Entity (Defining_Entity (Get_Body_From_Stub (P)));
- end if;
- else
+ if Nkind (P) = N_Subprogram_Body
+ and then Present (Corresponding_Spec (P))
+ then
U := Corresponding_Spec (P);
- end if;
- when Formal_Kind =>
- if Present (Spec_Entity (E)) then
- U := Spec_Entity (E);
+ elsif Nkind (P) = N_Subprogram_Body_Stub
+ and then Present (Corresponding_Spec_Of_Stub (P))
+ then
+ U := Corresponding_Spec_Of_Stub (P);
end if;
when E_Task_Body =>
P := Parent (E);
- U := Corresponding_Spec (P);
- when E_Entry =>
- if Nkind (Parent (E)) = N_Entry_Body then
- declare
- Decl : Entity_Id := First_Entity (Scope (E));
- begin
- -- Traverse the entity list of the protected object
- -- and locate an entry declaration with a matching
- -- Corresponding_Body.
+ if Nkind (P) = N_Task_Body
+ and then Present (Corresponding_Spec (P))
+ then
+ U := Corresponding_Spec (P);
- while Present (Decl) loop
- if Ekind (Decl) = E_Entry
- and then Corresponding_Body (Parent (Decl)) = E
- then
- U := Decl;
- exit;
- end if;
- Next_Entity (Decl);
- end loop;
- pragma Assert (Present (Decl));
- end;
+ elsif Nkind (P) = N_Task_Body_Stub
+ and then Present (Corresponding_Spec_Of_Stub (P))
+ then
+ U := Corresponding_Spec_Of_Stub (P);
+ end if;
+
+ when Type_Kind =>
+ if Present (Full_View (E)) then
+ U := Full_View (E);
end if;
when others =>
-- attribute, except in the case of formal private and derived types.
-- Possible optimization???
- function Corresponding_Spec_Of (Decl : Node_Id) return Entity_Id;
- -- Return the corresponding spec of Decl when it denotes a package or a
- -- subprogram [stub], or the defining entity of Decl.
-
function Current_Entity (N : Node_Id) return Entity_Id;
pragma Inline (Current_Entity);
-- Find the currently visible definition for a given identifier, that is to
function Unique_Defining_Entity (N : Node_Id) return Entity_Id;
-- Return the entity which represents declaration N, so that different
-- views of the same entity have the same unique defining entity:
- -- * package spec and body;
- -- * subprogram declaration, subprogram stub and subprogram body;
- -- * entry declaration and entry body;
- -- * task declaration, task body stub and task body;
- -- * private view and full view of a type;
- -- * private view and full view of a deferred constant.
+ -- * entry declaration and entry body
+ -- * package spec and body
+ -- * protected type declaration, protected body stub and protected body
+ -- * private view and full view of a deferred constant
+ -- * private view and full view of a type
+ -- * subprogram declaration, subprogram stub and subprogram body
+ -- * task type declaration, task body stub and task body
-- In other cases, return the defining entity for N.
function Unique_Entity (E : Entity_Id) return Entity_Id;
(N : Node_Id) return Boolean is
begin
pragma Assert (False
- or else NT (N).Nkind = N_Subprogram_Body);
+ or else NT (N).Nkind = N_Subprogram_Body
+ or else NT (N).Nkind = N_Subprogram_Declaration);
return Flag8 (N);
end Is_Entry_Barrier_Function;
return Flag6 (N);
end Is_Task_Allocation_Block;
+ function Is_Task_Body_Procedure
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Subprogram_Body
+ or else NT (N).Nkind = N_Subprogram_Declaration);
+ return Flag1 (N);
+ end Is_Task_Body_Procedure;
+
function Is_Task_Master
(N : Node_Id) return Boolean is
begin
(N : Node_Id; Val : Boolean := True) is
begin
pragma Assert (False
- or else NT (N).Nkind = N_Subprogram_Body);
+ or else NT (N).Nkind = N_Subprogram_Body
+ or else NT (N).Nkind = N_Subprogram_Declaration);
Set_Flag8 (N, Val);
end Set_Is_Entry_Barrier_Function;
Set_Flag6 (N, Val);
end Set_Is_Task_Allocation_Block;
+ procedure Set_Is_Task_Body_Procedure
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Subprogram_Body
+ or else NT (N).Nkind = N_Subprogram_Declaration);
+ Set_Flag1 (N, Val);
+ end Set_Is_Task_Body_Procedure;
+
procedure Set_Is_Task_Master
(N : Node_Id; Val : Boolean := True) is
begin
-- concatenation nodes in instances.
-- Is_Controlling_Actual (Flag16-Sem)
- -- This flag is set on in an expression that is a controlling argument in
+ -- This flag is set on an expression that is a controlling argument in
-- a dispatching call. It is off in all other cases. See Sem_Disp for
-- details of its use.
-- the enclosing object.
-- Is_Entry_Barrier_Function (Flag8-Sem)
- -- This flag is set in an N_Subprogram_Body node which is the expansion
- -- of an entry barrier from a protected entry body. It is used for the
- -- circuitry checking for incorrect use of Current_Task.
+ -- This flag is set on N_Subprogram_Declaration and N_Subprogram_Body
+ -- nodes which emulate the barrier function of a protected entry body.
+ -- The flag is used when checking for incorrect use of Current_Task.
-- Is_Expanded_Build_In_Place_Call (Flag11-Sem)
-- This flag is set in an N_Function_Call node to indicate that the extra
-- Expunge_Unactivated_Tasks to complete any tasks that have been
-- allocated but not activated when the allocator completes abnormally.
+ -- Is_Task_Body_Procedure (Flag1-Sem)
+ -- This flag is set on N_Subprogram_Declaration and N_Subprogram_Body
+ -- nodes which emulate the body of a task unit.
+
-- Is_Task_Master (Flag5-Sem)
-- A flag set in a Subprogram_Body, Block_Statement or Task_Body node to
-- indicate that the construct is a task master (i.e. has declared tasks
-- Body_To_Inline (Node3-Sem)
-- Corresponding_Body (Node5-Sem)
-- Parent_Spec (Node4-Sem)
+ -- Is_Entry_Barrier_Function (Flag8-Sem)
+ -- Is_Task_Body_Procedure (Flag1-Sem)
------------------------------------------
-- 6.1 Abstract Subprogram Declaration --
-- Acts_As_Spec (Flag4-Sem)
-- Bad_Is_Detected (Flag15) used only by parser
-- Do_Storage_Check (Flag17-Sem)
- -- Is_Protected_Subprogram_Body (Flag7-Sem)
-- Is_Entry_Barrier_Function (Flag8-Sem)
+ -- Is_Protected_Subprogram_Body (Flag7-Sem)
+ -- Is_Task_Body_Procedure (Flag1-Sem)
-- Is_Task_Master (Flag5-Sem)
-- Was_Originally_Stub (Flag13-Sem)
-- Has_Relative_Deadline_Pragma (Flag9-Sem)
function Is_Task_Allocation_Block
(N : Node_Id) return Boolean; -- Flag6
+ function Is_Task_Body_Procedure
+ (N : Node_Id) return Boolean; -- Flag1
+
function Is_Task_Master
(N : Node_Id) return Boolean; -- Flag5
procedure Set_Is_Task_Allocation_Block
(N : Node_Id; Val : Boolean := True); -- Flag6
+ procedure Set_Is_Task_Body_Procedure
+ (N : Node_Id; Val : Boolean := True); -- Flag1
+
procedure Set_Is_Task_Master
(N : Node_Id; Val : Boolean := True); -- Flag5
pragma Inline (Is_Static_Expression);
pragma Inline (Is_Subprogram_Descriptor);
pragma Inline (Is_Task_Allocation_Block);
+ pragma Inline (Is_Task_Body_Procedure);
pragma Inline (Is_Task_Master);
pragma Inline (Iteration_Scheme);
pragma Inline (Itype);
pragma Inline (Set_Is_Static_Expression);
pragma Inline (Set_Is_Subprogram_Descriptor);
pragma Inline (Set_Is_Task_Allocation_Block);
+ pragma Inline (Set_Is_Task_Body_Procedure);
pragma Inline (Set_Is_Task_Master);
pragma Inline (Set_Iteration_Scheme);
pragma Inline (Set_Iterator_Specification);
projects / gcc.git / commitdiff