return Flag215 (Base_Type (Id));
end Is_Param_Block_Component_Type;
+ function Is_Partial_DIC_Procedure (Id : E) return B is
+ Partial_DIC_Suffix : constant String := "Partial_DIC";
+ DIC_Nam : constant String := Get_Name_String (Chars (Id));
+
+ begin
+ pragma Assert (Ekind (Id) in E_Function | E_Procedure);
+
+ -- Instead of adding a new Entity_Id flag (which are in short supply),
+ -- we test the form of the subprogram name. When the node field and flag
+ -- situation is eased, this should be replaced with a flag. ???
+
+ if DIC_Nam'Length > Partial_DIC_Suffix'Length
+ and then
+ DIC_Nam
+ (DIC_Nam'Last - Partial_DIC_Suffix'Length + 1 .. DIC_Nam'Last) =
+ Partial_DIC_Suffix
+ then
+ return True;
+ else
+ return False;
+ end if;
+ end Is_Partial_DIC_Procedure;
+
function Is_Partial_Invariant_Procedure (Id : E) return B is
begin
pragma Assert (Ekind (Id) in E_Function | E_Procedure);
while Present (Subp_Elmt) loop
Subp_Id := Node (Subp_Elmt);
- if Is_DIC_Procedure (Subp_Id) then
+ -- Currently the flag Is_DIC_Procedure is set for both normal DIC
+ -- check procedures as well as for partial DIC check procedures,
+ -- and we don't have a flag for the partial procedures.
+
+ if Is_DIC_Procedure (Subp_Id)
+ and then not Is_Partial_DIC_Procedure (Subp_Id)
+ then
return Subp_Id;
end if;
return Ekind (Id);
end Parameter_Mode;
+ ---------------------------
+ -- Partial_DIC_Procedure --
+ ---------------------------
+
+ function Partial_DIC_Procedure (Id : E) return E is
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
+
+ begin
+ pragma Assert (Is_Type (Id));
+
+ Subps := Subprograms_For_Type (Base_Type (Id));
+
+ if Present (Subps) then
+ Subp_Elmt := First_Elmt (Subps);
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Is_Partial_DIC_Procedure (Subp_Id) then
+ return Subp_Id;
+ end if;
+
+ Next_Elmt (Subp_Elmt);
+ end loop;
+ end if;
+
+ return Empty;
+ end Partial_DIC_Procedure;
+
---------------------------------
-- Partial_Invariant_Procedure --
---------------------------------
procedure Set_DIC_Procedure (Id : E; V : E) is
Base_Typ : Entity_Id;
- Subp_Elmt : Elmt_Id;
- Subp_Id : Entity_Id;
Subps : Elist_Id;
begin
Set_Subprograms_For_Type (Base_Typ, Subps);
end if;
- Subp_Elmt := First_Elmt (Subps);
Prepend_Elmt (V, Subps);
+ end Set_DIC_Procedure;
- -- Check for a duplicate default initial condition procedure
-
- while Present (Subp_Elmt) loop
- Subp_Id := Node (Subp_Elmt);
-
- if Is_DIC_Procedure (Subp_Id) then
- raise Program_Error;
- end if;
+ -------------------------------------
+ -- Set_Partial_Invariant_Procedure --
+ -------------------------------------
- Next_Elmt (Subp_Elmt);
- end loop;
- end Set_DIC_Procedure;
+ procedure Set_Partial_DIC_Procedure (Id : E; V : E) is
+ begin
+ Set_DIC_Procedure (Id, V);
+ end Set_Partial_DIC_Procedure;
-----------------------------
-- Set_Invariant_Procedure --
-- of a single protected/task type, the references are examined as they
-- must appear only within the type defintion and the corresponding body.
+-- Partial_DIC_Procedure (synthesized)
+-- Defined in type entities. Set for a private type and its full view
+-- when the type is subject to pragma Default_Initial_Condition (DIC), or
+-- when the type inherits a DIC pragma from a parent type. Points to the
+-- entity of a procedure that takes a single argument of the given type
+-- and verifies the assertion expression of the DIC pragma at run time.
+-- When present, the Partial_DIC_Procedure of a type only checks DICs
+-- associated with the partial (private) view of the type, and is invoked
+-- by the full DIC_Procedure (which may check additional DICs associated
+-- with the full view).
+
+-- Note: the reason this is marked as a synthesized attribute is that the
+-- way this is stored is as an element of the Subprograms_For_Type field.
+
-- Partial_Invariant_Procedure (synthesized)
-- Defined in types and subtypes. Set for private types when one or more
-- [class-wide] type invariants apply to them. Points to the entity for a
-- Is_Full_Access (synth)
-- Is_Controlled (synth)
-- Object_Size_Clause (synth)
+ -- Partial_DIC_Procedure (synth)
-- Partial_Invariant_Procedure (synth)
-- Predicate_Function (synth)
-- Predicate_Function_M (synth)
-- Is_Invariant_Procedure (Flag257) (non-generic case only)
-- Is_Machine_Code_Subprogram (Flag137) (non-generic case only)
-- Is_Null_Init_Proc (Flag178)
+ -- Is_Partial_DIC_Procedure (synth) (non-generic case only)
-- Is_Partial_Invariant_Procedure (Flag292) (non-generic case only)
-- Is_Predicate_Function (Flag255) (non-generic case only)
-- Is_Predicate_Function_M (Flag256) (non-generic case only)
function Is_Packed_Array_Impl_Type (Id : E) return B;
function Is_Potentially_Use_Visible (Id : E) return B;
function Is_Param_Block_Component_Type (Id : E) return B;
+ function Is_Partial_DIC_Procedure (Id : E) return B;
function Is_Partial_Invariant_Procedure (Id : E) return B;
function Is_Predicate_Function (Id : E) return B;
function Is_Predicate_Function_M (Id : E) return B;
---------------------------------------------------
function DIC_Procedure (Id : E) return E;
+ function Partial_DIC_Procedure (Id : E) return E;
function Invariant_Procedure (Id : E) return E;
function Partial_Invariant_Procedure (Id : E) return E;
function Predicate_Function (Id : E) return E;
function Predicate_Function_M (Id : E) return E;
procedure Set_DIC_Procedure (Id : E; V : E);
+ procedure Set_Partial_DIC_Procedure (Id : E; V : E);
procedure Set_Invariant_Procedure (Id : E; V : E);
procedure Set_Partial_Invariant_Procedure (Id : E; V : E);
procedure Set_Predicate_Function (Id : E; V : E);
Typ => Ctype,
With_Default_Init => True));
+ -- If Default_Initial_Condition applies to the component type,
+ -- add a DIC check after the component is default-initialized.
+ -- It will be analyzed and resolved before the code for
+ -- initialization of other components.
+
+ -- Theoretically this might also be needed for cases where
+ -- the component type doesn't have an init proc (such as for
+ -- Default_Value cases), but those should be uncommon, and for
+ -- now we only support the init proc case. ???
+
+ if Has_DIC (Ctype) and then Present (DIC_Procedure (Ctype)) then
+ Append_To (Stmts,
+ Build_DIC_Call (Loc, New_Copy_Tree (Indexed_Comp), Ctype));
+ end if;
+
-- If the component type has invariants, add an invariant
-- check after the component is default-initialized. It will
-- be analyzed and resolved before the code for initialization
then
Check_Ancestor_Discriminants (Entity (Ancestor));
end if;
+
+ -- If ancestor type has Default_Initialization_Condition,
+ -- add a DIC check after the ancestor object is initialized
+ -- by default.
+
+ if Has_DIC (Entity (Ancestor))
+ and then Present (DIC_Procedure (Entity (Ancestor)))
+ then
+ Append_To (L,
+ Build_DIC_Call
+ (Loc, New_Copy_Tree (Ref), Entity (Ancestor)));
+ end if;
end if;
-- Handle calls to C++ constructors
end;
end if;
+ -- If the component association was specified with a box and the
+ -- component type has a Default_Initial_Condition, then generate
+ -- a call to the DIC procedure.
+
+ if Has_DIC (Etype (Selector))
+ and then Was_Default_Init_Box_Association (Comp)
+ and then Present (DIC_Procedure (Etype (Selector)))
+ then
+ Append_To (L,
+ Build_DIC_Call (Loc,
+ Make_Selected_Component (Loc,
+ Prefix => New_Copy_Tree (Target),
+ Selector_Name => New_Occurrence_Of (Selector, Loc)),
+ Etype (Selector)));
+ end if;
+
Next (Comp);
end loop;
------------------------
function Init_One_Dimension (N : Int) return List_Id is
- Index : Entity_Id;
+ Index : Entity_Id;
+ DIC_Call : Node_Id;
+ Result_List : List_Id;
+
+ function Possible_DIC_Call return Node_Id;
+ -- If the component type has Default_Initial_Conditions and a DIC
+ -- procedure that is not an empty body, then builds a call to the
+ -- DIC procedure and returns it.
+
+ -----------------------
+ -- Possible_DIC_Call --
+ -----------------------
+
+ function Possible_DIC_Call return Node_Id is
+ begin
+ -- When the component's type has a Default_Initial_Condition, then
+ -- create a call for the DIC check.
+
+ if Has_DIC (Comp_Type)
+ -- In GNATprove mode, the component DICs are checked by other
+ -- means. They should not be added to the record type DIC
+ -- procedure, so that the procedure can be used to check the
+ -- record type invariants or DICs if any.
+
+ and then not GNATprove_Mode
+
+ and then Present (DIC_Procedure (Comp_Type))
+
+ and then not Has_Null_Body (DIC_Procedure (Comp_Type))
+ then
+ return
+ Build_DIC_Call (Loc,
+ Make_Indexed_Component (Loc,
+ Prefix => Make_Identifier (Loc, Name_uInit),
+ Expressions => Index_List),
+ Comp_Type);
+ else
+ return Empty;
+ end if;
+ end Possible_DIC_Call;
+
+ -- Start of processing for Init_One_Dimension
begin
-- If the component does not need initializing, then there is nothing
-- to do here, so we return a null body. This occurs when generating
-- the dummy Init_Proc needed for Initialize_Scalars processing.
+ -- An exception is if component type has a Default_Initial_Condition,
+ -- in which case we generate a call to the type's DIC procedure.
if not Has_Non_Null_Base_Init_Proc (Comp_Type)
and then not Comp_Simple_Init
and then not Has_Task (Comp_Type)
and then not Has_Default_Aspect (A_Type)
+ and then (not Has_DIC (Comp_Type)
+ or else N > Number_Dimensions (A_Type))
then
- return New_List (Make_Null_Statement (Loc));
+ DIC_Call := Possible_DIC_Call;
+
+ if Present (DIC_Call) then
+ return New_List (DIC_Call);
+ else
+ return New_List (Make_Null_Statement (Loc));
+ end if;
-- If all dimensions dealt with, we simply initialize the component
+ -- and append a call to component type's DIC procedure when needed.
elsif N > Number_Dimensions (A_Type) then
- return Init_Component;
+ DIC_Call := Possible_DIC_Call;
+
+ if Present (DIC_Call) then
+ Result_List := Init_Component;
+ Append (DIC_Call, Result_List);
+ return Result_List;
+
+ else
+ return Init_Component;
+ end if;
-- Here we generate the required loop
-- 3. Tasks are present
-- 4. The type is marked as a public entity
-- 5. The array type has a Default_Component_Value aspect
+ -- 6. The array component type has a Default_Initialization_Condition
-- The reason for the public entity test is to deal properly with the
-- Initialize_Scalars pragma. This pragma can be set in the client and
Has_Default_Init := Has_Non_Null_Base_Init_Proc (Comp_Type)
or else Comp_Simple_Init
or else Has_Task (Comp_Type)
- or else Has_Default_Aspect (A_Type);
+ or else Has_Default_Aspect (A_Type)
+ or else Has_DIC (Comp_Type);
if Has_Default_Init
or else (not Restriction_Active (No_Initialize_Scalars)
Actions := No_List;
end if;
+ -- When the component's type has a Default_Initial_Condition,
+ -- and the component is default initialized, then check the
+ -- DIC here.
+
+ if Has_DIC (Typ)
+ and then not Present (Expression (Decl))
+ and then Present (DIC_Procedure (Typ))
+ and then not Has_Null_Body (DIC_Procedure (Typ))
+
+ -- The DICs of ancestors are checked as part of the type's
+ -- DIC procedure.
+
+ and then Chars (Id) /= Name_uParent
+
+ -- In GNATprove mode, the component DICs are checked by other
+ -- means. They should not be added to the record type DIC
+ -- procedure, so that the procedure can be used to check the
+ -- record type invariants or DICs if any.
+
+ and then not GNATprove_Mode
+ then
+ Append_New_To (Actions,
+ Build_DIC_Call
+ (Comp_Loc,
+ Make_Selected_Component (Comp_Loc,
+ Prefix =>
+ Make_Identifier (Comp_Loc, Name_uInit),
+ Selector_Name =>
+ New_Occurrence_Of (Id, Comp_Loc)),
+ Typ));
+ end if;
+
if Present (Checks) then
if Chars (Id) = Name_uParent then
Append_List_To (Parent_Stmts, Checks);
if Comes_From_Source (Def_Id)
and then Has_DIC (Typ)
and then Present (DIC_Procedure (Typ))
+ and then not Has_Null_Body (DIC_Procedure (Typ))
and then not Has_Init_Expression (N)
and then not Is_Imported (Def_Id)
then
declare
- DIC_Call : constant Node_Id := Build_DIC_Call (Loc, Def_Id, Typ);
-
+ DIC_Call : constant Node_Id :=
+ Build_DIC_Call
+ (Loc, New_Occurrence_Of (Def_Id, Loc), Typ);
begin
if Present (Next_N) then
Insert_Before_And_Analyze (Next_N, DIC_Call);
Process_Pending_Access_Types (Def_Id);
Freeze_Stream_Operations (N, Def_Id);
- -- Generate the [spec and] body of the procedure tasked with the runtime
- -- verification of pragma Default_Initial_Condition's expression.
-
- if Has_DIC (Def_Id) then
- Build_DIC_Procedure_Body (Def_Id, For_Freeze => True);
- end if;
-
-- Generate the [spec and] body of the invariant procedure tasked with
-- the runtime verification of all invariants that pertain to the type.
-- This includes invariants on the partial and full view, inherited
-- subprograms, which may involve local declarations of local
-- subtypes to which these checks do not apply.
- elsif Has_Invariants (Def_Id) then
- if not Predicate_Check_In_Scope (Def_Id)
- or else (Ekind (Current_Scope) = E_Function
- and then Is_Predicate_Function (Current_Scope))
- then
- null;
- else
- Build_Invariant_Procedure_Body (Def_Id);
+ else
+ if Has_Invariants (Def_Id) then
+ if not Predicate_Check_In_Scope (Def_Id)
+ or else (Ekind (Current_Scope) = E_Function
+ and then Is_Predicate_Function (Current_Scope))
+ then
+ null;
+ else
+ Build_Invariant_Procedure_Body (Def_Id);
+ end if;
+ end if;
+
+ -- Generate the [spec and] body of the procedure tasked with the
+ -- run-time verification of pragma Default_Initial_Condition's
+ -- expression.
+
+ if Has_DIC (Def_Id) then
+ Build_DIC_Procedure_Body (Def_Id);
end if;
end if;
Rewrite (N, New_Occurrence_Of (Temp, Loc));
Analyze_And_Resolve (N, PtrT);
+
+ -- When designated type has Default_Initial_Condition aspects,
+ -- make a call to the type's DIC procedure to perform the
+ -- checks. Theoretically this might also be needed for cases
+ -- where the type doesn't have an init proc, but those should
+ -- be very uncommon, and for now we only support the init proc
+ -- case. ???
+
+ if Has_DIC (Dtyp)
+ and then Present (DIC_Procedure (Dtyp))
+ and then not Has_Null_Body (DIC_Procedure (Dtyp))
+ then
+ Insert_Action (N,
+ Build_DIC_Call (Loc,
+ Make_Explicit_Dereference (Loc,
+ Prefix => New_Occurrence_Of (Temp, Loc)),
+ Dtyp));
+ end if;
end if;
end if;
end;
-- procedure for it as done during regular expansion for compilation.
if Has_DIC (E) and then Is_Tagged_Type (E) then
- Build_DIC_Procedure_Body (E, For_Freeze => True);
+ -- Why is this needed for DIC, but not for other aspects (such as
+ -- Type_Invariant)???
+
+ Build_DIC_Procedure_Body (E);
end if;
end Expand_SPARK_N_Freeze_Type;
and then Present (DIC_Procedure (Typ))
and then not Has_Init_Expression (N)
then
- Call := Build_DIC_Call (Loc, Obj_Id, Typ);
+ Call := Build_DIC_Call (Loc, New_Occurrence_Of (Obj_Id, Loc), Typ);
-- Partially insert the call into the tree by setting its parent
-- pointer.
--------------------
function Build_DIC_Call
- (Loc : Source_Ptr;
- Obj_Id : Entity_Id;
- Typ : Entity_Id) return Node_Id
+ (Loc : Source_Ptr;
+ Obj_Name : Node_Id;
+ Typ : Entity_Id) return Node_Id
is
Proc_Id : constant Entity_Id := DIC_Procedure (Typ);
Formal_Typ : constant Entity_Id := Etype (First_Formal (Proc_Id));
begin
+ -- The DIC procedure has a null body if assertions are disabled or
+ -- Assertion_Policy Ignore is in effect. In that case, it would be
+ -- nice to generate a null statement instead of a call to the DIC
+ -- procedure, but doing that seems to interfere with the determination
+ -- of ECRs (early call regions) in SPARK. ???
+
return
Make_Procedure_Call_Statement (Loc,
Name => New_Occurrence_Of (Proc_Id, Loc),
Parameter_Associations => New_List (
Make_Unchecked_Type_Conversion (Loc,
Subtype_Mark => New_Occurrence_Of (Formal_Typ, Loc),
- Expression => New_Occurrence_Of (Obj_Id, Loc))));
+ Expression => Obj_Name)));
end Build_DIC_Call;
------------------------------
-- Ghost mode.
procedure Build_DIC_Procedure_Body
- (Typ : Entity_Id;
- For_Freeze : Boolean := False)
+ (Typ : Entity_Id;
+ Partial_DIC : Boolean := False)
is
+ Pragmas_Seen : Elist_Id := No_Elist;
+ -- This list contains all DIC pragmas processed so far. The list is used
+ -- to avoid redundant Default_Initial_Condition checks.
+
procedure Add_DIC_Check
(DIC_Prag : Node_Id;
DIC_Expr : Node_Id;
-- pragma. All generated code is added to list Stmts.
procedure Add_Inherited_Tagged_DIC
- (DIC_Prag : Node_Id;
- Par_Typ : Entity_Id;
- Deriv_Typ : Entity_Id;
- Stmts : in out List_Id);
+ (DIC_Prag : Node_Id;
+ Expr : Node_Id;
+ Stmts : in out List_Id);
-- Add a runtime check to verify assertion expression DIC_Expr of
- -- inherited pragma DIC_Prag. This routine applies class-wide pre- and
- -- postcondition-like runtime semantics to the check. Par_Typ is the
- -- parent type whose DIC pragma is being inherited. Deriv_Typ is the
- -- derived type inheriting the DIC pragma. All generated code is added
- -- to list Stmts.
+ -- inherited pragma DIC_Prag. This routine applies class-wide pre-
+ -- and postcondition-like runtime semantics to the check. Expr is
+ -- the assertion expression after substitition has been performed
+ -- (via Replace_References). All generated code is added to list Stmts.
+
+ procedure Add_Inherited_DICs
+ (T : Entity_Id;
+ Priv_Typ : Entity_Id;
+ Full_Typ : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id);
+ -- Generate a DIC check for each inherited Default_Initial_Condition
+ -- coming from all parent types of type T. Priv_Typ and Full_Typ denote
+ -- the partial and full view of the parent type. Obj_Id denotes the
+ -- entity of the _object formal parameter of the DIC procedure. All
+ -- created checks are added to list Checks.
procedure Add_Own_DIC
(DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
+ Obj_Id : Entity_Id;
Stmts : in out List_Id);
-- Add a runtime check to verify the assertion expression of pragma
- -- DIC_Prag. DIC_Typ is the owner of the DIC pragma. All generated code
- -- is added to list Stmts.
+ -- DIC_Prag. DIC_Typ is the owner of the DIC pragma. Obj_Id is the
+ -- object to substitute in the assertion expression for any references
+ -- to the current instance of the type All generated code is added to
+ -- list Stmts.
+
+ procedure Add_Parent_DICs
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id);
+ -- Generate a Default_Initial_Condition check for each inherited DIC
+ -- aspect coming from all parent types of type T. Obj_Id denotes the
+ -- entity of the _object formal parameter of the DIC procedure. All
+ -- created checks are added to list Checks.
-------------------
-- Add_DIC_Check --
Make_Pragma_Argument_Association (Loc,
Expression => DIC_Expr))));
end if;
+
+ -- Add the pragma to the list of processed pragmas
+
+ Append_New_Elmt (DIC_Prag, Pragmas_Seen);
end Add_DIC_Check;
-----------------------
------------------------------
procedure Add_Inherited_Tagged_DIC
- (DIC_Prag : Node_Id;
- Par_Typ : Entity_Id;
- Deriv_Typ : Entity_Id;
- Stmts : in out List_Id)
+ (DIC_Prag : Node_Id;
+ Expr : Node_Id;
+ Stmts : in out List_Id)
is
- Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ);
- DIC_Args : constant List_Id :=
- Pragma_Argument_Associations (DIC_Prag);
- DIC_Arg : constant Node_Id := First (DIC_Args);
- DIC_Expr : constant Node_Id := Expression_Copy (DIC_Arg);
- Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ);
+ begin
+ -- Once the DIC assertion expression is fully processed, add a check
+ -- to the statements of the DIC procedure.
- Expr : Node_Id;
+ Add_DIC_Check
+ (DIC_Prag => DIC_Prag,
+ DIC_Expr => Expr,
+ Stmts => Stmts);
+ end Add_Inherited_Tagged_DIC;
+
+ ------------------------
+ -- Add_Inherited_DICs --
+ ------------------------
+
+ procedure Add_Inherited_DICs
+ (T : Entity_Id;
+ Priv_Typ : Entity_Id;
+ Full_Typ : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id)
+ is
+ Deriv_Typ : Entity_Id;
+ Expr : Node_Id;
+ Prag : Node_Id;
+ Prag_Expr : Node_Id;
+ Prag_Expr_Arg : Node_Id;
+ Prag_Typ : Node_Id;
+ Prag_Typ_Arg : Node_Id;
+
+ Par_Proc : Entity_Id;
+ -- The "partial" invariant procedure of Par_Typ
+
+ Par_Typ : Entity_Id;
+ -- The suitable view of the parent type used in the substitution of
+ -- type attributes.
begin
- -- The processing of an inherited DIC assertion expression starts off
- -- with a copy of the original parent expression where all references
- -- to the parent type have already been replaced with references to
- -- the _object formal parameter of the parent type's DIC procedure.
+ if not Present (Priv_Typ) and then not Present (Full_Typ) then
+ return;
+ end if;
- pragma Assert (Present (DIC_Expr));
- Expr := New_Copy_Tree (DIC_Expr);
+ -- When the type inheriting the class-wide invariant is a concurrent
+ -- type, use the corresponding record type because it contains all
+ -- primitive operations of the concurrent type and allows for proper
+ -- substitution.
- -- Perform the following substitutions:
+ if Is_Concurrent_Type (T) then
+ Deriv_Typ := Corresponding_Record_Type (T);
+ else
+ Deriv_Typ := T;
+ end if;
- -- * Replace a reference to the _object parameter of the parent
- -- type's DIC procedure with a reference to the _object parameter
- -- of the derived types' DIC procedure.
+ pragma Assert (Present (Deriv_Typ));
- -- * Replace a reference to a discriminant of the parent type with
- -- a suitable value from the point of view of the derived type.
+ -- Determine which rep item chain to use. Precedence is given to that
+ -- of the parent type's partial view since it usually carries all the
+ -- class-wide invariants.
- -- * Replace a call to an overridden parent primitive with a call
- -- to the overriding derived type primitive.
+ if Present (Priv_Typ) then
+ Prag := First_Rep_Item (Priv_Typ);
+ else
+ Prag := First_Rep_Item (Full_Typ);
+ end if;
- -- * Replace a call to an inherited parent primitive with a call to
- -- the internally-generated inherited derived type primitive.
+ while Present (Prag) loop
+ if Nkind (Prag) = N_Pragma
+ and then Pragma_Name (Prag) = Name_Default_Initial_Condition
+ then
+ -- Nothing to do if the pragma was already processed
- -- Note that primitives defined in the private part are automatically
- -- handled by the overriding/inheritance mechanism and do not require
- -- an extra replacement pass.
+ if Contains (Pragmas_Seen, Prag) then
+ return;
+ end if;
- pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc));
+ -- Extract arguments of the Default_Initial_Condition pragma
- Replace_References
- (Expr => Expr,
- Par_Typ => Par_Typ,
- Deriv_Typ => Deriv_Typ,
- Par_Obj => First_Formal (Par_Proc),
- Deriv_Obj => First_Formal (Deriv_Proc));
+ Prag_Expr_Arg := First (Pragma_Argument_Associations (Prag));
+ Prag_Expr := Expression_Copy (Prag_Expr_Arg);
- -- Once the DIC assertion expression is fully processed, add a check
- -- to the statements of the DIC procedure.
+ -- Pick up the implicit second argument of the pragma, which
+ -- indicates the type that the pragma applies to.
- Add_DIC_Check
- (DIC_Prag => DIC_Prag,
- DIC_Expr => Expr,
- Stmts => Stmts);
- end Add_Inherited_Tagged_DIC;
+ Prag_Typ_Arg := Next (Prag_Expr_Arg);
+ if Present (Prag_Typ_Arg) then
+ Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg);
+ else
+ Prag_Typ := Empty;
+ end if;
+
+ -- The pragma applies to the partial view of the parent type
+
+ if Present (Priv_Typ)
+ and then Present (Prag_Typ)
+ and then Entity (Prag_Typ) = Priv_Typ
+ then
+ Par_Typ := Priv_Typ;
+
+ -- The pragma applies to the full view of the parent type
+
+ elsif Present (Full_Typ)
+ and then Present (Prag_Typ)
+ and then Entity (Prag_Typ) = Full_Typ
+ then
+ Par_Typ := Full_Typ;
+
+ -- Otherwise the pragma does not belong to the parent type and
+ -- should not be considered.
+
+ else
+ return;
+ end if;
+
+ -- Substitute references in the DIC expression that are related
+ -- to the partial type with corresponding references related to
+ -- the derived type (call to Replace_References below).
+
+ Expr := New_Copy_Tree (Prag_Expr);
+
+ Par_Proc := Partial_DIC_Procedure (Par_Typ);
+
+ -- If there's not a partial DIC procedure (such as when a
+ -- full type doesn't have its own DIC, but is inherited from
+ -- a type with DIC), get the full DIC procedure.
+
+ if not Present (Par_Proc) then
+ Par_Proc := DIC_Procedure (Par_Typ);
+ end if;
+
+ Replace_References
+ (Expr => Expr,
+ Par_Typ => Par_Typ,
+ Deriv_Typ => Deriv_Typ,
+ Par_Obj => First_Formal (Par_Proc),
+ Deriv_Obj => Obj_Id);
+
+ -- Why are there different actions depending on whether T is
+ -- tagged? Can these be unified? ???
+
+ if Is_Tagged_Type (T) then
+ Add_Inherited_Tagged_DIC
+ (DIC_Prag => Prag,
+ Expr => Expr,
+ Stmts => Checks);
+
+ else
+ Add_Inherited_DIC
+ (DIC_Prag => Prag,
+ Par_Typ => Par_Typ,
+ Deriv_Typ => Deriv_Typ,
+ Stmts => Checks);
+ end if;
+
+ -- Leave as soon as we get a DIC pragma, since we'll visit
+ -- the pragmas of the parents, so will get to any "inherited"
+ -- pragmas that way.
+
+ return;
+ end if;
+
+ Next_Rep_Item (Prag);
+ end loop;
+ end Add_Inherited_DICs;
-----------------
-- Add_Own_DIC --
procedure Add_Own_DIC
(DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
+ Obj_Id : Entity_Id;
Stmts : in out List_Id)
is
DIC_Args : constant List_Id :=
DIC_Arg : constant Node_Id := First (DIC_Args);
DIC_Asp : constant Node_Id := Corresponding_Aspect (DIC_Prag);
DIC_Expr : constant Node_Id := Get_Pragma_Arg (DIC_Arg);
- DIC_Proc : constant Entity_Id := DIC_Procedure (DIC_Typ);
- Obj_Id : constant Entity_Id := First_Formal (DIC_Proc);
-- Local variables
Stmts => Stmts);
end Add_Own_DIC;
+ ---------------------
+ -- Add_Parent_DICs --
+ ---------------------
+
+ procedure Add_Parent_DICs
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id)
+ is
+ Dummy_1 : Entity_Id;
+ Dummy_2 : Entity_Id;
+
+ Curr_Typ : Entity_Id;
+ -- The entity of the current type being examined
+
+ Full_Typ : Entity_Id;
+ -- The full view of Par_Typ
+
+ Par_Typ : Entity_Id;
+ -- The entity of the parent type
+
+ Priv_Typ : Entity_Id;
+ -- The partial view of Par_Typ
+
+ begin
+ -- Climb the parent type chain
+
+ Curr_Typ := T;
+ loop
+ -- Do not consider subtypes, as they inherit the DICs from their
+ -- base types.
+
+ Par_Typ := Base_Type (Etype (Base_Type (Curr_Typ)));
+
+ -- Stop the climb once the root of the parent chain is
+ -- reached.
+
+ exit when Curr_Typ = Par_Typ;
+
+ -- Process the DICs of the parent type
+
+ Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2);
+
+ -- Only try to inherit a DIC pragma from the parent type Par_Typ
+ -- if it Has_Own_DIC pragma. The loop will proceed up the parent
+ -- chain to find all types that have their own DIC.
+
+ if Has_Own_DIC (Par_Typ) then
+ Add_Inherited_DICs
+ (T => T,
+ Priv_Typ => Priv_Typ,
+ Full_Typ => Full_Typ,
+ Obj_Id => Obj_Id,
+ Checks => Checks);
+ end if;
+
+ Curr_Typ := Par_Typ;
+ end loop;
+ end Add_Parent_DICs;
+
-- Local variables
Loc : constant Source_Ptr := Sloc (Typ);
Proc_Id : Entity_Id;
Stmts : List_Id := No_List;
- Build_Body : Boolean := False;
- -- Flag set when the type requires a DIC procedure body to be built
+ CRec_Typ : Entity_Id := Empty;
+ -- The corresponding record type of Full_Typ
+
+ Full_Typ : Entity_Id := Empty;
+ -- The full view of the working type
+
+ Obj_Id : Entity_Id := Empty;
+ -- The _object formal parameter of the invariant procedure
+
+ Part_Proc : Entity_Id := Empty;
+ -- The entity of the "partial" invariant procedure
+
+ Priv_Typ : Entity_Id := Empty;
+ -- The partial view of the working type
Work_Typ : Entity_Id;
-- The working type
goto Leave;
end if;
- -- The working type may lack a DIC procedure declaration. This may be
- -- due to several reasons:
+ -- Obtain both views of the type
+
+ Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy_1, CRec_Typ);
- -- * The working type's own DIC pragma does not contain a verifiable
- -- assertion expression. In this case there is no need to build a
- -- DIC procedure because there is nothing to check.
+ -- The caller requests a body for the partial DIC procedure
- -- * The working type derives from a parent type. In this case a DIC
- -- procedure should be built only when the inherited DIC pragma has
- -- a verifiable assertion expression.
+ if Partial_DIC then
+ Proc_Id := Partial_DIC_Procedure (Work_Typ);
- Proc_Id := DIC_Procedure (Work_Typ);
+ -- The "full" DIC procedure body was already created
- -- Build a DIC procedure declaration when the working type derives from
- -- a parent type.
+ -- Create a declaration for the "partial" DIC procedure if it
+ -- is not available.
+
+ if No (Proc_Id) then
+ Build_DIC_Procedure_Declaration
+ (Typ => Work_Typ,
+ Partial_DIC => True);
- if No (Proc_Id) then
- Build_DIC_Procedure_Declaration (Work_Typ);
- Proc_Id := DIC_Procedure (Work_Typ);
+ Proc_Id := Partial_DIC_Procedure (Work_Typ);
+ end if;
+
+ -- The caller requests a body for the "full" DIC procedure
+
+ else
+ Proc_Id := DIC_Procedure (Work_Typ);
+ Part_Proc := Partial_DIC_Procedure (Work_Typ);
+
+ -- Create a declaration for the "full" DIC procedure if it is
+ -- not available.
+
+ if No (Proc_Id) then
+ Build_DIC_Procedure_Declaration (Work_Typ);
+ Proc_Id := DIC_Procedure (Work_Typ);
+ end if;
end if;
-- At this point there should be a DIC procedure declaration
Push_Scope (Proc_Id);
Install_Formals (Proc_Id);
- -- The working type defines its own DIC pragma. Replace the current
- -- instance of the working type with the formal of the DIC procedure.
- -- Note that there is no need to consider inherited DIC pragmas from
- -- parent types because the working type's DIC pragma "hides" all
- -- inherited DIC pragmas.
+ Obj_Id := First_Formal (Proc_Id);
+ pragma Assert (Present (Obj_Id));
- if Has_Own_DIC (Work_Typ) then
- pragma Assert (DIC_Typ = Work_Typ);
+ -- The "partial" DIC procedure verifies the DICs of the partial view
+ -- only.
- Add_Own_DIC
- (DIC_Prag => DIC_Prag,
- DIC_Typ => DIC_Typ,
- Stmts => Stmts);
+ if Partial_DIC then
+ pragma Assert (Present (Priv_Typ));
+
+ if Has_Own_DIC (Work_Typ) then -- If we're testing this then maybe
+ Add_Own_DIC -- we shouldn't be calling Find_DIC_Typ above???
+ (DIC_Prag => DIC_Prag,
+ DIC_Typ => DIC_Typ, -- Should this just be Work_Typ???
+ Obj_Id => Obj_Id,
+ Stmts => Stmts);
+ end if;
- Build_Body := True;
+ -- Otherwise the "full" DIC procedure verifies the DICs of the full
+ -- view, well as DICs inherited from parent types. In addition, it
+ -- indirectly verifies the DICs of the partial view by calling the
+ -- "partial" DIC procedure.
- -- Otherwise the working type inherits a DIC pragma from a parent type.
- -- This processing is carried out when the type is frozen because the
- -- state of all parent discriminants is known at that point. Note that
- -- it is semantically sound to delay the creation of the DIC procedure
- -- body till the freeze point. If the type has a DIC pragma of its own,
- -- then the DIC procedure body would have already been constructed at
- -- the end of the visible declarations and all parent DIC pragmas are
- -- effectively "hidden" and irrelevant.
+ else
+ pragma Assert (Present (Full_Typ));
- elsif For_Freeze then
- pragma Assert (Has_Inherited_DIC (Work_Typ));
- pragma Assert (DIC_Typ /= Work_Typ);
+ -- Check the DIC of the partial view by calling the "partial" DIC
+ -- procedure, unless the partial DIC body is empty. Generate:
- -- The working type is tagged. The verification of the assertion
- -- expression is subject to the same semantics as class-wide pre-
- -- and postconditions.
+ -- <Work_Typ>Partial_DIC (_object);
+
+ if Present (Part_Proc) and then not Has_Null_Body (Part_Proc) then
+ Append_New_To (Stmts,
+ Make_Procedure_Call_Statement (Loc,
+ Name => New_Occurrence_Of (Part_Proc, Loc),
+ Parameter_Associations => New_List (
+ New_Occurrence_Of (Obj_Id, Loc))));
+ end if;
- if Is_Tagged_Type (Work_Typ) then
- Add_Inherited_Tagged_DIC
- (DIC_Prag => DIC_Prag,
- Par_Typ => DIC_Typ,
- Deriv_Typ => Work_Typ,
- Stmts => Stmts);
+ -- Derived subtypes do not have a partial view
- -- Otherwise the working type is not tagged. Verify the assertion
- -- expression of the inherited DIC pragma by directly calling the
- -- DIC procedure of the parent type.
+ if Present (Priv_Typ) then
- else
- Add_Inherited_DIC
- (DIC_Prag => DIC_Prag,
- Par_Typ => DIC_Typ,
- Deriv_Typ => Work_Typ,
- Stmts => Stmts);
+ -- The processing of the "full" DIC procedure intentionally
+ -- skips the partial view because a) this may result in changes of
+ -- visibility and b) lead to duplicate checks. However, when the
+ -- full view is the underlying full view of an untagged derived
+ -- type whose parent type is private, partial DICs appear on
+ -- the rep item chain of the partial view only.
+
+ -- package Pack_1 is
+ -- type Root ... is private;
+ -- private
+ -- <full view of Root>
+ -- end Pack_1;
+
+ -- with Pack_1;
+ -- package Pack_2 is
+ -- type Child is new Pack_1.Root with Type_DIC => ...;
+ -- <underlying full view of Child>
+ -- end Pack_2;
+
+ -- As a result, the processing of the full view must also consider
+ -- all DICs of the partial view.
+
+ if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then
+ null;
+
+ -- Otherwise the DICs of the partial view are ignored
+
+ else
+ -- Ignore the DICs of the partial view by eliminating the view
+
+ Priv_Typ := Empty;
+ end if;
end if;
- Build_Body := True;
+ -- Process inherited Default_Initial_Conditions for all parent types
+
+ Add_Parent_DICs (Work_Typ, Obj_Id, Stmts);
end if;
End_Scope;
- if Build_Body then
+ -- Produce an empty completing body in the following cases:
+ -- * Assertions are disabled
+ -- * The DIC Assertion_Policy is Ignore
- -- Produce an empty completing body in the following cases:
- -- * Assertions are disabled
- -- * The DIC Assertion_Policy is Ignore
+ if No (Stmts) then
+ Stmts := New_List (Make_Null_Statement (Loc));
+ end if;
- if No (Stmts) then
- Stmts := New_List (Make_Null_Statement (Loc));
- end if;
+ -- Generate:
+ -- procedure <Work_Typ>DIC (_object : <Work_Typ>) is
+ -- begin
+ -- <Stmts>
+ -- end <Work_Typ>DIC;
- -- Generate:
- -- procedure <Work_Typ>DIC (_object : <Work_Typ>) is
- -- begin
- -- <Stmts>
- -- end <Work_Typ>DIC;
-
- Proc_Body :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Copy_Subprogram_Spec (Parent (Proc_Id)),
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Stmts));
- Proc_Body_Id := Defining_Entity (Proc_Body);
-
- -- Perform minor decoration in case the body is not analyzed
-
- Set_Ekind (Proc_Body_Id, E_Subprogram_Body);
- Set_Etype (Proc_Body_Id, Standard_Void_Type);
- Set_Scope (Proc_Body_Id, Current_Scope);
- Set_SPARK_Pragma (Proc_Body_Id, SPARK_Pragma (Proc_Id));
- Set_SPARK_Pragma_Inherited
- (Proc_Body_Id, SPARK_Pragma_Inherited (Proc_Id));
-
- -- Link both spec and body to avoid generating duplicates
-
- Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
- Set_Corresponding_Spec (Proc_Body, Proc_Id);
-
- -- The body should not be inserted into the tree when the context
- -- is a generic unit because it is not part of the template.
- -- Note that the body must still be generated in order to resolve the
- -- DIC assertion expression.
-
- if Inside_A_Generic then
- null;
+ Proc_Body :=
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Copy_Subprogram_Spec (Parent (Proc_Id)),
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Stmts));
+ Proc_Body_Id := Defining_Entity (Proc_Body);
- -- Semi-insert the body into the tree for GNATprove by setting its
- -- Parent field. This allows for proper upstream tree traversals.
+ -- Perform minor decoration in case the body is not analyzed
- elsif GNATprove_Mode then
- Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
+ Set_Ekind (Proc_Body_Id, E_Subprogram_Body);
+ Set_Etype (Proc_Body_Id, Standard_Void_Type);
+ Set_Scope (Proc_Body_Id, Current_Scope);
+ Set_SPARK_Pragma (Proc_Body_Id, SPARK_Pragma (Proc_Id));
+ Set_SPARK_Pragma_Inherited
+ (Proc_Body_Id, SPARK_Pragma_Inherited (Proc_Id));
- -- Otherwise the body is part of the freezing actions of the working
- -- type.
+ -- Link both spec and body to avoid generating duplicates
- else
- Append_Freeze_Action (Work_Typ, Proc_Body);
- end if;
+ Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
+ Set_Corresponding_Spec (Proc_Body, Proc_Id);
+
+ -- The body should not be inserted into the tree when the context
+ -- is a generic unit because it is not part of the template.
+ -- Note that the body must still be generated in order to resolve the
+ -- DIC assertion expression.
+
+ if Inside_A_Generic then
+ null;
+
+ -- Semi-insert the body into the tree for GNATprove by setting its
+ -- Parent field. This allows for proper upstream tree traversals.
+
+ elsif GNATprove_Mode then
+ Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
+
+ -- Otherwise the body is part of the freezing actions of the working
+ -- type.
+
+ else
+ Append_Freeze_Action (Work_Typ, Proc_Body);
end if;
<<Leave>>
-- replaced by gotos which jump to the end of the routine and restore the
-- Ghost mode.
- procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is
+ procedure Build_DIC_Procedure_Declaration
+ (Typ : Entity_Id;
+ Partial_DIC : Boolean := False)
+ is
Loc : constant Source_Ptr := Sloc (Typ);
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
DIC_Typ : Entity_Id;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
+ Proc_Nam : Name_Id;
Typ_Decl : Node_Id;
CRec_Typ : Entity_Id;
if not Is_Verifiable_DIC_Pragma (DIC_Prag) then
goto Leave;
+ end if;
+
+ -- Nothing to do if the type already has a "partial" DIC procedure
+
+ if Partial_DIC then
+ if Present (Partial_DIC_Procedure (Work_Typ)) then
+ goto Leave;
+ end if;
- -- Nothing to do if the type already has a DIC procedure
+ -- Nothing to do if the type already has a "full" DIC procedure
elsif Present (DIC_Procedure (Work_Typ)) then
goto Leave;
end if;
+ -- The caller requests the declaration of the "partial" DIC procedure
+
+ if Partial_DIC then
+ Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_DIC");
+
+ -- Otherwise the caller requests the declaration of the "full" DIC
+ -- procedure.
+
+ else
+ Proc_Nam := New_External_Name (Chars (Work_Typ), "DIC");
+ end if;
+
Proc_Id :=
- Make_Defining_Identifier (Loc,
- Chars =>
- New_External_Name (Chars (Work_Typ), "Default_Initial_Condition"));
+ Make_Defining_Identifier (Loc, Chars => Proc_Nam);
-- Perform minor decoration in case the declaration is not analyzed
return
Present (Args)
+
+ -- If there are args, but the first arg is Empty, then treat the
+ -- pragma the same as having no args (there may be a second arg that
+ -- is an implicitly added type arg, and Empty is a placeholder).
+
+ and then Present (Get_Pragma_Arg (First (Args)))
+
and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null;
end Is_Verifiable_DIC_Pragma;
-- type is frozen.
function Build_DIC_Call
- (Loc : Source_Ptr;
- Obj_Id : Entity_Id;
- Typ : Entity_Id) return Node_Id;
- -- Build a call to the DIC procedure of type Typ with Obj_Id as the actual
+ (Loc : Source_Ptr;
+ Obj_Name : Node_Id;
+ Typ : Entity_Id) return Node_Id;
+ -- Build a call to the DIC procedure for Typ with Obj_Name as the actual
-- parameter.
procedure Build_DIC_Procedure_Body
- (Typ : Entity_Id;
- For_Freeze : Boolean := False);
+ (Typ : Entity_Id;
+ Partial_DIC : Boolean := False);
-- Create the body of the procedure which verifies the assertion expression
- -- of pragma Default_Initial_Condition at run time. Flag For_Freeze should
- -- be set when the body is constructed as part of the freezing actions for
- -- Typ.
-
- procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id);
+ -- of pragma Default_Initial_Condition at run time. Partial_DIC indicates
+ -- that a partial DIC-checking procedure body should be built, for checking
+ -- a DIC associated with the type's partial view, and which will be called
+ -- by the main DIC procedure.
+
+ procedure Build_DIC_Procedure_Declaration
+ (Typ : Entity_Id;
+ Partial_DIC : Boolean := False);
-- Create the declaration of the procedure which verifies the assertion
- -- expression of pragma Default_Initial_Condition at run time.
+ -- expression of pragma Default_Initial_Condition at run time. Partial_DIC
+ -- indicates that a partial DIC-checking procedure should be declared,
+ -- for checking a DIC associated with the type's partial view, and which
+ -- will be called by the main DIC procedure.
procedure Build_Invariant_Procedure_Body
(Typ : Entity_Id;
--
-- This variable is updated as a side effect of function Get_Value.
- Box_Node : Node_Id := Empty;
- Is_Box_Present : Boolean := False;
- Others_Box : Natural := 0;
+ Box_Node : Node_Id := Empty;
+ Is_Box_Present : Boolean := False;
+ Is_Box_Init_By_Default : Boolean := False;
+ Others_Box : Natural := 0;
-- Ada 2005 (AI-287): Variables used in case of default initialization
-- to provide a functionality similar to Others_Etype. Box_Present
-- indicates that the component takes its default initialization;
Choices => Choice_List,
Expression => Expr,
Box_Present => Is_Box_Present));
+
+ -- If this association has a box for a component that is initialized
+ -- by default, then set flag on the new association to indicate that
+ -- the original association was for such a box-initialized component.
+
+ if Resolve_Record_Aggregate.Is_Box_Present
+ and then not Is_Box_Present
+ and then Is_Box_Init_By_Default -- ???
+ then
+ Set_Was_Default_Init_Box_Association (Last (Assoc_List));
+ end if;
end Add_Association;
-----------------------------
begin
Is_Box_Present := False;
+ Is_Box_Init_By_Default := False;
if No (From) then
return Empty;
Ctyp : constant Entity_Id := Etype (Component);
begin
+ -- Initially assume that the box is for a default-initialized
+ -- component and reset to False in cases where that's not true.
+
+ Is_Box_Init_By_Default := True;
+
-- If there is a default expression for the aggregate, copy
-- it into a new association. This copy must modify the scopes
-- of internal types that may be attached to the expression
and then Nkind (Parent (Component)) = N_Component_Declaration
and then Present (Expression (Parent (Component)))
then
+ -- If component declaration has an initialization expression
+ -- then this is not a case of default initialization.
+
+ Is_Box_Init_By_Default := False;
+
Expr :=
New_Copy_Tree_And_Copy_Dimensions
(Expression (Parent (Component)),
-- wrapped inside of a procedure at the freeze point of the
-- private type's full view.
+ -- A type entity argument is appended to facilitate inheriting
+ -- the aspect from parent types (see Build_DIC_Procedure_Body),
+ -- though that extra argument isn't documented for the pragma.
+
when Aspect_Default_Initial_Condition =>
Aitem := Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
+ Expression => Relocate_Node (Expr)),
+ Make_Pragma_Argument_Association (Sloc (Ent),
+ Expression => Ent)),
Pragma_Name =>
Name_Default_Initial_Condition);
procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id) is
begin
- -- Preanalyze and resolve the Default_Initial_Condition assertion
- -- expression at the end of the declarations to catch any errors.
-
- if Has_DIC (Typ) then
- Build_DIC_Procedure_Body (Typ);
- end if;
-
if Nkind (Context) = N_Package_Specification then
-- Preanalyze and resolve the class-wide invariants of an
Partial_Invariant => True);
end if;
- -- Preanalyze and resolve the invariants of a private type
- -- at the end of the visible declarations to catch potential
- -- errors. Inherited class-wide invariants are not included
- -- because they have already been resolved.
+ elsif Decls = Visible_Declarations (Context) then
+ -- Preanalyze and resolve the invariants of a private type
+ -- at the end of the visible declarations to catch potential
+ -- errors. Inherited class-wide invariants are not included
+ -- because they have already been resolved.
- elsif Decls = Visible_Declarations (Context)
- and then Ekind (Typ) in E_Limited_Private_Type
- | E_Private_Type
- | E_Record_Type_With_Private
- and then Has_Own_Invariants (Typ)
- then
- Build_Invariant_Procedure_Body
- (Typ => Typ,
- Partial_Invariant => True);
-
- -- Preanalyze and resolve the invariants of a private type's
- -- full view at the end of the private declarations to catch
- -- potential errors.
-
- elsif Decls = Private_Declarations (Context)
- and then (not Is_Private_Type (Typ)
- or else Present (Underlying_Full_View (Typ)))
- and then Has_Private_Declaration (Typ)
- and then Has_Invariants (Typ)
- then
- Build_Invariant_Procedure_Body (Typ);
+ if Ekind (Typ) in E_Limited_Private_Type
+ | E_Private_Type
+ | E_Record_Type_With_Private
+ and then Has_Own_Invariants (Typ)
+ then
+ Build_Invariant_Procedure_Body
+ (Typ => Typ,
+ Partial_Invariant => True);
+ end if;
+
+ -- Preanalyze and resolve the Default_Initial_Condition
+ -- assertion expression at the end of the declarations to
+ -- catch any errors.
+
+ if Ekind (Typ) in E_Limited_Private_Type
+ | E_Private_Type
+ | E_Record_Type_With_Private
+ and then Has_Own_DIC (Typ)
+ then
+ Build_DIC_Procedure_Body
+ (Typ => Typ,
+ Partial_DIC => True);
+ end if;
+
+ elsif Decls = Private_Declarations (Context) then
+
+ -- Preanalyze and resolve the invariants of a private type's
+ -- full view at the end of the private declarations to catch
+ -- potential errors.
+
+ if (not Is_Private_Type (Typ)
+ or else Present (Underlying_Full_View (Typ)))
+ and then Has_Private_Declaration (Typ)
+ and then Has_Invariants (Typ)
+ then
+ Build_Invariant_Procedure_Body (Typ);
+ end if;
+
+ if (not Is_Private_Type (Typ)
+ or else Present (Underlying_Full_View (Typ)))
+ and then Has_Private_Declaration (Typ)
+ and then Has_DIC (Typ)
+ then
+ Build_DIC_Procedure_Body (Typ);
+ end if;
end if;
end if;
end Build_Assertion_Bodies_For_Type;
begin
GNAT_Pragma;
Check_No_Identifiers;
- Check_At_Most_N_Arguments (1);
+ Check_At_Most_N_Arguments (2); -- Accounts for implicit type arg
Typ := Empty;
Stmt := Prev (N);
Set_Has_Own_DIC (Typ);
+ -- A type entity argument is appended to facilitate inheriting the
+ -- aspect/pragma from parent types (see Build_DIC_Procedure_Body),
+ -- though that extra argument isn't documented for the pragma.
+
+ if not Present (Arg2) then
+ -- When the pragma has no arguments, create an argument with
+ -- the value Empty, so the type name argument can be appended
+ -- following it (since it's expected as the second argument).
+
+ if not Present (Arg1) then
+ Set_Pragma_Argument_Associations (N, New_List (
+ Make_Pragma_Argument_Association (Sloc (Typ),
+ Expression => Empty)));
+ end if;
+
+ Append_To
+ (Pragma_Argument_Associations (N),
+ Make_Pragma_Argument_Association (Sloc (Typ),
+ Expression => New_Occurrence_Of (Typ, Sloc (Typ))));
+ end if;
+
-- Chain the pragma on the rep item chain for further processing
Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
(Typ : Entity_Id;
From_Typ : Entity_Id)
is
- DIC_Proc : Entity_Id;
+ DIC_Proc : Entity_Id;
+ Partial_DIC_Proc : Entity_Id;
begin
if Present (Typ) and then Present (From_Typ) then
end if;
DIC_Proc := DIC_Procedure (From_Typ);
+ Partial_DIC_Proc := Partial_DIC_Procedure (From_Typ);
-- The setting of the attributes is intentionally conservative. This
-- prevents accidental clobbering of enabled attributes.
if Present (DIC_Proc) and then No (DIC_Procedure (Typ)) then
Set_DIC_Procedure (Typ, DIC_Proc);
end if;
+
+ if Present (Partial_DIC_Proc)
+ and then No (Partial_DIC_Procedure (Typ))
+ then
+ Set_Partial_DIC_Procedure (Typ, Partial_DIC_Proc);
+ end if;
end if;
end Propagate_DIC_Attributes;
return Flag2 (N);
end Was_Attribute_Reference;
+ function Was_Default_Init_Box_Association
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Component_Association);
+ return Flag14 (N);
+ end Was_Default_Init_Box_Association;
+
function Was_Expression_Function
(N : Node_Id) return Boolean is
begin
Set_Flag2 (N, Val);
end Set_Was_Attribute_Reference;
+ procedure Set_Was_Default_Init_Box_Association
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Component_Association);
+ Set_Flag14 (N, Val);
+ end Set_Was_Default_Init_Box_Association;
+
procedure Set_Was_Expression_Function
(N : Node_Id; Val : Boolean := True) is
begin
-- instantiation prologue renames these attributes, and expansion later
-- converts them into subprogram bodies.
+ -- Was_Default_Init_Box_Association (Flag14-Sem)
+ -- Present in N_Component_Association. Set to True if the original source
+ -- is an aggregate component association with a box (<>) for a component
+ -- that is initialized by default.
+
-- Was_Expression_Function (Flag18-Sem)
-- Present in N_Subprogram_Body. True if the original source had an
-- N_Expression_Function, which was converted to the N_Subprogram_Body
-- Expression (Node3) (empty if Box_Present)
-- Loop_Actions (List5-Sem)
-- Box_Present (Flag15)
+ -- Was_Default_Init_Box_Association (Flag14)
-- Inherited_Discriminant (Flag13)
-- Note: this structure is used for both record component associations
-- list of selector names in the record aggregate case, or a list of
-- discrete choices in the array aggregate case or an N_Others_Choice
-- node (which appears as a singleton list). Box_Present gives support
- -- to Ada 2005 (AI-287).
+ -- to Ada 2005 (AI-287). Was_Default_Init_Box_Association is used for
+ -- determining the need for Default_Initial_Condition check on component
+ -- associations with a box.
----------------------------------
-- 4.3.1 Component Choice List --
function Was_Attribute_Reference
(N : Node_Id) return Boolean; -- Flag2
+ function Was_Default_Init_Box_Association
+ (N : Node_Id) return Boolean; -- Flag14
+
function Was_Expression_Function
(N : Node_Id) return Boolean; -- Flag18
procedure Set_Was_Attribute_Reference
(N : Node_Id; Val : Boolean := True); -- Flag2
+ procedure Set_Was_Default_Init_Box_Association
+ (N : Node_Id; Val : Boolean := True); -- Flag14
+
procedure Set_Was_Expression_Function
(N : Node_Id; Val : Boolean := True); -- Flag18
pragma Inline (Visible_Declarations);
pragma Inline (Used_Operations);
pragma Inline (Was_Attribute_Reference);
+ pragma Inline (Was_Default_Init_Box_Association);
pragma Inline (Was_Expression_Function);
pragma Inline (Was_Originally_Stub);
pragma Inline (Set_Variants);
pragma Inline (Set_Visible_Declarations);
pragma Inline (Set_Was_Attribute_Reference);
+ pragma Inline (Set_Was_Default_Init_Box_Association);
pragma Inline (Set_Was_Expression_Function);
pragma Inline (Set_Was_Originally_Stub);
projects / gcc.git / commitdiff