| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT COMPILER COMPONENTS -- |
| -- -- |
| -- E X P _ U T I L -- |
| -- -- |
| -- B o d y -- |
| -- -- |
| -- Copyright (C) 1992-2022, Free Software Foundation, Inc. -- |
| -- -- |
| -- GNAT is free software; you can redistribute it and/or modify it under -- |
| -- terms of the GNU General Public License as published by the Free Soft- -- |
| -- ware Foundation; either version 3, or (at your option) any later ver- -- |
| -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
| -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- |
| -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- |
| -- for more details. You should have received a copy of the GNU General -- |
| -- Public License distributed with GNAT; see file COPYING3. If not, go to -- |
| -- http://www.gnu.org/licenses for a complete copy of the license. -- |
| -- -- |
| -- GNAT was originally developed by the GNAT team at New York University. -- |
| -- Extensive contributions were provided by Ada Core Technologies Inc. -- |
| -- -- |
| ------------------------------------------------------------------------------ |
| |
| with Aspects; use Aspects; |
| with Atree; use Atree; |
| with Casing; use Casing; |
| with Checks; use Checks; |
| with Debug; use Debug; |
| with Einfo; use Einfo; |
| with Einfo.Entities; use Einfo.Entities; |
| with Einfo.Utils; use Einfo.Utils; |
| with Elists; use Elists; |
| with Errout; use Errout; |
| with Exp_Aggr; use Exp_Aggr; |
| with Exp_Ch6; use Exp_Ch6; |
| with Exp_Ch7; use Exp_Ch7; |
| with Exp_Ch11; use Exp_Ch11; |
| with Freeze; use Freeze; |
| with Ghost; use Ghost; |
| with Inline; use Inline; |
| with Itypes; use Itypes; |
| with Lib; use Lib; |
| with Nlists; use Nlists; |
| with Nmake; use Nmake; |
| with Opt; use Opt; |
| with Restrict; use Restrict; |
| with Rident; use Rident; |
| with Sem; use Sem; |
| with Sem_Aux; use Sem_Aux; |
| with Sem_Ch3; use Sem_Ch3; |
| with Sem_Ch6; use Sem_Ch6; |
| with Sem_Ch8; use Sem_Ch8; |
| with Sem_Ch12; use Sem_Ch12; |
| with Sem_Ch13; use Sem_Ch13; |
| with Sem_Disp; use Sem_Disp; |
| with Sem_Elab; use Sem_Elab; |
| 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 Sinfo.Utils; use Sinfo.Utils; |
| with Snames; use Snames; |
| with Stand; use Stand; |
| with Stringt; use Stringt; |
| with Tbuild; use Tbuild; |
| with Ttypes; use Ttypes; |
| with Validsw; use Validsw; |
| |
| with GNAT.HTable; |
| package body Exp_Util is |
| |
| --------------------------------------------------------- |
| -- Handling of inherited class-wide pre/postconditions -- |
| --------------------------------------------------------- |
| |
| -- Following AI12-0113, the expression for a class-wide condition is |
| -- transformed for a subprogram that inherits it, by replacing calls |
| -- to primitive operations of the original controlling type into the |
| -- corresponding overriding operations of the derived type. The following |
| -- hash table manages this mapping, and is expanded on demand whenever |
| -- such inherited expression needs to be constructed. |
| |
| -- The mapping is also used to check whether an inherited operation has |
| -- a condition that depends on overridden operations. For such an |
| -- operation we must create a wrapper that is then treated as a normal |
| -- overriding. In SPARK mode such operations are illegal. |
| |
| -- For a given root type there may be several type extensions with their |
| -- own overriding operations, so at various times a given operation of |
| -- the root will be mapped into different overridings. The root type is |
| -- also mapped into the current type extension to indicate that its |
| -- operations are mapped into the overriding operations of that current |
| -- type extension. |
| |
| -- The contents of the map are as follows: |
| |
| -- Key Value |
| |
| -- Discriminant (Entity_Id) Discriminant (Entity_Id) |
| -- Discriminant (Entity_Id) Non-discriminant name (Entity_Id) |
| -- Discriminant (Entity_Id) Expression (Node_Id) |
| -- Primitive subprogram (Entity_Id) Primitive subprogram (Entity_Id) |
| -- Type (Entity_Id) Type (Entity_Id) |
| |
| Type_Map_Size : constant := 511; |
| |
| subtype Type_Map_Header is Integer range 0 .. Type_Map_Size - 1; |
| function Type_Map_Hash (Id : Entity_Id) return Type_Map_Header; |
| |
| package Type_Map is new GNAT.HTable.Simple_HTable |
| (Header_Num => Type_Map_Header, |
| Key => Entity_Id, |
| Element => Node_Or_Entity_Id, |
| No_element => Empty, |
| Hash => Type_Map_Hash, |
| Equal => "="); |
| |
| ----------------------- |
| -- Local Subprograms -- |
| ----------------------- |
| |
| function Build_Task_Array_Image |
| (Loc : Source_Ptr; |
| Id_Ref : Node_Id; |
| A_Type : Entity_Id; |
| Dyn : Boolean := False) return Node_Id; |
| -- Build function to generate the image string for a task that is an array |
| -- component, concatenating the images of each index. To avoid storage |
| -- leaks, the string is built with successive slice assignments. The flag |
| -- Dyn indicates whether this is called for the initialization procedure of |
| -- an array of tasks, or for the name of a dynamically created task that is |
| -- assigned to an indexed component. |
| |
| function Build_Task_Image_Function |
| (Loc : Source_Ptr; |
| Decls : List_Id; |
| Stats : List_Id; |
| Res : Entity_Id) return Node_Id; |
| -- Common processing for Task_Array_Image and Task_Record_Image. Build |
| -- function body that computes image. |
| |
| procedure Build_Task_Image_Prefix |
| (Loc : Source_Ptr; |
| Len : out Entity_Id; |
| Res : out Entity_Id; |
| Pos : out Entity_Id; |
| Prefix : Entity_Id; |
| Sum : Node_Id; |
| Decls : List_Id; |
| Stats : List_Id); |
| -- Common processing for Task_Array_Image and Task_Record_Image. Create |
| -- local variables and assign prefix of name to result string. |
| |
| function Build_Task_Record_Image |
| (Loc : Source_Ptr; |
| Id_Ref : Node_Id; |
| Dyn : Boolean := False) return Node_Id; |
| -- Build function to generate the image string for a task that is a record |
| -- component. Concatenate name of variable with that of selector. The flag |
| -- Dyn indicates whether this is called for the initialization procedure of |
| -- record with task components, or for a dynamically created task that is |
| -- assigned to a selected component. |
| |
| procedure Evaluate_Slice_Bounds (Slice : Node_Id); |
| -- Force evaluation of bounds of a slice, which may be given by a range |
| -- or by a subtype indication with or without a constraint. |
| |
| function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean; |
| -- Determine whether pragma Default_Initial_Condition denoted by Prag has |
| -- an assertion expression that should be verified at run time. |
| |
| function Is_Uninitialized_Aggregate |
| (Exp : Node_Id; |
| T : Entity_Id) return Boolean; |
| -- Determine whether an array aggregate used in an object declaration |
| -- is uninitialized, when the aggregate is declared with a box and |
| -- the component type has no default value. Such an aggregate can be |
| -- optimized away to prevent the copying of uninitialized data, and |
| -- the bounds of the aggregate can be propagated directly to the |
| -- object declaration. |
| |
| function Make_CW_Equivalent_Type |
| (T : Entity_Id; |
| E : Node_Id) return Entity_Id; |
| -- T is a class-wide type entity, E is the initial expression node that |
| -- constrains T in case such as: " X: T := E" or "new T'(E)". This function |
| -- returns the entity of the Equivalent type and inserts on the fly the |
| -- necessary declaration such as: |
| -- |
| -- type anon is record |
| -- _parent : Root_Type (T); constrained with E discriminants (if any) |
| -- Extension : String (1 .. expr to match size of E); |
| -- end record; |
| -- |
| -- This record is compatible with any object of the class of T thanks to |
| -- the first field and has the same size as E thanks to the second. |
| |
| function Make_Literal_Range |
| (Loc : Source_Ptr; |
| Literal_Typ : Entity_Id) return Node_Id; |
| -- Produce a Range node whose bounds are: |
| -- Low_Bound (Literal_Type) .. |
| -- Low_Bound (Literal_Type) + (Length (Literal_Typ) - 1) |
| -- this is used for expanding declarations like X : String := "sdfgdfg"; |
| -- |
| -- If the index type of the target array is not integer, we generate: |
| -- Low_Bound (Literal_Type) .. |
| -- Literal_Type'Val |
| -- (Literal_Type'Pos (Low_Bound (Literal_Type)) |
| -- + (Length (Literal_Typ) -1)) |
| |
| function Make_Non_Empty_Check |
| (Loc : Source_Ptr; |
| N : Node_Id) return Node_Id; |
| -- Produce a boolean expression checking that the unidimensional array |
| -- node N is not empty. |
| |
| function New_Class_Wide_Subtype |
| (CW_Typ : Entity_Id; |
| N : Node_Id) return Entity_Id; |
| -- Create an implicit subtype of CW_Typ attached to node N |
| |
| function Requires_Cleanup_Actions |
| (L : List_Id; |
| Lib_Level : Boolean; |
| Nested_Constructs : Boolean) return Boolean; |
| -- Given a list L, determine whether it contains one of the following: |
| -- |
| -- 1) controlled objects |
| -- 2) library-level tagged types |
| -- |
| -- Lib_Level is True when the list comes from a construct at the library |
| -- level, and False otherwise. Nested_Constructs is True when any nested |
| -- packages declared in L must be processed, and False otherwise. |
| |
| function Side_Effect_Free_Attribute (Name : Name_Id) return Boolean; |
| -- Return True if the evaluation of the given attribute is considered |
| -- side-effect free, independently of its prefix and expressions. |
| |
| ------------------------------------- |
| -- Activate_Atomic_Synchronization -- |
| ------------------------------------- |
| |
| procedure Activate_Atomic_Synchronization (N : Node_Id) is |
| Msg_Node : Node_Id; |
| |
| begin |
| case Nkind (Parent (N)) is |
| |
| -- Check for cases of appearing in the prefix of a construct where we |
| -- don't need atomic synchronization for this kind of usage. |
| |
| when |
| -- Nothing to do if we are the prefix of an attribute, since we |
| -- do not want an atomic sync operation for things like 'Size. |
| |
| N_Attribute_Reference |
| |
| -- The N_Reference node is like an attribute |
| |
| | N_Reference |
| |
| -- Nothing to do for a reference to a component (or components) |
| -- of a composite object. Only reads and updates of the object |
| -- as a whole require atomic synchronization (RM C.6 (15)). |
| |
| | N_Indexed_Component |
| | N_Selected_Component |
| | N_Slice |
| => |
| -- For all the above cases, nothing to do if we are the prefix |
| |
| if Prefix (Parent (N)) = N then |
| return; |
| end if; |
| |
| when others => |
| null; |
| end case; |
| |
| -- Nothing to do for the identifier in an object renaming declaration, |
| -- the renaming itself does not need atomic synchronization. |
| |
| if Nkind (Parent (N)) = N_Object_Renaming_Declaration then |
| return; |
| end if; |
| |
| -- Go ahead and set the flag |
| |
| Set_Atomic_Sync_Required (N); |
| |
| -- Generate info message if requested |
| |
| if Warn_On_Atomic_Synchronization then |
| case Nkind (N) is |
| when N_Identifier => |
| Msg_Node := N; |
| |
| when N_Expanded_Name |
| | N_Selected_Component |
| => |
| Msg_Node := Selector_Name (N); |
| |
| when N_Explicit_Dereference |
| | N_Indexed_Component |
| => |
| Msg_Node := Empty; |
| |
| when others => |
| pragma Assert (False); |
| return; |
| end case; |
| |
| if Present (Msg_Node) then |
| Error_Msg_N |
| ("info: atomic synchronization set for &?.n?", Msg_Node); |
| else |
| Error_Msg_N |
| ("info: atomic synchronization set?.n?", N); |
| end if; |
| end if; |
| end Activate_Atomic_Synchronization; |
| |
| ---------------------- |
| -- Adjust_Condition -- |
| ---------------------- |
| |
| procedure Adjust_Condition (N : Node_Id) is |
| begin |
| if No (N) then |
| return; |
| end if; |
| |
| declare |
| Loc : constant Source_Ptr := Sloc (N); |
| T : constant Entity_Id := Etype (N); |
| |
| begin |
| -- Defend against a call where the argument has no type, or has a |
| -- type that is not Boolean. This can occur because of prior errors. |
| |
| if No (T) or else not Is_Boolean_Type (T) then |
| return; |
| end if; |
| |
| -- Apply validity checking if needed |
| |
| if Validity_Checks_On and Validity_Check_Tests then |
| Ensure_Valid (N); |
| end if; |
| |
| -- Immediate return if standard boolean, the most common case, |
| -- where nothing needs to be done. |
| |
| if Base_Type (T) = Standard_Boolean then |
| return; |
| end if; |
| |
| -- Case of zero/nonzero semantics or nonstandard enumeration |
| -- representation. In each case, we rewrite the node as: |
| |
| -- ityp!(N) /= False'Enum_Rep |
| |
| -- where ityp is an integer type with large enough size to hold any |
| -- value of type T. |
| |
| if Nonzero_Is_True (T) or else Has_Non_Standard_Rep (T) then |
| Rewrite (N, |
| Make_Op_Ne (Loc, |
| Left_Opnd => |
| Unchecked_Convert_To |
| (Integer_Type_For (Esize (T), Uns => False), N), |
| Right_Opnd => |
| Make_Attribute_Reference (Loc, |
| Attribute_Name => Name_Enum_Rep, |
| Prefix => |
| New_Occurrence_Of (First_Literal (T), Loc)))); |
| Analyze_And_Resolve (N, Standard_Boolean); |
| |
| else |
| Rewrite (N, Convert_To (Standard_Boolean, N)); |
| Analyze_And_Resolve (N, Standard_Boolean); |
| end if; |
| end; |
| end Adjust_Condition; |
| |
| ------------------------ |
| -- Adjust_Result_Type -- |
| ------------------------ |
| |
| procedure Adjust_Result_Type (N : Node_Id; T : Entity_Id) is |
| begin |
| -- Ignore call if current type is not Standard.Boolean |
| |
| if Etype (N) /= Standard_Boolean then |
| return; |
| end if; |
| |
| -- If result is already of correct type, nothing to do. Note that |
| -- this will get the most common case where everything has a type |
| -- of Standard.Boolean. |
| |
| if Base_Type (T) = Standard_Boolean then |
| return; |
| |
| else |
| declare |
| KP : constant Node_Kind := Nkind (Parent (N)); |
| |
| begin |
| -- If result is to be used as a Condition in the syntax, no need |
| -- to convert it back, since if it was changed to Standard.Boolean |
| -- using Adjust_Condition, that is just fine for this usage. |
| |
| if KP in N_Raise_xxx_Error or else KP in N_Has_Condition then |
| return; |
| |
| -- If result is an operand of another logical operation, no need |
| -- to reset its type, since Standard.Boolean is just fine, and |
| -- such operations always do Adjust_Condition on their operands. |
| |
| elsif KP in N_Op_Boolean |
| or else KP in N_Short_Circuit |
| or else KP = N_Op_Not |
| then |
| return; |
| |
| -- Otherwise we perform a conversion from the current type, which |
| -- must be Standard.Boolean, to the desired type. Use the base |
| -- type to prevent spurious constraint checks that are extraneous |
| -- to the transformation. The type and its base have the same |
| -- representation, standard or otherwise. |
| |
| else |
| Set_Analyzed (N); |
| Rewrite (N, Convert_To (Base_Type (T), N)); |
| Analyze_And_Resolve (N, Base_Type (T)); |
| end if; |
| end; |
| end if; |
| end Adjust_Result_Type; |
| |
| -------------------------- |
| -- Append_Freeze_Action -- |
| -------------------------- |
| |
| procedure Append_Freeze_Action (T : Entity_Id; N : Node_Id) is |
| Fnode : Node_Id; |
| |
| begin |
| Ensure_Freeze_Node (T); |
| Fnode := Freeze_Node (T); |
| |
| if No (Actions (Fnode)) then |
| Set_Actions (Fnode, New_List (N)); |
| else |
| Append (N, Actions (Fnode)); |
| end if; |
| end Append_Freeze_Action; |
| |
| --------------------------- |
| -- Append_Freeze_Actions -- |
| --------------------------- |
| |
| procedure Append_Freeze_Actions (T : Entity_Id; L : List_Id) is |
| Fnode : Node_Id; |
| |
| begin |
| if No (L) then |
| return; |
| end if; |
| |
| Ensure_Freeze_Node (T); |
| Fnode := Freeze_Node (T); |
| |
| if No (Actions (Fnode)) then |
| Set_Actions (Fnode, L); |
| else |
| Append_List (L, Actions (Fnode)); |
| end if; |
| end Append_Freeze_Actions; |
| |
| ---------------------------------------- |
| -- Attribute_Constrained_Static_Value -- |
| ---------------------------------------- |
| |
| function Attribute_Constrained_Static_Value (Pref : Node_Id) return Boolean |
| is |
| Ptyp : constant Entity_Id := Etype (Pref); |
| Formal_Ent : constant Entity_Id := Param_Entity (Pref); |
| |
| function Is_Constrained_Aliased_View (Obj : Node_Id) return Boolean; |
| -- Ada 2005 (AI-363): Returns True if the object name Obj denotes a |
| -- view of an aliased object whose subtype is constrained. |
| |
| --------------------------------- |
| -- Is_Constrained_Aliased_View -- |
| --------------------------------- |
| |
| function Is_Constrained_Aliased_View (Obj : Node_Id) return Boolean is |
| E : Entity_Id; |
| |
| begin |
| if Is_Entity_Name (Obj) then |
| E := Entity (Obj); |
| |
| if Present (Renamed_Object (E)) then |
| return Is_Constrained_Aliased_View (Renamed_Object (E)); |
| else |
| return Is_Aliased (E) and then Is_Constrained (Etype (E)); |
| end if; |
| |
| else |
| return Is_Aliased_View (Obj) |
| and then |
| (Is_Constrained (Etype (Obj)) |
| or else |
| (Nkind (Obj) = N_Explicit_Dereference |
| and then |
| not Object_Type_Has_Constrained_Partial_View |
| (Typ => Base_Type (Etype (Obj)), |
| Scop => Current_Scope))); |
| end if; |
| end Is_Constrained_Aliased_View; |
| |
| -- Start of processing for Attribute_Constrained_Static_Value |
| |
| begin |
| -- We are in a case where the attribute is known statically, and |
| -- implicit dereferences have been rewritten. |
| |
| pragma Assert |
| (not (Present (Formal_Ent) |
| and then Ekind (Formal_Ent) /= E_Constant |
| and then Present (Extra_Constrained (Formal_Ent))) |
| and then |
| not (Is_Access_Type (Etype (Pref)) |
| and then (not Is_Entity_Name (Pref) |
| or else Is_Object (Entity (Pref)))) |
| and then |
| not (Nkind (Pref) = N_Identifier |
| and then Ekind (Entity (Pref)) = E_Variable |
| and then Present (Extra_Constrained (Entity (Pref))))); |
| |
| if Is_Entity_Name (Pref) then |
| declare |
| Ent : constant Entity_Id := Entity (Pref); |
| Res : Boolean; |
| |
| begin |
| -- (RM J.4) obsolescent cases |
| |
| if Is_Type (Ent) then |
| |
| -- Private type |
| |
| if Is_Private_Type (Ent) then |
| Res := not Has_Discriminants (Ent) |
| or else Is_Constrained (Ent); |
| |
| -- It not a private type, must be a generic actual type |
| -- that corresponded to a private type. We know that this |
| -- correspondence holds, since otherwise the reference |
| -- within the generic template would have been illegal. |
| |
| else |
| if Is_Composite_Type (Underlying_Type (Ent)) then |
| Res := Is_Constrained (Ent); |
| else |
| Res := True; |
| end if; |
| end if; |
| |
| else |
| |
| -- If the prefix is not a variable or is aliased, then |
| -- definitely true; if it's a formal parameter without an |
| -- associated extra formal, then treat it as constrained. |
| |
| -- Ada 2005 (AI-363): An aliased prefix must be known to be |
| -- constrained in order to set the attribute to True. |
| |
| if not Is_Variable (Pref) |
| or else Present (Formal_Ent) |
| or else (Ada_Version < Ada_2005 |
| and then Is_Aliased_View (Pref)) |
| or else (Ada_Version >= Ada_2005 |
| and then Is_Constrained_Aliased_View (Pref)) |
| then |
| Res := True; |
| |
| -- Variable case, look at type to see if it is constrained. |
| -- Note that the one case where this is not accurate (the |
| -- procedure formal case), has been handled above. |
| |
| -- We use the Underlying_Type here (and below) in case the |
| -- type is private without discriminants, but the full type |
| -- has discriminants. This case is illegal, but we generate |
| -- it internally for passing to the Extra_Constrained |
| -- parameter. |
| |
| else |
| -- In Ada 2012, test for case of a limited tagged type, |
| -- in which case the attribute is always required to |
| -- return True. The underlying type is tested, to make |
| -- sure we also return True for cases where there is an |
| -- unconstrained object with an untagged limited partial |
| -- view which has defaulted discriminants (such objects |
| -- always produce a False in earlier versions of |
| -- Ada). (Ada 2012: AI05-0214) |
| |
| Res := |
| Is_Constrained (Underlying_Type (Etype (Ent))) |
| or else |
| (Ada_Version >= Ada_2012 |
| and then Is_Tagged_Type (Underlying_Type (Ptyp)) |
| and then Is_Limited_Type (Ptyp)); |
| end if; |
| end if; |
| |
| return Res; |
| end; |
| |
| -- Prefix is not an entity name. These are also cases where we can |
| -- always tell at compile time by looking at the form and type of the |
| -- prefix. If an explicit dereference of an object with constrained |
| -- partial view, this is unconstrained (Ada 2005: AI95-0363). If the |
| -- underlying type is a limited tagged type, then Constrained is |
| -- required to always return True (Ada 2012: AI05-0214). |
| |
| else |
| return not Is_Variable (Pref) |
| or else |
| (Nkind (Pref) = N_Explicit_Dereference |
| and then |
| not Object_Type_Has_Constrained_Partial_View |
| (Typ => Base_Type (Ptyp), |
| Scop => Current_Scope)) |
| or else Is_Constrained (Underlying_Type (Ptyp)) |
| or else (Ada_Version >= Ada_2012 |
| and then Is_Tagged_Type (Underlying_Type (Ptyp)) |
| and then Is_Limited_Type (Ptyp)); |
| end if; |
| end Attribute_Constrained_Static_Value; |
| |
| ------------------------------------ |
| -- Build_Allocate_Deallocate_Proc -- |
| ------------------------------------ |
| |
| procedure Build_Allocate_Deallocate_Proc |
| (N : Node_Id; |
| Is_Allocate : Boolean) |
| is |
| function Find_Object (E : Node_Id) return Node_Id; |
| -- Given an arbitrary expression of an allocator, try to find an object |
| -- reference in it, otherwise return the original expression. |
| |
| function Is_Allocate_Deallocate_Proc (Subp : Entity_Id) return Boolean; |
| -- Determine whether subprogram Subp denotes a custom allocate or |
| -- deallocate. |
| |
| ----------------- |
| -- Find_Object -- |
| ----------------- |
| |
| function Find_Object (E : Node_Id) return Node_Id is |
| Expr : Node_Id; |
| |
| begin |
| pragma Assert (Is_Allocate); |
| |
| Expr := E; |
| loop |
| if Nkind (Expr) = N_Explicit_Dereference then |
| Expr := Prefix (Expr); |
| |
| elsif Nkind (Expr) = N_Qualified_Expression then |
| Expr := Expression (Expr); |
| |
| elsif Nkind (Expr) = N_Unchecked_Type_Conversion then |
| |
| -- When interface class-wide types are involved in allocation, |
| -- the expander introduces several levels of address arithmetic |
| -- to perform dispatch table displacement. In this scenario the |
| -- object appears as: |
| |
| -- Tag_Ptr (Base_Address (<object>'Address)) |
| |
| -- Detect this case and utilize the whole expression as the |
| -- "object" since it now points to the proper dispatch table. |
| |
| if Is_RTE (Etype (Expr), RE_Tag_Ptr) then |
| exit; |
| |
| -- Continue to strip the object |
| |
| else |
| Expr := Expression (Expr); |
| end if; |
| |
| else |
| exit; |
| end if; |
| end loop; |
| |
| return Expr; |
| end Find_Object; |
| |
| --------------------------------- |
| -- Is_Allocate_Deallocate_Proc -- |
| --------------------------------- |
| |
| function Is_Allocate_Deallocate_Proc (Subp : Entity_Id) return Boolean is |
| begin |
| -- Look for a subprogram body with only one statement which is a |
| -- call to Allocate_Any_Controlled / Deallocate_Any_Controlled. |
| |
| if Ekind (Subp) = E_Procedure |
| and then Nkind (Parent (Parent (Subp))) = N_Subprogram_Body |
| then |
| declare |
| HSS : constant Node_Id := |
| Handled_Statement_Sequence (Parent (Parent (Subp))); |
| Proc : Entity_Id; |
| |
| begin |
| if Present (Statements (HSS)) |
| and then Nkind (First (Statements (HSS))) = |
| N_Procedure_Call_Statement |
| then |
| Proc := Entity (Name (First (Statements (HSS)))); |
| |
| return |
| Is_RTE (Proc, RE_Allocate_Any_Controlled) |
| or else Is_RTE (Proc, RE_Deallocate_Any_Controlled); |
| end if; |
| end; |
| end if; |
| |
| return False; |
| end Is_Allocate_Deallocate_Proc; |
| |
| -- Local variables |
| |
| Desig_Typ : Entity_Id; |
| Expr : Node_Id; |
| Needs_Fin : Boolean; |
| Pool_Id : Entity_Id; |
| Proc_To_Call : Node_Id := Empty; |
| Ptr_Typ : Entity_Id; |
| Use_Secondary_Stack_Pool : Boolean; |
| |
| -- Start of processing for Build_Allocate_Deallocate_Proc |
| |
| begin |
| -- Obtain the attributes of the allocation / deallocation |
| |
| if Nkind (N) = N_Free_Statement then |
| Expr := Expression (N); |
| Ptr_Typ := Base_Type (Etype (Expr)); |
| Proc_To_Call := Procedure_To_Call (N); |
| |
| else |
| if Nkind (N) = N_Object_Declaration then |
| Expr := Expression (N); |
| else |
| Expr := N; |
| end if; |
| |
| -- In certain cases an allocator with a qualified expression may |
| -- be relocated and used as the initialization expression of a |
| -- temporary: |
| |
| -- before: |
| -- Obj : Ptr_Typ := new Desig_Typ'(...); |
| |
| -- after: |
| -- Tmp : Ptr_Typ := new Desig_Typ'(...); |
| -- Obj : Ptr_Typ := Tmp; |
| |
| -- Since the allocator is always marked as analyzed to avoid infinite |
| -- expansion, it will never be processed by this routine given that |
| -- the designated type needs finalization actions. Detect this case |
| -- and complete the expansion of the allocator. |
| |
| if Nkind (Expr) = N_Identifier |
| and then Nkind (Parent (Entity (Expr))) = N_Object_Declaration |
| and then Nkind (Expression (Parent (Entity (Expr)))) = N_Allocator |
| then |
| Build_Allocate_Deallocate_Proc (Parent (Entity (Expr)), True); |
| return; |
| end if; |
| |
| -- The allocator may have been rewritten into something else in which |
| -- case the expansion performed by this routine does not apply. |
| |
| if Nkind (Expr) /= N_Allocator then |
| return; |
| end if; |
| |
| Ptr_Typ := Base_Type (Etype (Expr)); |
| Proc_To_Call := Procedure_To_Call (Expr); |
| end if; |
| |
| Pool_Id := Associated_Storage_Pool (Ptr_Typ); |
| Desig_Typ := Available_View (Designated_Type (Ptr_Typ)); |
| |
| -- Handle concurrent types |
| |
| if Is_Concurrent_Type (Desig_Typ) |
| and then Present (Corresponding_Record_Type (Desig_Typ)) |
| then |
| Desig_Typ := Corresponding_Record_Type (Desig_Typ); |
| end if; |
| |
| Use_Secondary_Stack_Pool := |
| Is_RTE (Pool_Id, RE_SS_Pool) |
| or else (Nkind (Expr) = N_Allocator |
| and then Is_RTE (Storage_Pool (Expr), RE_SS_Pool)); |
| |
| -- Do not process allocations / deallocations without a pool |
| |
| if No (Pool_Id) then |
| return; |
| |
| -- Do not process allocations on / deallocations from the secondary |
| -- stack, except for access types used to implement indirect temps. |
| |
| elsif Use_Secondary_Stack_Pool |
| and then not Old_Attr_Util.Indirect_Temps |
| .Is_Access_Type_For_Indirect_Temp (Ptr_Typ) |
| then |
| return; |
| |
| -- Optimize the case where we are using the default Global_Pool_Object, |
| -- and we don't need the heavy finalization machinery. |
| |
| elsif Is_RTE (Pool_Id, RE_Global_Pool_Object) |
| and then not Needs_Finalization (Desig_Typ) |
| then |
| return; |
| |
| -- Do not replicate the machinery if the allocator / free has already |
| -- been expanded and has a custom Allocate / Deallocate. |
| |
| elsif Present (Proc_To_Call) |
| and then Is_Allocate_Deallocate_Proc (Proc_To_Call) |
| then |
| return; |
| end if; |
| |
| -- Finalization actions are required when the object to be allocated or |
| -- deallocated needs these actions and the associated access type is not |
| -- subject to pragma No_Heap_Finalization. |
| |
| Needs_Fin := |
| Needs_Finalization (Desig_Typ) |
| and then not No_Heap_Finalization (Ptr_Typ); |
| |
| if Needs_Fin then |
| |
| -- Do nothing if the access type may never allocate / deallocate |
| -- objects. |
| |
| if No_Pool_Assigned (Ptr_Typ) then |
| return; |
| end if; |
| |
| -- The allocation / deallocation of a controlled object must be |
| -- chained on / detached from a finalization master. |
| |
| pragma Assert (Present (Finalization_Master (Ptr_Typ))); |
| |
| -- The only other kind of allocation / deallocation supported by this |
| -- routine is on / from a subpool. |
| |
| elsif Nkind (Expr) = N_Allocator |
| and then No (Subpool_Handle_Name (Expr)) |
| then |
| return; |
| end if; |
| |
| declare |
| Loc : constant Source_Ptr := Sloc (N); |
| Addr_Id : constant Entity_Id := Make_Temporary (Loc, 'A'); |
| Alig_Id : constant Entity_Id := Make_Temporary (Loc, 'L'); |
| Proc_Id : constant Entity_Id := Make_Temporary (Loc, 'P'); |
| Size_Id : constant Entity_Id := Make_Temporary (Loc, 'S'); |
| |
| Actuals : List_Id; |
| Fin_Addr_Id : Entity_Id; |
| Fin_Mas_Act : Node_Id; |
| Fin_Mas_Id : Entity_Id; |
| Proc_To_Call : Entity_Id; |
| Subpool : Node_Id := Empty; |
| |
| begin |
| -- Step 1: Construct all the actuals for the call to library routine |
| -- Allocate_Any_Controlled / Deallocate_Any_Controlled. |
| |
| -- a) Storage pool |
| |
| Actuals := New_List (New_Occurrence_Of (Pool_Id, Loc)); |
| |
| if Is_Allocate then |
| |
| -- b) Subpool |
| |
| if Nkind (Expr) = N_Allocator then |
| Subpool := Subpool_Handle_Name (Expr); |
| end if; |
| |
| -- If a subpool is present it can be an arbitrary name, so make |
| -- the actual by copying the tree. |
| |
| if Present (Subpool) then |
| Append_To (Actuals, New_Copy_Tree (Subpool, New_Sloc => Loc)); |
| else |
| Append_To (Actuals, Make_Null (Loc)); |
| end if; |
| |
| -- c) Finalization master |
| |
| if Needs_Fin then |
| Fin_Mas_Id := Finalization_Master (Ptr_Typ); |
| Fin_Mas_Act := New_Occurrence_Of (Fin_Mas_Id, Loc); |
| |
| -- Handle the case where the master is actually a pointer to a |
| -- master. This case arises in build-in-place functions. |
| |
| if Is_Access_Type (Etype (Fin_Mas_Id)) then |
| Append_To (Actuals, Fin_Mas_Act); |
| else |
| Append_To (Actuals, |
| Make_Attribute_Reference (Loc, |
| Prefix => Fin_Mas_Act, |
| Attribute_Name => Name_Unrestricted_Access)); |
| end if; |
| else |
| Append_To (Actuals, Make_Null (Loc)); |
| end if; |
| |
| -- d) Finalize_Address |
| |
| -- Primitive Finalize_Address is never generated in CodePeer mode |
| -- since it contains an Unchecked_Conversion. |
| |
| if Needs_Fin and then not CodePeer_Mode then |
| Fin_Addr_Id := Finalize_Address (Desig_Typ); |
| pragma Assert (Present (Fin_Addr_Id)); |
| |
| Append_To (Actuals, |
| Make_Attribute_Reference (Loc, |
| Prefix => New_Occurrence_Of (Fin_Addr_Id, Loc), |
| Attribute_Name => Name_Unrestricted_Access)); |
| else |
| Append_To (Actuals, Make_Null (Loc)); |
| end if; |
| end if; |
| |
| -- e) Address |
| -- f) Storage_Size |
| -- g) Alignment |
| |
| Append_To (Actuals, New_Occurrence_Of (Addr_Id, Loc)); |
| Append_To (Actuals, New_Occurrence_Of (Size_Id, Loc)); |
| |
| if (Is_Allocate or else not Is_Class_Wide_Type (Desig_Typ)) |
| and then not Use_Secondary_Stack_Pool |
| then |
| Append_To (Actuals, New_Occurrence_Of (Alig_Id, Loc)); |
| |
| -- For deallocation of class-wide types we obtain the value of |
| -- alignment from the Type Specific Record of the deallocated object. |
| -- This is needed because the frontend expansion of class-wide types |
| -- into equivalent types confuses the back end. |
| |
| else |
| -- Generate: |
| -- Obj.all'Alignment |
| |
| -- ... because 'Alignment applied to class-wide types is expanded |
| -- into the code that reads the value of alignment from the TSD |
| -- (see Expand_N_Attribute_Reference) |
| |
| -- In the Use_Secondary_Stack_Pool case, Alig_Id is not |
| -- passed in and therefore must not be referenced. |
| |
| Append_To (Actuals, |
| Unchecked_Convert_To (RTE (RE_Storage_Offset), |
| Make_Attribute_Reference (Loc, |
| Prefix => |
| Make_Explicit_Dereference (Loc, Relocate_Node (Expr)), |
| Attribute_Name => Name_Alignment))); |
| end if; |
| |
| -- h) Is_Controlled |
| |
| if Needs_Fin then |
| Is_Controlled : declare |
| Flag_Id : constant Entity_Id := Make_Temporary (Loc, 'F'); |
| Flag_Expr : Node_Id; |
| Param : Node_Id; |
| Pref : Node_Id; |
| Temp : Node_Id; |
| |
| begin |
| if Is_Allocate then |
| Temp := Find_Object (Expression (Expr)); |
| else |
| Temp := Expr; |
| end if; |
| |
| -- Processing for allocations where the expression is a subtype |
| -- indication. |
| |
| if Is_Allocate |
| and then Is_Entity_Name (Temp) |
| and then Is_Type (Entity (Temp)) |
| then |
| Flag_Expr := |
| New_Occurrence_Of |
| (Boolean_Literals |
| (Needs_Finalization (Entity (Temp))), Loc); |
| |
| -- The allocation / deallocation of a class-wide object relies |
| -- on a runtime check to determine whether the object is truly |
| -- controlled or not. Depending on this check, the finalization |
| -- machinery will request or reclaim extra storage reserved for |
| -- a list header. |
| |
| elsif Is_Class_Wide_Type (Desig_Typ) then |
| |
| -- Detect a special case where interface class-wide types |
| -- are involved as the object appears as: |
| |
| -- Tag_Ptr (Base_Address (<object>'Address)) |
| |
| -- The expression already yields the proper tag, generate: |
| |
| -- Temp.all |
| |
| if Is_RTE (Etype (Temp), RE_Tag_Ptr) then |
| Param := |
| Make_Explicit_Dereference (Loc, |
| Prefix => Relocate_Node (Temp)); |
| |
| -- In the default case, obtain the tag of the object about |
| -- to be allocated / deallocated. Generate: |
| |
| -- Temp'Tag |
| |
| -- If the object is an unchecked conversion (typically to |
| -- an access to class-wide type), we must preserve the |
| -- conversion to ensure that the object is seen as tagged |
| -- in the code that follows. |
| |
| else |
| Pref := Temp; |
| |
| if Nkind (Parent (Pref)) = N_Unchecked_Type_Conversion |
| then |
| Pref := Parent (Pref); |
| end if; |
| |
| Param := |
| Make_Attribute_Reference (Loc, |
| Prefix => Relocate_Node (Pref), |
| Attribute_Name => Name_Tag); |
| end if; |
| |
| -- Generate: |
| -- Needs_Finalization (<Param>) |
| |
| Flag_Expr := |
| Make_Function_Call (Loc, |
| Name => |
| New_Occurrence_Of (RTE (RE_Needs_Finalization), Loc), |
| Parameter_Associations => New_List (Param)); |
| |
| -- Processing for generic actuals |
| |
| elsif Is_Generic_Actual_Type (Desig_Typ) then |
| Flag_Expr := |
| New_Occurrence_Of (Boolean_Literals |
| (Needs_Finalization (Base_Type (Desig_Typ))), Loc); |
| |
| -- The object does not require any specialized checks, it is |
| -- known to be controlled. |
| |
| else |
| Flag_Expr := New_Occurrence_Of (Standard_True, Loc); |
| end if; |
| |
| -- Create the temporary which represents the finalization state |
| -- of the expression. Generate: |
| -- |
| -- F : constant Boolean := <Flag_Expr>; |
| |
| Insert_Action (N, |
| Make_Object_Declaration (Loc, |
| Defining_Identifier => Flag_Id, |
| Constant_Present => True, |
| Object_Definition => |
| New_Occurrence_Of (Standard_Boolean, Loc), |
| Expression => Flag_Expr)); |
| |
| Append_To (Actuals, New_Occurrence_Of (Flag_Id, Loc)); |
| end Is_Controlled; |
| |
| -- The object is not controlled |
| |
| else |
| Append_To (Actuals, New_Occurrence_Of (Standard_False, Loc)); |
| end if; |
| |
| -- i) On_Subpool |
| |
| if Is_Allocate then |
| Append_To (Actuals, |
| New_Occurrence_Of (Boolean_Literals (Present (Subpool)), Loc)); |
| end if; |
| |
| -- Step 2: Build a wrapper Allocate / Deallocate which internally |
| -- calls Allocate_Any_Controlled / Deallocate_Any_Controlled. |
| |
| -- Select the proper routine to call |
| |
| if Is_Allocate then |
| Proc_To_Call := RTE (RE_Allocate_Any_Controlled); |
| else |
| Proc_To_Call := RTE (RE_Deallocate_Any_Controlled); |
| end if; |
| |
| -- Create a custom Allocate / Deallocate routine which has identical |
| -- profile to that of System.Storage_Pools. |
| |
| declare |
| -- P : Root_Storage_Pool |
| function Pool_Param return Node_Id is ( |
| Make_Parameter_Specification (Loc, |
| Defining_Identifier => Make_Temporary (Loc, 'P'), |
| Parameter_Type => |
| New_Occurrence_Of (RTE (RE_Root_Storage_Pool), Loc))); |
| |
| -- A : [out] Address |
| function Address_Param return Node_Id is ( |
| Make_Parameter_Specification (Loc, |
| Defining_Identifier => Addr_Id, |
| Out_Present => Is_Allocate, |
| Parameter_Type => |
| New_Occurrence_Of (RTE (RE_Address), Loc))); |
| |
| -- S : Storage_Count |
| function Size_Param return Node_Id is ( |
| Make_Parameter_Specification (Loc, |
| Defining_Identifier => Size_Id, |
| Parameter_Type => |
| New_Occurrence_Of (RTE (RE_Storage_Count), Loc))); |
| |
| -- L : Storage_Count |
| function Alignment_Param return Node_Id is ( |
| Make_Parameter_Specification (Loc, |
| Defining_Identifier => Alig_Id, |
| Parameter_Type => |
| New_Occurrence_Of (RTE (RE_Storage_Count), Loc))); |
| |
| Formal_Params : List_Id; |
| begin |
| if Use_Secondary_Stack_Pool then |
| -- Gigi expects a different profile in the Secondary_Stack_Pool |
| -- case. There must be no uses of the two missing formals |
| -- (i.e., Pool_Param and Alignment_Param) in this case. |
| Formal_Params := New_List (Address_Param, Size_Param); |
| else |
| Formal_Params := New_List ( |
| Pool_Param, Address_Param, Size_Param, Alignment_Param); |
| end if; |
| |
| Insert_Action (N, |
| Make_Subprogram_Body (Loc, |
| Specification => |
| -- procedure Pnn |
| Make_Procedure_Specification (Loc, |
| Defining_Unit_Name => Proc_Id, |
| Parameter_Specifications => Formal_Params), |
| |
| Declarations => No_List, |
| |
| Handled_Statement_Sequence => |
| Make_Handled_Sequence_Of_Statements (Loc, |
| Statements => New_List ( |
| Make_Procedure_Call_Statement (Loc, |
| Name => |
| New_Occurrence_Of (Proc_To_Call, Loc), |
| Parameter_Associations => Actuals)))), |
| Suppress => All_Checks); |
| end; |
| |
| -- The newly generated Allocate / Deallocate becomes the default |
| -- procedure to call when the back end processes the allocation / |
| -- deallocation. |
| |
| if Is_Allocate then |
| Set_Procedure_To_Call (Expr, Proc_Id); |
| else |
| Set_Procedure_To_Call (N, Proc_Id); |
| end if; |
| end; |
| end Build_Allocate_Deallocate_Proc; |
| |
| ------------------------------- |
| -- Build_Abort_Undefer_Block -- |
| ------------------------------- |
| |
| function Build_Abort_Undefer_Block |
| (Loc : Source_Ptr; |
| Stmts : List_Id; |
| Context : Node_Id) return Node_Id |
| is |
| Exceptions_OK : constant Boolean := |
| not Restriction_Active (No_Exception_Propagation); |
| |
| AUD : Entity_Id; |
| Blk : Node_Id; |
| Blk_Id : Entity_Id; |
| HSS : Node_Id; |
| |
| begin |
| -- The block should be generated only when undeferring abort in the |
| -- context of a potential exception. |
| |
| pragma Assert (Abort_Allowed and Exceptions_OK); |
| |
| -- Generate: |
| -- begin |
| -- <Stmts> |
| -- at end |
| -- Abort_Undefer_Direct; |
| -- end; |
| |
| AUD := RTE (RE_Abort_Undefer_Direct); |
| |
| HSS := |
| Make_Handled_Sequence_Of_Statements (Loc, |
| Statements => Stmts, |
| At_End_Proc => New_Occurrence_Of (AUD, Loc)); |
| |
| Blk := |
| Make_Block_Statement (Loc, |
| Handled_Statement_Sequence => HSS); |
| Set_Is_Abort_Block (Blk); |
| |
| Add_Block_Identifier (Blk, Blk_Id); |
| Expand_At_End_Handler (HSS, Blk_Id); |
| |
| -- Present the Abort_Undefer_Direct function to the back end to inline |
| -- the call to the routine. |
| |
| Add_Inlined_Body (AUD, Context); |
| |
| return Blk; |
| end Build_Abort_Undefer_Block; |
| |
| --------------------------------- |
| -- Build_Class_Wide_Expression -- |
| --------------------------------- |
| |
| procedure Build_Class_Wide_Expression |
| (Pragma_Or_Expr : Node_Id; |
| Subp : Entity_Id; |
| Par_Subp : Entity_Id; |
| Adjust_Sloc : Boolean) |
| is |
| function Replace_Entity (N : Node_Id) return Traverse_Result; |
| -- Replace reference to formal of inherited operation or to primitive |
| -- operation of root type, with corresponding entity for derived type, |
| -- when constructing the class-wide condition of an overriding |
| -- subprogram. |
| |
| -------------------- |
| -- Replace_Entity -- |
| -------------------- |
| |
| function Replace_Entity (N : Node_Id) return Traverse_Result is |
| New_E : Entity_Id; |
| |
| begin |
| if Adjust_Sloc then |
| Adjust_Inherited_Pragma_Sloc (N); |
| end if; |
| |
| if Nkind (N) in N_Identifier | N_Expanded_Name | N_Operator_Symbol |
| and then Present (Entity (N)) |
| and then |
| (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N))) |
| and then |
| (Nkind (Parent (N)) /= N_Attribute_Reference |
| or else Attribute_Name (Parent (N)) /= Name_Class) |
| then |
| -- The replacement does not apply to dispatching calls within the |
| -- condition, but only to calls whose static tag is that of the |
| -- parent type. |
| |
| if Is_Subprogram (Entity (N)) |
| and then Nkind (Parent (N)) = N_Function_Call |
| and then Present (Controlling_Argument (Parent (N))) |
| then |
| return OK; |
| end if; |
| |
| -- Determine whether entity has a renaming |
| |
| New_E := Type_Map.Get (Entity (N)); |
| |
| if Present (New_E) then |
| Rewrite (N, New_Occurrence_Of (New_E, Sloc (N))); |
| end if; |
| |
| -- Update type of function call node, which should be the same as |
| -- the function's return type. |
| |
| if Is_Subprogram (Entity (N)) |
| and then Nkind (Parent (N)) = N_Function_Call |
| then |
| Set_Etype (Parent (N), Etype (Entity (N))); |
| end if; |
| |
| -- The whole expression will be reanalyzed |
| |
| elsif Nkind (N) in N_Has_Etype then |
| Set_Analyzed (N, False); |
| end if; |
| |
| return OK; |
| end Replace_Entity; |
| |
| procedure Replace_Condition_Entities is |
| new Traverse_Proc (Replace_Entity); |
| |
| -- Local variables |
| |
| Par_Typ : constant Entity_Id := Find_Dispatching_Type (Par_Subp); |
| Subp_Typ : constant Entity_Id := Find_Dispatching_Type (Subp); |
| |
| -- Start of processing for Build_Class_Wide_Expression |
| |
| begin |
| pragma Assert (Par_Typ /= Subp_Typ); |
| |
| Update_Primitives_Mapping (Par_Subp, Subp); |
| Map_Formals (Par_Subp, Subp); |
| Replace_Condition_Entities (Pragma_Or_Expr); |
| end Build_Class_Wide_Expression; |
| |
| -------------------- |
| -- Build_DIC_Call -- |
| -------------------- |
| |
| function Build_DIC_Call |
| (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 ( |
| Unchecked_Convert_To (Formal_Typ, Obj_Name))); |
| end Build_DIC_Call; |
| |
| ------------------------------ |
| -- Build_DIC_Procedure_Body -- |
| ------------------------------ |
| |
| -- WARNING: This routine manages Ghost regions. Return statements must be |
| -- replaced by gotos which jump to the end of the routine and restore the |
| -- Ghost mode. |
| |
| procedure Build_DIC_Procedure_Body |
| (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; |
| Stmts : in out List_Id); |
| -- Subsidiary to all Add_xxx_DIC routines. Add a runtime check to verify |
| -- assertion expression DIC_Expr of pragma DIC_Prag. All generated code |
| -- is added to list Stmts. |
| |
| procedure Add_Inherited_DIC |
| (DIC_Prag : Node_Id; |
| Par_Typ : Entity_Id; |
| Deriv_Typ : Entity_Id; |
| Stmts : in out List_Id); |
| -- Add a runtime check to verify the assertion expression of inherited |
| -- pragma DIC_Prag. Par_Typ is parent type, which is also the owner of |
| -- the DIC pragma. Deriv_Typ is the derived type inheriting the DIC |
| -- pragma. All generated code is added to list Stmts. |
| |
| procedure Add_Inherited_Tagged_DIC |
| (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. Expr is |
| -- the assertion expression after substitution 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. 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 -- |
| ------------------- |
| |
| procedure Add_DIC_Check |
| (DIC_Prag : Node_Id; |
| DIC_Expr : Node_Id; |
| Stmts : in out List_Id) |
| is |
| Loc : constant Source_Ptr := Sloc (DIC_Prag); |
| Nam : constant Name_Id := Original_Aspect_Pragma_Name (DIC_Prag); |
| |
| begin |
| -- The DIC pragma is ignored, nothing left to do |
| |
| if Is_Ignored (DIC_Prag) then |
| null; |
| |
| -- Otherwise the DIC expression must be checked at run time. |
| -- Generate: |
| |
| -- pragma Check (<Nam>, <DIC_Expr>); |
| |
| else |
| Append_New_To (Stmts, |
| Make_Pragma (Loc, |
| Pragma_Identifier => |
| Make_Identifier (Loc, Name_Check), |
| |
| Pragma_Argument_Associations => New_List ( |
| Make_Pragma_Argument_Association (Loc, |
| Expression => Make_Identifier (Loc, Nam)), |
| |
| 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; |
| |
| ----------------------- |
| -- Add_Inherited_DIC -- |
| ----------------------- |
| |
| procedure Add_Inherited_DIC |
| (DIC_Prag : Node_Id; |
| Par_Typ : Entity_Id; |
| Deriv_Typ : Entity_Id; |
| Stmts : in out List_Id) |
| is |
| Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ); |
| Deriv_Obj : constant Entity_Id := First_Entity (Deriv_Proc); |
| Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ); |
| Par_Obj : constant Entity_Id := First_Entity (Par_Proc); |
| Loc : constant Source_Ptr := Sloc (DIC_Prag); |
| |
| begin |
| pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc)); |
| |
| -- Verify the inherited DIC assertion expression by calling the DIC |
| -- procedure of the parent type. |
| |
| -- Generate: |
| -- <Par_Typ>DIC (Par_Typ (_object)); |
| |
| Append_New_To (Stmts, |
| Make_Procedure_Call_Statement (Loc, |
| Name => New_Occurrence_Of (Par_Proc, Loc), |
| Parameter_Associations => New_List ( |
| Convert_To |
| (Typ => Etype (Par_Obj), |
| Expr => New_Occurrence_Of (Deriv_Obj, Loc))))); |
| end Add_Inherited_DIC; |
| |
| ------------------------------ |
| -- Add_Inherited_Tagged_DIC -- |
| ------------------------------ |
| |
| procedure Add_Inherited_Tagged_DIC |
| (DIC_Prag : Node_Id; |
| Expr : Node_Id; |
| Stmts : in out List_Id) |
| is |
| begin |
| -- Once the DIC assertion expression is fully processed, add a check |
| -- to the statements of the DIC procedure. |
| |
| 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 |
| if not Present (Priv_Typ) and then not Present (Full_Typ) then |
| return; |
| end if; |
| |
| -- 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. |
| |
| if Is_Concurrent_Type (T) then |
| Deriv_Typ := Corresponding_Record_Type (T); |
| else |
| Deriv_Typ := T; |
| end if; |
| |
| pragma Assert (Present (Deriv_Typ)); |
| |
| -- 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. |
| |
| if Present (Priv_Typ) then |
| Prag := First_Rep_Item (Priv_Typ); |
| else |
| Prag := First_Rep_Item (Full_Typ); |
| end if; |
| |
| 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 |
| |
| if Contains (Pragmas_Seen, Prag) then |
| return; |
| end if; |
| |
| -- Extract arguments of the Default_Initial_Condition pragma |
| |
| Prag_Expr_Arg := First (Pragma_Argument_Associations (Prag)); |
| Prag_Expr := Expression_Copy (Prag_Expr_Arg); |
| |
| -- Pick up the implicit second argument of the pragma, which |
| -- indicates the type that the pragma applies to. |
| |
| 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 := |
| Pragma_Argument_Associations (DIC_Prag); |
| 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); |
| |
| -- Local variables |
| |
| Typ_Decl : constant Node_Id := Declaration_Node (DIC_Typ); |
| |
| Expr : Node_Id; |
| |
| -- Start of processing for Add_Own_DIC |
| |
| begin |
| pragma Assert (Present (DIC_Expr)); |
| Expr := New_Copy_Tree (DIC_Expr); |
| |
| -- Perform the following substitution: |
| |
| -- * Replace the current instance of DIC_Typ with a reference to |
| -- the _object formal parameter of the DIC procedure. |
| |
| Replace_Type_References |
| (Expr => Expr, |
| Typ => DIC_Typ, |
| Obj_Id => Obj_Id); |
| |
| -- Preanalyze the DIC expression to detect errors and at the same |
| -- time capture the visibility of the proper package part. |
| |
| Set_Parent (Expr, Typ_Decl); |
| Preanalyze_Assert_Expression (Expr, Any_Boolean); |
| |
| -- Save a copy of the expression with all replacements and analysis |
| -- already taken place in case a derived type inherits the pragma. |
| -- The copy will be used as the foundation of the derived type's own |
| -- version of the DIC assertion expression. |
| |
| if Is_Tagged_Type (DIC_Typ) then |
| Set_Expression_Copy (DIC_Arg, New_Copy_Tree (Expr)); |
| end if; |
| |
| -- If the pragma comes from an aspect specification, replace the |
| -- saved expression because all type references must be substituted |
| -- for the call to Preanalyze_Spec_Expression in Check_Aspect_At_xxx |
| -- routines. |
| |
| if Present (DIC_Asp) then |
| Set_Entity (Identifier (DIC_Asp), New_Copy_Tree (Expr)); |
| end if; |
| |
| -- Once the DIC assertion expression is fully processed, add a check |
| -- to the statements of the DIC procedure (unless the type is an |
| -- abstract type, in which case we don't want the possibility of |
| -- generating a call to an abstract function of the type; such DIC |
| -- procedures can never be called in any case, so not generating the |
| -- check at all is OK). |
| |
| if not Is_Abstract_Type (DIC_Typ) or else GNATprove_Mode then |
| Add_DIC_Check |
| (DIC_Prag => DIC_Prag, |
| DIC_Expr => Expr, |
| Stmts => Stmts); |
| end if; |
| 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 |
| |
| Op_Node : Elmt_Id; |
| Par_Prim : Entity_Id; |
| Prim : Entity_Id; |
| |
| begin |
| -- Map the overridden primitive to the overriding one; required by |
| -- Replace_References (called by Add_Inherited_DICs) to handle calls |
| -- to parent primitives. |
| |
| Op_Node := First_Elmt (Primitive_Operations (T)); |
| while Present (Op_Node) loop |
| Prim := Node (Op_Node); |
| |
| if Present (Overridden_Operation (Prim)) |
| and then Comes_From_Source (Prim) |
| then |
| Par_Prim := Overridden_Operation (Prim); |
| |
| -- Create a mapping of the form: |
| -- parent type primitive -> derived type primitive |
| |
| Type_Map.Set (Par_Prim, Prim); |
| end if; |
| |
| Next_Elmt (Op_Node); |
| end loop; |
| |
| -- 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); |
| |
| Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; |
| Saved_IGR : constant Node_Id := Ignored_Ghost_Region; |
| -- Save the Ghost-related attributes to restore on exit |
| |
| DIC_Prag : Node_Id; |
| DIC_Typ : Entity_Id; |
| Dummy_1 : Entity_Id; |
| Dummy_2 : Entity_Id; |
| Proc_Body : Node_Id; |
| Proc_Body_Id : Entity_Id; |
| Proc_Decl : Node_Id; |
| Proc_Id : Entity_Id; |
| Stmts : List_Id := No_List; |
| |
| 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 |
| |
| -- Start of processing for Build_DIC_Procedure_Body |
| |
| begin |
| Work_Typ := Base_Type (Typ); |
| |
| -- Do not process class-wide types as these are Itypes, but lack a first |
| -- subtype (see below). |
| |
| if Is_Class_Wide_Type (Work_Typ) then |
| return; |
| |
| -- Do not process the underlying full view of a private type. There is |
| -- no way to get back to the partial view, plus the body will be built |
| -- by the full view or the base type. |
| |
| elsif Is_Underlying_Full_View (Work_Typ) then |
| return; |
| |
| -- Use the first subtype when dealing with various base types |
| |
| elsif Is_Itype (Work_Typ) then |
| Work_Typ := First_Subtype (Work_Typ); |
| |
| -- The input denotes the corresponding record type of a protected or a |
| -- task type. Work with the concurrent type because the corresponding |
| -- record type may not be visible to clients of the type. |
| |
| elsif Ekind (Work_Typ) = E_Record_Type |
| and then Is_Concurrent_Record_Type (Work_Typ) |
| then |
| Work_Typ := Corresponding_Concurrent_Type (Work_Typ); |
| end if; |
| |
| -- The working type may be subject to pragma Ghost. Set the mode now to |
| -- ensure that the DIC procedure is properly marked as Ghost. |
| |
| Set_Ghost_Mode (Work_Typ); |
| |
| -- The working type must be either define a DIC pragma of its own or |
| -- inherit one from a parent type. |
| |
| pragma Assert (Has_DIC (Work_Typ)); |
| |
| -- Recover the type which defines the DIC pragma. This is either the |
| -- working type itself or a parent type when the pragma is inherited. |
| |
| DIC_Typ := Find_DIC_Type (Work_Typ); |
| pragma Assert (Present (DIC_Typ)); |
| |
| DIC_Prag := Get_Pragma (DIC_Typ, Pragma_Default_Initial_Condition); |
| pragma Assert (Present (DIC_Prag)); |
| |
| -- Nothing to do if pragma DIC appears without an argument or its sole |
| -- argument is "null". |
| |
| if not Is_Verifiable_DIC_Pragma (DIC_Prag) then |
| goto Leave; |
| end if; |
| |
| -- Obtain both views of the type |
| |
| Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy_1, CRec_Typ); |
| |
| -- The caller requests a body for the partial DIC procedure |
| |
| if Partial_DIC then |
| Proc_Id := Partial_DIC_Procedure (Work_Typ); |
| |
| -- The "full" DIC procedure body was already created |
| |
| -- 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); |
| |
| 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 |
| |
| pragma Assert (Present (Proc_Id)); |
| Proc_Decl := Unit_Declaration_Node (Proc_Id); |
| |
| -- Nothing to do if the DIC procedure already has a body |
| |
| if Present (Corresponding_Body (Proc_Decl)) then |
| goto Leave; |
| end if; |
| |
| -- Emulate the environment of the DIC procedure by installing its scope |
| -- and formal parameters. |
| |
| Push_Scope (Proc_Id); |
| Install_Formals (Proc_Id); |
| |
| Obj_Id := First_Formal (Proc_Id); |
| pragma Assert (Present (Obj_Id)); |
| |
| -- The "partial" DIC procedure verifies the DICs of the partial view |
| -- only. |
| |
| 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; |
| |
| -- Otherwise, the "full" DIC procedure verifies the DICs inherited from |
| -- parent types, as well as indirectly verifying the DICs of the partial |
| -- view by calling the "partial" DIC procedure. |
| |
| else |
| -- Check the DIC of the partial view by calling the "partial" DIC |
| -- procedure, unless the partial DIC body is empty. Generate: |
| |
| -- <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; |
| |
| -- Process inherited Default_Initial_Conditions for all parent types |
| |
| Add_Parent_DICs (Work_Typ, Obj_Id, Stmts); |
| end if; |
| |
| End_Scope; |
| |
| -- 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; |
| |
| -- 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 |
| |
| Mutate_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; |
| |
| -- 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>> |
| Restore_Ghost_Region (Saved_GM, Saved_IGR); |
| end Build_DIC_Procedure_Body; |
| |
| ------------------------------------- |
| -- Build_DIC_Procedure_Declaration -- |
| ------------------------------------- |
| |
| -- WARNING: This routine manages Ghost regions. Return statements must be |
| -- replaced by gotos which jump to the end of the routine and restore the |
| -- Ghost mode. |
| |
| 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; |
| Saved_IGR : constant Node_Id := Ignored_Ghost_Region; |
| -- Save the Ghost-related attributes to restore on exit |
| |
| DIC_Prag : Node_Id; |
| DIC_Typ : Entity_Id; |
| Proc_Decl : Node_Id; |
| Proc_Id : Entity_Id; |
| Proc_Nam : Name_Id; |
| Typ_Decl : Node_Id; |
| |
| CRec_Typ : Entity_Id; |
| -- The corresponding record type of Full_Typ |
| |
| Full_Typ : Entity_Id; |
| -- The full view of working type |
| |
| Obj_Id : Entity_Id; |
| -- The _object formal parameter of the DIC procedure |
| |
| Priv_Typ : Entity_Id; |
| -- The partial view of working type |
| |
| UFull_Typ : Entity_Id; |
| -- The underlying full view of Full_Typ |
| |
| Work_Typ : Entity_Id; |
| -- The working type |
| |
| begin |
| Work_Typ := Base_Type (Typ); |
| |
| -- Do not process class-wide types as these are Itypes, but lack a first |
| -- subtype (see below). |
| |
| if Is_Class_Wide_Type (Work_Typ) then |
| return; |
| |
| -- Do not process the underlying full view of a private type. There is |
| -- no way to get back to the partial view, plus the body will be built |
| -- by the full view or the base type. |
| |
| elsif Is_Underlying_Full_View (Work_Typ) then |
| return; |
| |
| -- Use the first subtype when dealing with various base types |
| |
| elsif Is_Itype (Work_Typ) then |
| Work_Typ := First_Subtype (Work_Typ); |
| |
| -- The input denotes the corresponding record type of a protected or a |
| -- task type. Work with the concurrent type because the corresponding |
| -- record type may not be visible to clients of the type. |
| |
| elsif Ekind (Work_Typ) = E_Record_Type |
| and then Is_Concurrent_Record_Type (Work_Typ) |
| then |
| Work_Typ := Corresponding_Concurrent_Type (Work_Typ); |
| end if; |
| |
| -- The working type may be subject to pragma Ghost. Set the mode now to |
| -- ensure that the DIC procedure is properly marked as Ghost. |
| |
| Set_Ghost_Mode (Work_Typ); |
| |
| -- The type must be either subject to a DIC pragma or inherit one from a |
| -- parent type. |
| |
| pragma Assert (Has_DIC (Work_Typ)); |
| |
| -- Recover the type which defines the DIC pragma. This is either the |
| -- working type itself or a parent type when the pragma is inherited. |
| |
| DIC_Typ := Find_DIC_Type (Work_Typ); |
| pragma Assert (Present (DIC_Typ)); |
| |
| DIC_Prag := Get_Pragma (DIC_Typ, Pragma_Default_Initial_Condition); |
| pragma Assert (Present (DIC_Prag)); |
| |
| -- Nothing to do if pragma DIC appears without an argument or its sole |
| -- argument is "null". |
| |
| 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 "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 => Proc_Nam); |
| |
| -- Perform minor decoration in case the declaration is not analyzed |
| |
| Mutate_Ekind (Proc_Id, E_Procedure); |
| Set_Etype (Proc_Id, Standard_Void_Type); |
| Set_Is_DIC_Procedure (Proc_Id); |
| Set_Scope (Proc_Id, Current_Scope); |
| Set_SPARK_Pragma (Proc_Id, SPARK_Mode_Pragma); |
| Set_SPARK_Pragma_Inherited (Proc_Id); |
| |
| Set_DIC_Procedure (Work_Typ, Proc_Id); |
| |
| -- The DIC procedure requires debug info when the assertion expression |
| -- is subject to Source Coverage Obligations. |
| |
| if Generate_SCO then |
| Set_Debug_Info_Needed (Proc_Id); |
| end if; |
| |
| -- Obtain all views of the input type |
| |
| Get_Views (Work_Typ, Priv_Typ, Full_Typ, UFull_Typ, CRec_Typ); |
| |
| -- Associate the DIC procedure and various flags with all views |
| |
| Propagate_DIC_Attributes (Priv_Typ, From_Typ => Work_Typ); |
| Propagate_DIC_Attributes (Full_Typ, From_Typ => Work_Typ); |
| Propagate_DIC_Attributes (UFull_Typ, From_Typ => Work_Typ); |
| Propagate_DIC_Attributes (CRec_Typ, From_Typ => Work_Typ); |
| |
| -- The declaration of the DIC procedure must be inserted after the |
| -- declaration of the partial view as this allows for proper external |
| -- visibility. |
| |
| if Present (Priv_Typ) then |
| Typ_Decl := Declaration_Node (Priv_Typ); |
| |
| -- Derived types with the full view as parent do not have a partial |
| -- view. Insert the DIC procedure after the derived type. |
| |
| else |
| Typ_Decl := Declaration_Node (Full_Typ); |
| end if; |
| |
| -- The type should have a declarative node |
| |
| pragma Assert (Present (Typ_Decl)); |
| |
| -- Create the formal parameter which emulates the variable-like behavior |
| -- of the type's current instance. |
| |
| Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject); |
| |
| -- Perform minor decoration in case the declaration is not analyzed |
| |
| Mutate_Ekind (Obj_Id, E_In_Parameter); |
| Set_Etype (Obj_Id, Work_Typ); |
| Set_Scope (Obj_Id, Proc_Id); |
| |
| Set_First_Entity (Proc_Id, Obj_Id); |
| Set_Last_Entity (Proc_Id, Obj_Id); |
| |
| -- Generate: |
| -- procedure <Work_Typ>DIC (_object : <Work_Typ>); |
| |
| Proc_Decl := |
| Make_Subprogram_Declaration (Loc, |
| Specification => |
| Make_Procedure_Specification (Loc, |
| Defining_Unit_Name => Proc_Id, |
| Parameter_Specifications => New_List ( |
| Make_Parameter_Specification (Loc, |
| Defining_Identifier => Obj_Id, |
| Parameter_Type => |
| New_Occurrence_Of (Work_Typ, Loc))))); |
| |
| -- The declaration should not be inserted into the tree when the context |
| -- is a generic unit because it is not part of the template. |
| |
| if Inside_A_Generic then |
| null; |
| |
| -- Semi-insert the declaration into the tree for GNATprove by setting |
| -- its Parent field. This allows for proper upstream tree traversals. |
| |
| elsif GNATprove_Mode then |
| Set_Parent (Proc_Decl, Parent (Typ_Decl)); |
| |
| -- Otherwise insert the declaration |
| |
| else |
| Insert_After_And_Analyze (Typ_Decl, Proc_Decl); |
| end if; |
| |
| <<Leave>> |
| Restore_Ghost_Region (Saved_GM, Saved_IGR); |
| end Build_DIC_Procedure_Declaration; |
| |
| ------------------------------------ |
| -- Build_Invariant_Procedure_Body -- |
| ------------------------------------ |
| |
| -- WARNING: This routine manages Ghost regions. Return statements must be |
| -- replaced by gotos which jump to the end of the routine and restore the |
| -- Ghost mode. |
| |
| procedure Build_Invariant_Procedure_Body |
| (Typ : Entity_Id; |
| Partial_Invariant : Boolean := False) |
| is |
| Loc : constant Source_Ptr := Sloc (Typ); |
| |
| Pragmas_Seen : Elist_Id := No_Elist; |
| -- This list contains all invariant pragmas processed so far. The list |
| -- is used to avoid generating redundant invariant checks. |
| |
| Produced_Check : Boolean := False; |
| -- This flag tracks whether the type has produced at least one invariant |
| -- check. The flag is used as a sanity check at the end of the routine. |
| |
| -- NOTE: most of the routines in Build_Invariant_Procedure_Body are |
| -- intentionally unnested to avoid deep indentation of code. |
| |
| -- NOTE: all Add_xxx_Invariants routines are reactive. In other words |
| -- they emit checks, loops (for arrays) and case statements (for record |
| -- variant parts) only when there are invariants to verify. This keeps |
| -- the body of the invariant procedure free of useless code. |
| |
| procedure Add_Array_Component_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id); |
| -- Generate an invariant check for each component of array type T. |
| -- Obj_Id denotes the entity of the _object formal parameter of the |
| -- invariant procedure. All created checks are added to list Checks. |
| |
| procedure Add_Inherited_Invariants |
| (T : Entity_Id; |
| Priv_Typ : Entity_Id; |
| Full_Typ : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id); |
| -- Generate an invariant check for each inherited class-wide invariant |
| -- 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 invariant procedure. |
| -- All created checks are added to list Checks. |
| |
| procedure Add_Interface_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id); |
| -- Generate an invariant check for each inherited class-wide invariant |
| -- coming from all interfaces implemented by type T. Obj_Id denotes the |
| -- entity of the _object formal parameter of the invariant procedure. |
| -- All created checks are added to list Checks. |
| |
| procedure Add_Invariant_Check |
| (Prag : Node_Id; |
| Expr : Node_Id; |
| Checks : in out List_Id; |
| Inherited : Boolean := False); |
| -- Subsidiary to all Add_xxx_Invariant routines. Add a runtime check to |
| -- verify assertion expression Expr of pragma Prag. All generated code |
| -- is added to list Checks. Flag Inherited should be set when the pragma |
| -- is inherited from a parent or interface type. |
| |
| procedure Add_Own_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id; |
| Priv_Item : Node_Id := Empty); |
| -- Generate an invariant check for each invariant found for type T. |
| -- Obj_Id denotes the entity of the _object formal parameter of the |
| -- invariant procedure. All created checks are added to list Checks. |
| -- Priv_Item denotes the first rep item of the private type. |
| |
| procedure Add_Parent_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id); |
| -- Generate an invariant check for each inherited class-wide invariant |
| -- coming from all parent types of type T. Obj_Id denotes the entity of |
| -- the _object formal parameter of the invariant procedure. All created |
| -- checks are added to list Checks. |
| |
| procedure Add_Record_Component_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id); |
| -- Generate an invariant check for each component of record type T. |
| -- Obj_Id denotes the entity of the _object formal parameter of the |
| -- invariant procedure. All created checks are added to list Checks. |
| |
| ------------------------------------ |
| -- Add_Array_Component_Invariants -- |
| ------------------------------------ |
| |
| procedure Add_Array_Component_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id) |
| is |
| Comp_Typ : constant Entity_Id := Component_Type (T); |
| Dims : constant Pos := Number_Dimensions (T); |
| |
| procedure Process_Array_Component |
| (Indices : List_Id; |
| Comp_Checks : in out List_Id); |
| -- Generate an invariant check for an array component identified by |
| -- the indices in list Indices. All created checks are added to list |
| -- Comp_Checks. |
| |
| procedure Process_One_Dimension |
| (Dim : Pos; |
| Indices : List_Id; |
| Dim_Checks : in out List_Id); |
| -- Generate a loop over the Nth dimension Dim of an array type. List |
| -- Indices contains all array indices for the dimension. All created |
| -- checks are added to list Dim_Checks. |
| |
| ----------------------------- |
| -- Process_Array_Component -- |
| ----------------------------- |
| |
| procedure Process_Array_Component |
| (Indices : List_Id; |
| Comp_Checks : in out List_Id) |
| is |
| Proc_Id : Entity_Id; |
| |
| begin |
| if Has_Invariants (Comp_Typ) then |
| |
| -- In GNATprove mode, the component invariants are checked by |
| -- other means. They should not be added to the array type |
| -- invariant procedure, so that the procedure can be used to |
| -- check the array type invariants if any. |
| |
| if GNATprove_Mode then |
| null; |
| |
| else |
| Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ)); |
| |
| -- The component type should have an invariant procedure |
| -- if it has invariants of its own or inherits class-wide |
| -- invariants from parent or interface types. |
| |
| pragma Assert (Present (Proc_Id)); |
| |
| -- Generate: |
| -- <Comp_Typ>Invariant (_object (<Indices>)); |
| |
| -- The invariant procedure has a null body if assertions are |
| -- disabled or Assertion_Policy Ignore is in effect. |
| |
| if not Has_Null_Body (Proc_Id) then |
| Append_New_To (Comp_Checks, |
| Make_Procedure_Call_Statement (Loc, |
| Name => |
| New_Occurrence_Of (Proc_Id, Loc), |
| Parameter_Associations => New_List ( |
| Make_Indexed_Component (Loc, |
| Prefix => New_Occurrence_Of (Obj_Id, Loc), |
| Expressions => New_Copy_List (Indices))))); |
| end if; |
| end if; |
| |
| Produced_Check := True; |
| end if; |
| end Process_Array_Component; |
| |
| --------------------------- |
| -- Process_One_Dimension -- |
| --------------------------- |
| |
| procedure Process_One_Dimension |
| (Dim : Pos; |
| Indices : List_Id; |
| Dim_Checks : in out List_Id) |
| is |
| Comp_Checks : List_Id := No_List; |
| Index : Entity_Id; |
| |
| begin |
| -- Generate the invariant checks for the array component after all |
| -- dimensions have produced their respective loops. |
| |
| if Dim > Dims then |
| Process_Array_Component |
| (Indices => Indices, |
| Comp_Checks => Dim_Checks); |
| |
| -- Otherwise create a loop for the current dimension |
| |
| else |
| -- Create a new loop variable for each dimension |
| |
| Index := |
| Make_Defining_Identifier (Loc, |
| Chars => New_External_Name ('I', Dim)); |
| Append_To (Indices, New_Occurrence_Of (Index, Loc)); |
| |
| Process_One_Dimension |
| (Dim => Dim + 1, |
| Indices => Indices, |
| Dim_Checks => Comp_Checks); |
| |
| -- Generate: |
| -- for I<Dim> in _object'Range (<Dim>) loop |
| -- <Comp_Checks> |
| -- end loop; |
| |
| -- Note that the invariant procedure may have a null body if |
| -- assertions are disabled or Assertion_Policy Ignore is in |
| -- effect. |
| |
| if Present (Comp_Checks) then |
| Append_New_To (Dim_Checks, |
| Make_Implicit_Loop_Statement (T, |
| Identifier => Empty, |
| Iteration_Scheme => |
| Make_Iteration_Scheme (Loc, |
| Loop_Parameter_Specification => |
| Make_Loop_Parameter_Specification (Loc, |
| Defining_Identifier => Index, |
| Discrete_Subtype_Definition => |
| Make_Attribute_Reference (Loc, |
| Prefix => |
| New_Occurrence_Of (Obj_Id, Loc), |
| Attribute_Name => Name_Range, |
| Expressions => New_List ( |
| Make_Integer_Literal (Loc, Dim))))), |
| Statements => Comp_Checks)); |
| end if; |
| end if; |
| end Process_One_Dimension; |
| |
| -- Start of processing for Add_Array_Component_Invariants |
| |
| begin |
| Process_One_Dimension |
| (Dim => 1, |
| Indices => New_List, |
| Dim_Checks => Checks); |
| end Add_Array_Component_Invariants; |
| |
| ------------------------------ |
| -- Add_Inherited_Invariants -- |
| ------------------------------ |
| |
| procedure Add_Inherited_Invariants |
| (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 |
| if not Present (Priv_Typ) and then not Present (Full_Typ) then |
| return; |
| end if; |
| |
| -- 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. |
| |
| if Is_Concurrent_Type (T) then |
| Deriv_Typ := Corresponding_Record_Type (T); |
| else |
| Deriv_Typ := T; |
| end if; |
| |
| pragma Assert (Present (Deriv_Typ)); |
| |
| -- 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. |
| |
| if Present (Priv_Typ) then |
| Prag := First_Rep_Item (Priv_Typ); |
| else |
| Prag := First_Rep_Item (Full_Typ); |
| end if; |
| |
| while Present (Prag) loop |
| if Nkind (Prag) = N_Pragma |
| and then Pragma_Name (Prag) = Name_Invariant |
| then |
| -- Nothing to do if the pragma was already processed |
| |
| if Contains (Pragmas_Seen, Prag) then |
| return; |
| |
| -- Nothing to do when the caller requests the processing of all |
| -- inherited class-wide invariants, but the pragma does not |
| -- fall in this category. |
| |
| elsif not Class_Present (Prag) then |
| return; |
| end if; |
| |
| -- Extract the arguments of the invariant pragma |
| |
| Prag_Typ_Arg := First (Pragma_Argument_Associations (Prag)); |
| Prag_Expr_Arg := Next (Prag_Typ_Arg); |
| Prag_Expr := Expression_Copy (Prag_Expr_Arg); |
| Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg); |
| |
| -- The pragma applies to the partial view of the parent type |
| |
| if Present (Priv_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 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; |
| |
| -- Perform the following substitutions: |
| |
| -- * Replace a reference to the _object parameter of the |
| -- parent type's partial invariant procedure with a |
| -- reference to the _object parameter of the derived |
| -- type's full invariant procedure. |
| |
| -- * Replace a reference to a discriminant of the parent type |
| -- with a suitable value from the point of view of the |
| -- derived type. |
| |
| -- * Replace a call to an overridden parent primitive with a |
| -- call to the overriding derived type primitive. |
| |
| -- * Replace a call to an inherited parent primitive with a |
| -- call to the internally-generated inherited derived type |
| -- primitive. |
| |
| Expr := New_Copy_Tree (Prag_Expr); |
| |
| -- The parent type must have a "partial" invariant procedure |
| -- because class-wide invariants are captured exclusively by |
| -- it. |
| |
| Par_Proc := Partial_Invariant_Procedure (Par_Typ); |
| pragma Assert (Present (Par_Proc)); |
| |
| Replace_References |
| (Expr => Expr, |
| Par_Typ => Par_Typ, |
| Deriv_Typ => Deriv_Typ, |
| Par_Obj => First_Formal (Par_Proc), |
| Deriv_Obj => Obj_Id); |
| |
| Add_Invariant_Check (Prag, Expr, Checks, Inherited => True); |
| end if; |
| |
| Next_Rep_Item (Prag); |
| end loop; |
| end Add_Inherited_Invariants; |
| |
| ------------------------------ |
| -- Add_Interface_Invariants -- |
| ------------------------------ |
| |
| procedure Add_Interface_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id) |
| is |
| Iface_Elmt : Elmt_Id; |
| Ifaces : Elist_Id; |
| |
| begin |
| -- Generate an invariant check for each class-wide invariant coming |
| -- from all interfaces implemented by type T. |
| |
| if Is_Tagged_Type (T) then |
| Collect_Interfaces (T, Ifaces); |
| |
| -- Process the class-wide invariants of all implemented interfaces |
| |
| Iface_Elmt := First_Elmt (Ifaces); |
| while Present (Iface_Elmt) loop |
| |
| -- The Full_Typ parameter is intentionally left Empty because |
| -- interfaces are treated as the partial view of a private type |
| -- in order to achieve uniformity with the general case. |
| |
| Add_Inherited_Invariants |
| (T => T, |
| Priv_Typ => Node (Iface_Elmt), |
| Full_Typ => Empty, |
| Obj_Id => Obj_Id, |
| Checks => Checks); |
| |
| Next_Elmt (Iface_Elmt); |
| end loop; |
| end if; |
| end Add_Interface_Invariants; |
| |
| ------------------------- |
| -- Add_Invariant_Check -- |
| ------------------------- |
| |
| procedure Add_Invariant_Check |
| (Prag : Node_Id; |
| Expr : Node_Id; |
| Checks : in out List_Id; |
| Inherited : Boolean := False) |
| is |
| Args : constant List_Id := Pragma_Argument_Associations (Prag); |
| Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag); |
| Ploc : constant Source_Ptr := Sloc (Prag); |
| Str_Arg : constant Node_Id := Next (Next (First (Args))); |
| |
| Assoc : List_Id; |
| Str : String_Id; |
| |
| begin |
| -- The invariant is ignored, nothing left to do |
| |
| if Is_Ignored (Prag) then |
| null; |
| |
| -- Otherwise the invariant is checked. Build a pragma Check to verify |
| -- the expression at run time. |
| |
| else |
| Assoc := New_List ( |
| Make_Pragma_Argument_Association (Ploc, |
| Expression => Make_Identifier (Ploc, Nam)), |
| Make_Pragma_Argument_Association (Ploc, |
| Expression => Expr)); |
| |
| -- Handle the String argument (if any) |
| |
| if Present (Str_Arg) then |
| Str := Strval (Get_Pragma_Arg (Str_Arg)); |
| |
| -- When inheriting an invariant, modify the message from |
| -- "failed invariant" to "failed inherited invariant". |
| |
| if Inherited then |
| String_To_Name_Buffer (Str); |
| |
| if Name_Buffer (1 .. 16) = "failed invariant" then |
| Insert_Str_In_Name_Buffer ("inherited ", 8); |
| Str := String_From_Name_Buffer; |
| end if; |
| end if; |
| |
| Append_To (Assoc, |
| Make_Pragma_Argument_Association (Ploc, |
| Expression => Make_String_Literal (Ploc, Str))); |
| end if; |
| |
| -- Generate: |
| -- pragma Check (<Nam>, <Expr>, <Str>); |
| |
| Append_New_To (Checks, |
| Make_Pragma (Ploc, |
| Chars => Name_Check, |
| Pragma_Argument_Associations => Assoc)); |
| end if; |
| |
| -- Output an info message when inheriting an invariant and the |
| -- listing option is enabled. |
| |
| if Inherited and Opt.List_Inherited_Aspects then |
| Error_Msg_Sloc := Sloc (Prag); |
| Error_Msg_N |
| ("info: & inherits `Invariant''Class` aspect from #?.l?", Typ); |
| end if; |
| |
| -- Add the pragma to the list of processed pragmas |
| |
| Append_New_Elmt (Prag, Pragmas_Seen); |
| Produced_Check := True; |
| end Add_Invariant_Check; |
| |
| --------------------------- |
| -- Add_Parent_Invariants -- |
| --------------------------- |
| |
| procedure Add_Parent_Invariants |
| (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 |
| -- Do not process array types because they cannot have true parent |
| -- types. This also prevents the generation of a duplicate invariant |
| -- check when the input type is an array base type because its Etype |
| -- denotes the first subtype, both of which share the same component |
| -- type. |
| |
| if Is_Array_Type (T) then |
| return; |
| end if; |
| |
| -- Climb the parent type chain |
| |
| Curr_Typ := T; |
| loop |
| -- Do not consider subtypes as they inherit the invariants |
| -- from their base types. |
| |
| Par_Typ := Base_Type (Etype (Curr_Typ)); |
| |
| -- Stop the climb once the root of the parent chain is |
| -- reached. |
| |
| exit when Curr_Typ = Par_Typ; |
| |
| -- Process the class-wide invariants of the parent type |
| |
| Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2); |
| |
| -- Process the elements of an array type |
| |
| if Is_Array_Type (Full_Typ) then |
| Add_Array_Component_Invariants (Full_Typ, Obj_Id, Checks); |
| |
| -- Process the components of a record type |
| |
| elsif Ekind (Full_Typ) = E_Record_Type then |
| Add_Record_Component_Invariants (Full_Typ, Obj_Id, Checks); |
| end if; |
| |
| Add_Inherited_Invariants |
| (T => T, |
| Priv_Typ => Priv_Typ, |
| Full_Typ => Full_Typ, |
| Obj_Id => Obj_Id, |
| Checks => Checks); |
| |
| Curr_Typ := Par_Typ; |
| end loop; |
| end Add_Parent_Invariants; |
| |
| ------------------------ |
| -- Add_Own_Invariants -- |
| ------------------------ |
| |
| procedure Add_Own_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id; |
| Priv_Item : Node_Id := Empty) |
| is |
| Expr : Node_Id; |
| Prag : Node_Id; |
| Prag_Asp : Node_Id; |
| Prag_Expr : Node_Id; |
| Prag_Expr_Arg : Node_Id; |
| Prag_Typ : Node_Id; |
| Prag_Typ_Arg : Node_Id; |
| |
| begin |
| if not Present (T) then |
| return; |
| end if; |
| |
| Prag := First_Rep_Item (T); |
| while Present (Prag) loop |
| if Nkind (Prag) = N_Pragma |
| and then Pragma_Name (Prag) = Name_Invariant |
| then |
| -- Stop the traversal of the rep item chain once a specific |
| -- item is encountered. |
| |
| if Present (Priv_Item) and then Prag = Priv_Item then |
| exit; |
| end if; |
| |
| -- Nothing to do if the pragma was already processed |
| |
| if Contains (Pragmas_Seen, Prag) then |
| return; |
| end if; |
| |
| -- Extract the arguments of the invariant pragma |
| |
| Prag_Typ_Arg := First (Pragma_Argument_Associations (Prag)); |
| Prag_Expr_Arg := Next (Prag_Typ_Arg); |
| Prag_Expr := Get_Pragma_Arg (Prag_Expr_Arg); |
| Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg); |
| Prag_Asp := Corresponding_Aspect (Prag); |
| |
| -- Verify the pragma belongs to T, otherwise the pragma applies |
| -- to a parent type in which case it will be processed later by |
| -- Add_Parent_Invariants or Add_Interface_Invariants. |
| |
| if Entity (Prag_Typ) /= T then |
| return; |
| end if; |
| |
| Expr := New_Copy_Tree (Prag_Expr); |
| |
| -- Substitute all references to type T with references to the |
| -- _object formal parameter. |
| |
| Replace_Type_References (Expr, T, Obj_Id); |
| |
| -- Preanalyze the invariant expression to detect errors and at |
| -- the same time capture the visibility of the proper package |
| -- part. |
| |
| Set_Parent (Expr, Parent (Prag_Expr)); |
| Preanalyze_Assert_Expression (Expr, Any_Boolean); |
| |
| -- Save a copy of the expression when T is tagged to detect |
| -- errors and capture the visibility of the proper package part |
| -- for the generation of inherited type invariants. |
| |
| if Is_Tagged_Type (T) then |
| Set_Expression_Copy (Prag_Expr_Arg, New_Copy_Tree (Expr)); |
| end if; |
| |
| -- If the pragma comes from an aspect specification, replace |
| -- the saved expression because all type references must be |
| -- substituted for the call to Preanalyze_Spec_Expression in |
| -- Check_Aspect_At_xxx routines. |
| |
| if Present (Prag_Asp) then |
| Set_Entity (Identifier (Prag_Asp), New_Copy_Tree (Expr)); |
| end if; |
| |
| Add_Invariant_Check (Prag, Expr, Checks); |
| end if; |
| |
| Next_Rep_Item (Prag); |
| end loop; |
| end Add_Own_Invariants; |
| |
| ------------------------------------- |
| -- Add_Record_Component_Invariants -- |
| ------------------------------------- |
| |
| procedure Add_Record_Component_Invariants |
| (T : Entity_Id; |
| Obj_Id : Entity_Id; |
| Checks : in out List_Id) |
| is |
| procedure Process_Component_List |
| (Comp_List : Node_Id; |
| CL_Checks : in out List_Id); |
| -- Generate invariant checks for all record components found in |
| -- component list Comp_List, including variant parts. All created |
| -- checks are added to list CL_Checks. |
| |
| procedure Process_Record_Component |
| (Comp_Id : Entity_Id; |
| Comp_Checks : in out List_Id); |
| -- Generate an invariant check for a record component identified by |
| -- Comp_Id. All created checks are added to list Comp_Checks. |
| |
| ---------------------------- |
| -- Process_Component_List -- |
| ---------------------------- |
| |
| procedure Process_Component_List |
| (Comp_List : Node_Id; |
| CL_Checks : in out List_Id) |
| is |
| Comp : Node_Id; |
| Var : Node_Id; |
| Var_Alts : List_Id := No_List; |
| Var_Checks : List_Id := No_List; |
| Var_Stmts : List_Id; |
| |
| Produced_Variant_Check : Boolean := False; |
| -- This flag tracks whether the component has produced at least |
| -- one invariant check. |
| |
| begin |
| -- Traverse the component items |
| |
| Comp := First (Component_Items (Comp_List)); |
| while Present (Comp) loop |
| if Nkind (Comp) = N_Component_Declaration then |
| |
| -- Generate the component invariant check |
| |
| Process_Record_Component |
| (Comp_Id => Defining_Entity (Comp), |
| Comp_Checks => CL_Checks); |
| end if; |
| |
| Next (Comp); |
| end loop; |
| |
| -- Traverse the variant part |
| |
| if Present (Variant_Part (Comp_List)) then |
| Var := First (Variants (Variant_Part (Comp_List))); |
| while Present (Var) loop |
| Var_Checks := No_List; |
| |
| -- Generate invariant checks for all components and variant |
| -- parts that qualify. |
| |
| Process_Component_List |
| (Comp_List => Component_List (Var), |
| CL_Checks => Var_Checks); |
| |
| -- The components of the current variant produced at least |
| -- one invariant check. |
| |
| if Present (Var_Checks) then |
| Var_Stmts := Var_Checks; |
| Produced_Variant_Check := True; |
| |
| -- Otherwise there are either no components with invariants, |
| -- assertions are disabled, or Assertion_Policy Ignore is in |
| -- effect. |
| |
| else |
| Var_Stmts := New_List (Make_Null_Statement (Loc)); |
| end if; |
| |
| Append_New_To (Var_Alts, |
| Make_Case_Statement_Alternative (Loc, |
| Discrete_Choices => |
| New_Copy_List (Discrete_Choices (Var)), |
| Statements => Var_Stmts)); |
| |
| Next (Var); |
| end loop; |
| |
| -- Create a case statement which verifies the invariant checks |
| -- of a particular component list depending on the discriminant |
| -- values only when there is at least one real invariant check. |
| |
| if Produced_Variant_Check then |
| Append_New_To (CL_Checks, |
| Make_Case_Statement (Loc, |
| Expression => |
| Make_Selected_Component (Loc, |
| Prefix => New_Occurrence_Of (Obj_Id, Loc), |
| Selector_Name => |
| New_Occurrence_Of |
| (Entity (Name (Variant_Part (Comp_List))), Loc)), |
| Alternatives => Var_Alts)); |
| end if; |
| end if; |
| end Process_Component_List; |
| |
| ------------------------------ |
| -- Process_Record_Component -- |
| ------------------------------ |
| |
| procedure Process_Record_Component |
| (Comp_Id : Entity_Id; |
| Comp_Checks : in out List_Id) |
| is |
| Comp_Typ : constant Entity_Id := Etype (Comp_Id); |
| Proc_Id : Entity_Id; |
| |
| Produced_Component_Check : Boolean := False; |
| -- This flag tracks whether the component has produced at least |
| -- one invariant check. |
| |
| begin |
| -- Nothing to do for internal component _parent. Note that it is |
| -- not desirable to check whether the component comes from source |
| -- because protected type components are relocated to an internal |
| -- corresponding record, but still need processing. |
| |
| if Chars (Comp_Id) = Name_uParent then |
| return; |
| end if; |
| |
| -- Verify the invariant of the component. Note that an access |
| -- type may have an invariant when it acts as the full view of a |
| -- private type and the invariant appears on the partial view. In |
| -- this case verify the access value itself. |
| |
| if Has_Invariants (Comp_Typ) then |
| |
| -- In GNATprove mode, the component invariants are checked by |
| -- other means. They should not be added to the record type |
| -- invariant procedure, so that the procedure can be used to |
| -- check the record type invariants if any. |
| |
| if GNATprove_Mode then |
| null; |
| |
| else |
| Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ)); |
| |
| -- The component type should have an invariant procedure |
| -- if it has invariants of its own or inherits class-wide |
| -- invariants from parent or interface types. |
| |
| pragma Assert (Present (Proc_Id)); |
| |
| -- Generate: |
| -- <Comp_Typ>Invariant (T (_object).<Comp_Id>); |
| |
| -- Note that the invariant procedure may have a null body if |
| -- assertions are disabled or Assertion_Policy Ignore is in |
| -- effect. |
| |
| if not Has_Null_Body (Proc_Id) then |
| Append_New_To (Comp_Checks, |
| Make_Procedure_Call_Statement (Loc, |
| Name => |
| New_Occurrence_Of (Proc_Id, Loc), |
| Parameter_Associations => New_List ( |
| Make_Selected_Component (Loc, |
| Prefix => |
| Unchecked_Convert_To |
| (T, New_Occurrence_Of (Obj_Id, Loc)), |
| Selector_Name => |
| New_Occurrence_Of (Comp_Id, Loc))))); |
| end if; |
| end if; |
| |
| Produced_Check := True; |
| Produced_Component_Check := True; |
| end if; |
| |
| if Produced_Component_Check and then Has_Unchecked_Union (T) then |
| Error_Msg_NE |
| ("invariants cannot be checked on components of " |
| & "unchecked_union type &??", Comp_Id, T); |
| end if; |
| end Process_Record_Component; |
| |
| -- Local variables |
| |
| Comps : Node_Id; |
| Def : Node_Id; |
| |
| -- Start of processing for Add_Record_Component_Invariants |
| |
| begin |
| -- An untagged derived type inherits the components of its parent |
| -- type. In order to avoid creating redundant invariant checks, do |
| -- not process the components now. Instead wait until the ultimate |
| -- parent of the untagged derivation chain is reached. |
| |
| if not Is_Untagged_Derivation (T) then |
| Def := Type_Definition (Parent (T)); |
| |
| if Nkind (Def) = N_Derived_Type_Definition then |
| Def := Record_Extension_Part (Def); |
| end if; |
| |
| pragma Assert (Nkind (Def) = N_Record_Definition); |
| Comps := Component_List (Def); |
| |
| if Present (Comps) then |
| Process_Component_List |
| (Comp_List => Comps, |
| CL_Checks => Checks); |
| end if; |
| end if; |
| end Add_Record_Component_Invariants; |
| |
| -- Local variables |
| |
| Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; |
| Saved_IGR : constant Node_Id := Ignored_Ghost_Region; |
| -- Save the Ghost-related attributes to restore on exit |
| |
| Dummy : Entity_Id; |
| Priv_Item : Node_Id; |
| Proc_Body : Node_Id; |
| Proc_Body_Id : Entity_Id; |
| Proc_Decl : Node_Id; |
| Proc_Id : Entity_Id; |
| Stmts : List_Id := No_List; |
| |
| CRec_Typ : Entity_Id := Empty; |
| -- The corresponding record type of Full_Typ |
| |
| Full_Proc : Entity_Id := Empty; |
| -- The entity of the "full" invariant procedure |
| |
| 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 := Empty; |
| -- The working type |
| |
| -- Start of processing for Build_Invariant_Procedure_Body |
| |
| begin |
| Work_Typ := Typ; |
| |
| -- Do not process the underlying full view of a private type. There is |
| -- no way to get back to the partial view, plus the body will be built |
| -- by the full view or the base type. |
| |
| if Is_Underlying_Full_View (Work_Typ) then |
| return; |
| |
| -- The input type denotes the implementation base type of a constrained |
| -- array type. Work with the first subtype as all invariant pragmas are |
| -- on its rep item chain. |
| |
| elsif Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then |
| Work_Typ := First_Subtype (Work_Typ); |
| |
| -- The input type denotes the corresponding record type of a protected |
| -- or task type. Work with the concurrent type because the corresponding |
| -- record type may not be visible to clients of the type. |
| |
| elsif Ekind (Work_Typ) = E_Record_Type |
| and then Is_Concurrent_Record_Type (Work_Typ) |
| then |
| Work_Typ := Corresponding_Concurrent_Type (Work_Typ); |
| end if; |
| |
| -- The working type may be subject to pragma Ghost. Set the mode now to |
| -- ensure that the invariant procedure is properly marked as Ghost. |
| |
| Set_Ghost_Mode (Work_Typ); |
| |
| -- The type must either have invariants of its own, inherit class-wide |
| -- invariants from parent types or interfaces, or be an array or record |
| -- type whose components have invariants. |
| |
| pragma Assert (Has_Invariants (Work_Typ)); |
| |
| -- Interfaces are treated as the partial view of a private type in order |
| -- to achieve uniformity with the general case. |
| |
| if Is_Interface (Work_Typ) then |
| Priv_Typ := Work_Typ; |
| |
| -- Otherwise obtain both views of the type |
| |
| else |
| Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ); |
| end if; |
| |
| -- The caller requests a body for the partial invariant procedure |
| |
| if Partial_Invariant then |
| Full_Proc := Invariant_Procedure (Work_Typ); |
| Proc_Id := Partial_Invariant_Procedure (Work_Typ); |
| |
| -- The "full" invariant procedure body was already created |
| |
| if Present (Full_Proc) |
| and then Present |
| (Corresponding_Body (Unit_Declaration_Node (Full_Proc))) |
| then |
| -- This scenario happens only when the type is an untagged |
| -- derivation from a private parent and the underlying full |
| -- view was processed before the partial view. |
| |
| pragma Assert |
| (Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ)); |
| |
| -- Nothing to do because the processing of the underlying full |
| -- view already checked the invariants of the partial view. |
| |
| goto Leave; |
| end if; |
| |
| -- Create a declaration for the "partial" invariant procedure if it |
| -- is not available. |
| |
| if No (Proc_Id) then |
| Build_Invariant_Procedure_Declaration |
| (Typ => Work_Typ, |
| Partial_Invariant => True); |
| |
| Proc_Id := Partial_Invariant_Procedure (Work_Typ); |
| end if; |
| |
| -- The caller requests a body for the "full" invariant procedure |
| |
| else |
| Proc_Id := Invariant_Procedure (Work_Typ); |
| Part_Proc := Partial_Invariant_Procedure (Work_Typ); |
| |
| -- Create a declaration for the "full" invariant procedure if it is |
| -- not available. |
| |
| if No (Proc_Id) then |
| Build_Invariant_Procedure_Declaration (Work_Typ); |
| Proc_Id := Invariant_Procedure (Work_Typ); |
| end if; |
| end if; |
| |
| -- At this point there should be an invariant procedure declaration |
| |
| pragma Assert (Present (Proc_Id)); |
| Proc_Decl := Unit_Declaration_Node (Proc_Id); |
| |
| -- Nothing to do if the invariant procedure already has a body |
| |
| if Present (Corresponding_Body (Proc_Decl)) then |
| goto Leave; |
| end if; |
| |
| -- Emulate the environment of the invariant procedure by installing its |
| -- scope and formal parameters. Note that this is not needed, but having |
| -- the scope installed helps with the detection of invariant-related |
| -- errors. |
| |
| Push_Scope (Proc_Id); |
| Install_Formals (Proc_Id); |
| |
| Obj_Id := First_Formal (Proc_Id); |
| pragma Assert (Present (Obj_Id)); |
| |
| -- The "partial" invariant procedure verifies the invariants of the |
| -- partial view only. |
| |
| if Partial_Invariant then |
| pragma Assert (Present (Priv_Typ)); |
| |
| Add_Own_Invariants |
| (T => Priv_Typ, |
| Obj_Id => Obj_Id, |
| Checks => Stmts); |
| |
| -- Otherwise the "full" invariant procedure verifies the invariants of |
| -- the full view, all array or record components, as well as class-wide |
| -- invariants inherited from parent types or interfaces. In addition, it |
| -- indirectly verifies the invariants of the partial view by calling the |
| -- "partial" invariant procedure. |
| |
| else |
| pragma Assert (Present (Full_Typ)); |
| |
| -- Check the invariants of the partial view by calling the "partial" |
| -- invariant procedure. Generate: |
| |
| -- <Work_Typ>Partial_Invariant (_object); |
| |
| if Present (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)))); |
| |
| Produced_Check := True; |
| end if; |
| |
| Priv_Item := Empty; |
| |
| -- Derived subtypes do not have a partial view |
| |
| if Present (Priv_Typ) then |
| |
| -- The processing of the "full" invariant 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 invariants 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_Invariant => ...; |
| -- <underlying full view of Child> |
| -- end Pack_2; |
| |
| -- As a result, the processing of the full view must also consider |
| -- all invariants of the partial view. |
| |
| if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then |
| null; |
| |
| -- Otherwise the invariants of the partial view are ignored |
| |
| else |
| -- Note that the rep item chain is shared between the partial |
| -- and full views of a type. To avoid processing the invariants |
| -- of the partial view, signal the logic to stop when the first |
| -- rep item of the partial view has been reached. |
| |
| Priv_Item := First_Rep_Item (Priv_Typ); |
| |
| -- Ignore the invariants of the partial view by eliminating the |
| -- view. |
| |
| Priv_Typ := Empty; |
| end if; |
| end if; |
| |
| -- Process the invariants of the full view and in certain cases those |
| -- of the partial view. This also handles any invariants on array or |
| -- record components. |
| |
| Add_Own_Invariants |
| (T => Priv_Typ, |
| Obj_Id => Obj_Id, |
| Checks => Stmts, |
| Priv_Item => Priv_Item); |
| |
| Add_Own_Invariants |
| (T => Full_Typ, |
| Obj_Id => Obj_Id, |
| Checks => Stmts, |
| Priv_Item => Priv_Item); |
| |
| -- Process the elements of an array type |
| |
| if Is_Array_Type (Full_Typ) then |
| Add_Array_Component_Invariants (Full_Typ, Obj_Id, Stmts); |
| |
| -- Process the components of a record type |
| |
| elsif Ekind (Full_Typ) = E_Record_Type then |
| Add_Record_Component_Invariants (Full_Typ, Obj_Id, Stmts); |
| |
| -- Process the components of a corresponding record |
| |
| elsif Present (CRec_Typ) then |
| Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Stmts); |
| end if; |
| |
| -- Process the inherited class-wide invariants of all parent types. |
| -- This also handles any invariants on record components. |
| |
| Add_Parent_Invariants (Full_Typ, Obj_Id, Stmts); |
| |
| -- Process the inherited class-wide invariants of all implemented |
| -- interface types. |
| |
| Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts); |
| end if; |
| |
| End_Scope; |
| |
| -- At this point there should be at least one invariant check. If this |
| -- is not the case, then the invariant-related flags were not properly |
| -- set, or there is a missing invariant procedure on one of the array |
| -- or record components. |
| |
| pragma Assert (Produced_Check); |
| |
| -- Account for the case where assertions are disabled or all invariant |
| -- checks are subject to Assertion_Policy Ignore. Produce a completing |
| -- empty body. |
| |
| if No (Stmts) then |
| Stmts := New_List (Make_Null_Statement (Loc)); |
| end if; |
| |
| -- Generate: |
| -- procedure <Work_Typ>[Partial_]Invariant (_object : <Obj_Typ>) is |
| -- begin |
| -- <Stmts> |
| -- end <Work_Typ>[Partial_]Invariant; |
| |
| 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 |
| |
| Mutate_Ekind (Proc_Body_Id, E_Subprogram_Body); |
| Set_Etype (Proc_Body_Id, Standard_Void_Type); |
| Set_Scope (Proc_Body_Id, Current_Scope); |
| |
| -- 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 |
| -- invariants. |
| |
| 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 type |
| |
| else |
| Append_Freeze_Action (Work_Typ, Proc_Body); |
| end if; |
| |
| <<Leave>> |
| Restore_Ghost_Region (Saved_GM, Saved_IGR); |
| end Build_Invariant_Procedure_Body; |
| |
| ------------------------------------------- |
| -- Build_Invariant_Procedure_Declaration -- |
| ------------------------------------------- |
| |
| -- WARNING: This routine manages Ghost regions. Return statements must be |
| -- replaced by gotos which jump to the end of the routine and restore the |
| -- Ghost mode. |
| |
| procedure Build_Invariant_Procedure_Declaration |
| (Typ : Entity_Id; |
| Partial_Invariant : Boolean := False) |
| is |
| Loc : constant Source_Ptr := Sloc (Typ); |
| |
| Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; |
| Saved_IGR : constant Node_Id := Ignored_Ghost_Region; |
| -- Save the Ghost-related attributes to restore on exit |
| |
| Proc_Decl : Node_Id; |
| Proc_Id : Entity_Id; |
| Proc_Nam : Name_Id; |
| Typ_Decl : Node_Id; |
| |
| CRec_Typ : Entity_Id; |
| -- The corresponding record type of Full_Typ |
| |
| Full_Typ : Entity_Id; |
| -- The full view of working type |
| |
| Obj_Id : Entity_Id; |
| -- The _object formal parameter of the invariant procedure |
| |
| Obj_Typ : Entity_Id; |
| -- The type of the _object formal parameter |
| |
| Priv_Typ : Entity_Id; |
| -- The partial view of working type |
| |
| UFull_Typ : Entity_Id; |
| -- The underlying full view of Full_Typ |
| |
| Work_Typ : Entity_Id; |
| -- The working type |
| |
| begin |
| Work_Typ := Typ; |
| |
| -- The input type denotes the implementation base type of a constrained |
| -- array type. Work with the first subtype as all invariant pragmas are |
| -- on its rep item chain. |
| |
| if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then |
| Work_Typ := First_Subtype (Work_Typ); |
| |
| -- The input denotes the corresponding record type of a protected or a |
| -- task type. Work with the concurrent type because the corresponding |
| -- record type may not be visible to clients of the type. |
| |
| elsif Ekind (Work_Typ) = E_Record_Type |
| and then Is_Concurrent_Record_Type (Work_Typ) |
| then |
| Work_Typ := Corresponding_Concurrent_Type (Work_Typ); |
| end if; |
| |
| -- The working type may be subject to pragma Ghost. Set the mode now to |
| -- ensure that the invariant procedure is properly marked as Ghost. |
| |
| Set_Ghost_Mode (Work_Typ); |
| |
| -- The type must either have invariants of its own, inherit class-wide |
| -- invariants from parent or interface types, or be an array or record |
| -- type whose components have invariants. |
| |
| pragma Assert (Has_Invariants (Work_Typ)); |
| |
| -- Nothing to do if the type already has a "partial" invariant procedure |
| |
| if Partial_Invariant then |
| if Present (Partial_Invariant_Procedure (Work_Typ)) then |
| goto Leave; |
| end if; |
| |
| -- Nothing to do if the type already has a "full" invariant procedure |
| |
| elsif Present (Invariant_Procedure (Work_Typ)) then |
| goto Leave; |
| end if; |
| |
| -- The caller requests the declaration of the "partial" invariant |
| -- procedure. |
| |
| if Partial_Invariant then |
| Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_Invariant"); |
| |
| -- Otherwise the caller requests the declaration of the "full" invariant |
| -- procedure. |
| |
| else |
| Proc_Nam := New_External_Name (Chars (Work_Typ), "Invariant"); |
| end if; |
| |
| Proc_Id := Make_Defining_Identifier (Loc, Chars => Proc_Nam); |
| |
| -- Perform minor decoration in case the declaration is not analyzed |
| |
| Mutate_Ekind (Proc_Id, E_Procedure); |
| Set_Etype (Proc_Id, Standard_Void_Type); |
| Set_Scope (Proc_Id, Current_Scope); |
| |
| if Partial_Invariant then |
| Set_Is_Partial_Invariant_Procedure (Proc_Id); |
| Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id); |
| else |
| Set_Is_Invariant_Procedure (Proc_Id); |
| Set_Invariant_Procedure (Work_Typ, Proc_Id); |
| end if; |
| |
| -- The invariant procedure requires debug info when the invariants are |
| -- subject to Source Coverage Obligations. |
| |
| if Generate_SCO then |
| Set_Debug_Info_Needed (Proc_Id); |
| end if; |
| |
| -- Obtain all views of the input type |
| |
| Get_Views (Work_Typ, Priv_Typ, Full_Typ, UFull_Typ, CRec_Typ); |
| |
| -- Associate the invariant procedure and various flags with all views |
| |
| Propagate_Invariant_Attributes (Priv_Typ, From_Typ => Work_Typ); |
| Propagate_Invariant_Attributes (Full_Typ, From_Typ => Work_Typ); |
| Propagate_Invariant_Attributes (UFull_Typ, From_Typ => Work_Typ); |
| Propagate_Invariant_Attributes (CRec_Typ, From_Typ => Work_Typ); |
| |
| -- The declaration of the invariant procedure is inserted after the |
| -- declaration of the partial view as this allows for proper external |
| -- visibility. |
| |
| if Present (Priv_Typ) then |
| Typ_Decl := Declaration_Node (Priv_Typ); |
| |
| -- Anonymous arrays in object declarations have no explicit declaration |
| -- so use the related object declaration as the insertion point. |
| |
| elsif Is_Itype (Work_Typ) and then Is_Array_Type (Work_Typ) then |
| Typ_Decl := Associated_Node_For_Itype (Work_Typ); |
| |
| -- Derived types with the full view as parent do not have a partial |
| -- view. Insert the invariant procedure after the derived type. |
| |
| else |
| Typ_Decl := Declaration_Node (Full_Typ); |
| end if; |
| |
| -- The type should have a declarative node |
| |
| pragma Assert (Present (Typ_Decl)); |
| |
| -- Create the formal parameter which emulates the variable-like behavior |
| -- of the current type instance. |
| |
| Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject); |
| |
| -- When generating an invariant procedure declaration for an abstract |
| -- type (including interfaces), use the class-wide type as the _object |
| -- type. This has several desirable effects: |
| |
| -- * The invariant procedure does not become a primitive of the type. |
| -- This eliminates the need to either special case the treatment of |
| -- invariant procedures, or to make it a predefined primitive and |
| -- force every derived type to potentially provide an empty body. |
| |
| -- * The invariant procedure does not need to be declared as abstract. |
| -- This allows for a proper body, which in turn avoids redundant |
| -- processing of the same invariants for types with multiple views. |
| |
| -- * The class-wide type allows for calls to abstract primitives |
| -- within a nonabstract subprogram. The calls are treated as |
| -- dispatching and require additional processing when they are |
| -- remapped to call primitives of derived types. See routine |
| -- Replace_References for details. |
| |
| if Is_Abstract_Type (Work_Typ) then |
| Obj_Typ := Class_Wide_Type (Work_Typ); |
| else |
| Obj_Typ := Work_Typ; |
| end if; |
| |
| -- Perform minor decoration in case the declaration is not analyzed |
| |
| Mutate_Ekind (Obj_Id, E_In_Parameter); |
| Set_Etype (Obj_Id, Obj_Typ); |
| Set_Scope (Obj_Id, Proc_Id); |
| |
| Set_First_Entity (Proc_Id, Obj_Id); |
| Set_Last_Entity (Proc_Id, Obj_Id); |
| |
| -- Generate: |
| -- procedure <Work_Typ>[Partial_]Invariant (_object : <Obj_Typ>); |
| |
| Proc_Decl := |
| Make_Subprogram_Declaration (Loc, |
| Specification => |
| Make_Procedure_Specification (Loc, |
| Defining_Unit_Name => Proc_Id, |
| Parameter_Specifications => New_List ( |
| Make_Parameter_Specification (Loc, |
| Defining_Identifier => Obj_Id, |
| Parameter_Type => New_Occurrence_Of (Obj_Typ, Loc))))); |
| |
| -- The declaration should not be inserted into the tree when the context |
| -- is a generic unit because it is not part of the template. |
| |
| if Inside_A_Generic then |
| null; |
| |
| -- Semi-insert the declaration into the tree for GNATprove by setting |
| -- its Parent field. This allows for proper upstream tree traversals. |
| |
| elsif GNATprove_Mode then |
| Set_Parent (Proc_Decl, Parent (Typ_Decl)); |
| |
| -- Otherwise insert the declaration |
| |
| else |
| pragma Assert (Present (Typ_Decl)); |
| Insert_After_And_Analyze (Typ_Decl, Proc_Decl); |
| end if; |
| |
| <<Leave>> |
| Restore_Ghost_Region (Saved_GM, Saved_IGR); |
| end Build_Invariant_Procedure_Declaration; |
| |
| -------------------------- |
| -- Build_Procedure_Form -- |
| -------------------------- |
| |
| procedure Build_Procedure_Form (N : Node_Id) is |
| Loc : constant Source_Ptr := Sloc (N); |
| Subp : constant Entity_Id := Defining_Entity (N); |
| |
| Func_Formal : Entity_Id; |
| Proc_Formals : List_Id; |
| Proc_Decl : Node_Id; |
| |
| begin |
| -- No action needed if this transformation was already done, or in case |
| -- of subprogram renaming declarations. |
| |
| if Nkind (Specification (N)) = N_Procedure_Specification |
| or else Nkind (N) = N_Subprogram_Renaming_Declaration |
| then |
| return; |
| end if; |
| |
| -- Ditto when dealing with an expression function, where both the |
| -- original expression and the generated declaration end up being |
| -- expanded here. |
| |
| if Rewritten_For_C (Subp) then |
| return; |
| end if; |
| |
| Proc_Formals := New_List; |
| |
| -- Create a list of formal parameters with the same types as the |
| -- function. |
| |
| Func_Formal := First_Formal (Subp); |
| while Present (Func_Formal) loop |
| Append_To (Proc_Formals, |
| Make_Parameter_Specification (Loc, |
| Defining_Identifier => |
| Make_Defining_Identifier (Loc, Chars (Func_Formal)), |
| Parameter_Type => |
| New_Occurrence_Of (Etype (Func_Formal), Loc))); |
| |
| Next_Formal (Func_Formal); |
| end loop; |
| |
| -- Add an extra out parameter to carry the function result |
| |
| Append_To (Proc_Formals, |
| Make_Parameter_Specification (Loc, |
| Defining_Identifier => |
| Make_Defining_Identifier (Loc, Name_UP_RESULT), |
| Out_Present => True, |
| Parameter_Type => New_Occurrence_Of (Etype (Subp), Loc))); |
| |
| -- The new procedure declaration is inserted before the function |
| -- declaration. The processing in Build_Procedure_Body_Form relies on |
| -- this order. Note that we insert before because in the case of a |
| -- function body with no separate spec, we do not want to insert the |
| -- new spec after the body which will later get rewritten. |
| |
| Proc_Decl := |
| Make_Subprogram_Declaration (Loc, |
| Specification => |
| Make_Procedure_Specification (Loc, |
| Defining_Unit_Name => |
| Make_Defining_Identifier (Loc, Chars (Subp)), |
| Parameter_Specifications => Proc_Formals)); |
| |
| Insert_Before_And_Analyze (Unit_Declaration_Node (Subp), Proc_Decl); |
| |
| -- Entity of procedure must remain invisible so that it does not |
| -- overload subsequent references to the original function. |
| |
| Set_Is_Immediately_Visible (Defining_Entity (Proc_Decl), False); |
| |
| -- Mark the function as having a procedure form and link the function |
| -- and its internally built procedure. |
| |
| Set_Rewritten_For_C (Subp); |
| Set_Corresponding_Procedure (Subp, Defining_Entity (Proc_Decl)); |
| Set_Corresponding_Function (Defining_Entity (Proc_Decl), Subp); |
| end Build_Procedure_Form; |
| |
| ------------------------ |
| -- Build_Runtime_Call -- |
| ------------------------ |
| |
| function Build_Runtime_Call (Loc : Source_Ptr; RE : RE_Id) return Node_Id is |
| begin |
| -- If entity is not available, we can skip making the call (this avoids |
| -- junk duplicated error messages in a number of cases). |
| |
| if not RTE_Available (RE) then |
| return Make_Null_Statement (Loc); |
| else |
| return |
| Make_Procedure_Call_Statement (Loc, |
| Name => New_Occurrence_Of (RTE (RE), Loc)); |
| end if; |
| end Build_Runtime_Call; |
| |
| ------------------------ |
| -- Build_SS_Mark_Call -- |
| ------------------------ |
| |
| function Build_SS_Mark_Call |
| (Loc : Source_Ptr; |
| Mark : Entity_Id) return Node_Id |
| is |
| begin |
| -- Generate: |
| -- Mark : constant Mark_Id := SS_Mark; |
| |
| return |
| Make_Object_Declaration (Loc, |
| Defining_Identifier => Mark, |
| Constant_Present => True, |
| Object_Definition => |
| New_Occurrence_Of (RTE (RE_Mark_Id), Loc), |
| Expression => |
| Make_Function_Call (Loc, |
| Name => New_Occurrence_Of (RTE (RE_SS_Mark), Loc))); |
| end Build_SS_Mark_Call; |
| |
| --------------------------- |
| -- Build_SS_Release_Call -- |
| --------------------------- |
| |
| function Build_SS_Release_Call |
| (Loc : Source_Ptr; |
| Mark : Entity_Id) return Node_Id |
| is |
| begin |
| -- Generate: |
| -- SS_Release (Mark); |
| |
| return |
| Make_Procedure_Call_Statement (Loc, |
| Name => |
| New_Occurrence_Of (RTE (RE_SS_Release), Loc), |
| Parameter_Associations => New_List ( |
| New_Occurrence_Of (Mark, Loc))); |
| end Build_SS_Release_Call; |
| |
| ---------------------------- |
| -- Build_Task_Array_Image -- |
| ---------------------------- |
| |
| -- This function generates the body for a function that constructs the |
| -- image string for a task that is an array component. The function is |
| -- local to the init proc for the array type, and is called for each one |
| -- of the components. The constructed image has the form of an indexed |
| -- component, whose prefix is the outer variable of the array type. |
| -- The n-dimensional array type has known indexes Index, Index2... |
| |
| -- Id_Ref is an indexed component form created by the enclosing init proc. |
| -- Its successive indexes are Val1, Val2, ... which are the loop variables |
| -- in the loops that call the individual task init proc on each component. |
| |
| -- The generated function has the following structure: |
| |
| -- function F return String is |
| -- Pref : string renames Task_Name; |
| -- T1 : String := Index1'Image (Val1); |
| -- ... |
| -- Tn : String := indexn'image (Valn); |
| -- Len : Integer := T1'Length + ... + Tn'Length + n + 1; |
| -- -- Len includes commas and the end parentheses. |
| -- Res : String (1..Len); |
| -- Pos : Integer := Pref'Length; |
| -- |
| -- begin |
| -- Res (1 .. Pos) := Pref; |
| -- Pos := Pos + 1; |
| -- Res (Pos) := '('; |
| -- Pos := Pos + 1; |
| -- Res (Pos .. Pos + T1'Length - 1) := T1; |
| -- Pos := Pos + T1'Length; |
| -- Res (Pos) := '.'; |
| -- Pos := Pos + 1; |
| -- ... |
| -- Res (Pos .. Pos + Tn'Length - 1) := Tn; |
| -- Res (Len) := ')'; |
| -- |
| -- return Res; |
| -- end F; |
| -- |
| -- Needless to say, multidimensional arrays of tasks are rare enough that |
| -- the bulkiness of this code is not really a concern. |
| |
| function Build_Task_Array_Image |
| (Loc : Source_Ptr; |
| Id_Ref : Node_Id; |
| A_Type : Entity_Id; |
| Dyn : Boolean := False) return Node_Id |
| is |
| Dims : constant Nat := Number_Dimensions (A_Type); |
| -- Number of dimensions for array of tasks |
| |
| Temps : array (1 .. Dims) of Entity_Id; |
| -- Array of temporaries to hold string for each index |
| |
| Indx : Node_Id; |
| -- Index expression |
| |
| Len : Entity_Id; |
| -- Total length of generated name |
| |
| Pos : Entity_Id; |
| -- Running index for substring assignments |
| |
| Pref : constant Entity_Id := Make_Temporary (Loc, 'P'); |
| -- Name of enclosing variable, prefix of resulting name |
| |
| Res : Entity_Id; |
| -- String to hold result |
| |
| Val : Node_Id; |
| -- Value of successive indexes |
| |
| Sum : Node_Id; |
| -- Expression to compute total size of string |
| |
| T : Entity_Id; |
| -- Entity for name at one index position |
| |
| Decls : constant List_Id := New_List; |
| Stats : constant List_Id := New_List; |
| |
| begin |
| -- For a dynamic task, the name comes from the target variable. For a |
| -- static one it is a formal of the enclosing init proc. |
| |
| if Dyn then |
| Get_Name_String (Chars (Entity (Prefix (Id_Ref)))); |
| Append_To (Decls, |
| Make_Object_Declaration (Loc, |
| Defining_Identifier => Pref, |
| Object_Definition => New_Occurrence_Of (Standard_String, Loc), |
| Expression => |
| Make_String_Literal (Loc, |
| Strval => String_From_Name_Buffer))); |
| |
| else |
| Append_To (Decls, |
| Make_Object_Renaming_Declaration (Loc, |
| Defining_Identifier => Pref, |
| Subtype_Mark => New_Occurrence_Of (Standard_String, Loc), |
| Name => Make_Identifier (Loc, Name_uTask_Name))); |
| end if; |
| |
| Indx := First_Index (A_Type); |
| Val := First (Expressions (Id_Ref)); |
| |
| for J in 1 .. Dims loop |
| T := Make_Temporary (Loc, 'T'); |
| Temps (J) := T; |
| |
| Append_To (Decls, |
| Make_Object_Declaration (Loc, |
| Defining_Identifier => T, |
| Object_Definition => New_Occurrence_Of (Standard_String, Loc), |
| Expression => |
| Make_Attribute_Reference (Loc, |
| Attribute_Name => Name_Image, |
| Prefix => New_Occurrence_Of (Etype (Indx), Loc), |
| Expressions => New_List (New_Copy_Tree (Val))))); |
| |
| Next_Index (Indx); |
| Next (Val); |
| end loop; |
| |
| Sum := Make_Integer_Literal (Loc, Dims + 1); |
| |
| Sum := |
| Make_Op_Add (Loc, |
| Left_Opnd => Sum, |
| Right_Opnd => |
| Make_Attribute_Reference (Loc, |
| Attribute_Name => Name_Length, |
| Prefix => New_Occurrence_Of (Pref, Loc), |
| Expressions => New_List (Make_Integer_Literal (Loc, 1)))); |
| |
| for J in 1 .. Dims loop |
| Sum := |
| Make_Op_Add (Loc, |
| Left_Opnd => Sum, |
| Right_Opnd => |
| Make_Attribute_Reference (Loc, |
| Attribute_Name => Name_Length, |
| Prefix => |
| New_Occurrence_Of (Temps (J), Loc), |
| Expressions => New_List (Make_Integer_Literal (Loc, 1)))); |
| end loop; |
| |
| Build_Task_Image_Prefix (Loc, Len, Res, Pos, Pref, Sum, Decls, Stats); |
| |
| Set_Character_Literal_Name (Char_Code (Character'Pos ('('))); |
| |
| Append_To (Stats, |
| Make_Assignment_Statement (Loc, |
| Name => |
| Make_Indexed_Component (Loc, |
| Prefix => New_Occurrence_Of (Res, Loc), |
| Expressions => New_List (New_Occurrence_Of (Pos, Loc))), |
| Expression => |
| Make_Character_Literal (Loc, |
| Chars => Name_Find, |
| Char_Literal_Value => UI_From_Int (Character'Pos ('('))))); |
| |
| Append_To (Stats, |
| Make_Assignment_Statement (Loc, |
| Name => New_Occurrence_Of (Pos, Loc), |
| Expression => |
| Make_Op_Add (Loc, |
| Left_Opnd => New_Occurrence_Of (Pos, Loc), |
| Right_Opnd => Make_Integer_Literal (Loc, 1)))); |
| |
| for J in 1 .. Dims loop |
| |
| Append_To (Stats, |
| Make_Assignment_Statement (Loc, |
| Name => |
| Make_Slice (Loc, |
| Prefix => New_Occurrence_Of (Res, Loc), |
| Discrete_Range => |
| Make_Range (Loc, |
| Low_Bound => New_Occurrence_Of (Pos, Loc), |
| High_Bound => |
| Make_Op_Subtract (Loc, |
| Left_Opnd => |
| Make_Op_Add (Loc, |
| Left_Opnd => New_Occurrence_Of (Pos, Loc), |
| Right_Opnd => |
| Make_Attribute_Reference (Loc, |
| Attribute_Name => Name_Length, |
| Prefix => |
| New_Occurrence_Of (Temps (J), Loc), |
| Expressions => |
| New_List (Make_Integer_Literal (Loc, 1)))), |
| Right_Opnd => Make_Integer_Literal (Loc, 1)))), |
| |
| Expression => New_Occurrence_Of (Temps (J), Loc))); |
| |
| if J < Dims then |
| Append_To (Stats, |
| Make_Assignment_Statement (Loc, |
| Name => New_Occurrence_Of (Pos, Loc), |
| Expression => |
| Make_Op_Add (Loc, |
| Left_Opnd => New_Occurrence_Of (Pos, Loc), |
| Right_Opnd => |
| Make_Attribute_Reference (Loc, |
| Attribute_Name => Name_Length, |
| Prefix => New_Occurrence_Of (Temps (J), Loc), |
| Expressions => |
| New_List (Make_Integer_Literal (Loc, 1)))))); |
| |
| Set_Character_Literal_Name (Char_Code (Character'Pos (','))); |
| |
| Append_To (Stats, |
| Make_Assignment_Statement (Loc, |
| Name => Make_Indexed_Component (Loc, |
| Prefix => New_Occurrence_Of (Res, Loc), |
| Expressions => New_List (New_Occurrence_Of (Pos, Loc))), |
| Expression => |
| Make_Character_Literal (Loc, |
| Chars => Name_Find, |
| Char_Literal_Value => UI_From_Int (Character'Pos (','))))); |
| |
| Append_To (Stats, |
| Make_Assignment_Statement (Loc, |
| Name => New_Occurrence_Of (Pos, Loc), |
| Expression => |
| Make_Op_Add (Loc, |
| Left_Opnd => New_Occurrence_Of (Pos, Loc), |
| Right_Opnd => Make_Integer_Literal (Loc, 1)))); |
| end if; |
| end loop; |
| |
| Set_Character_Literal_Name (Char_Code (Character'Pos (')'))); |
| |
| Append_To (Stats, |
| Make_Assignment_Statement (Loc, |
| Name => |
| Make_Indexed_Component (Loc, |
| Prefix => New_Occurrence_Of (Res, Loc), |
| Expressions => New_List (New_Occurrence_Of (Len, Loc))), |
| Expression => |
| Make_Character_Literal (Loc, |
| Chars => Name_Find, |
| Char_Literal_Value => UI_From_Int (Character'Pos (')'))))); |
| return Build_Task_Image_Function (Loc, Decls, Stats, Res); |
| end Build_Task_Array_Image; |
| |
| ---------------------------- |
| -- Build_Task_Image_Decls -- |
| ---------------------------- |
| |
| function Build_Task_Image_Decls |
| (Loc : Source_Ptr; |
| Id_Ref : Node_Id; |
| A_Type : Entity_Id; |
| In_Init_Proc : Boolean := False) return List_Id |
| is |
| Decls : constant List_Id := New_List; |
| T_Id : Entity_Id := Empty; |
| Decl : Node_Id; |
| Expr : Node_Id := Empty; |
| Fun : Node_Id := Empty; |
| Is_Dyn : constant Boolean := |
| Nkind (Parent (Id_Ref)) = N_Assignment_Statement |
| and then |
| Nkind (Expression (Parent (Id_Ref))) = N_Allocator; |
| |
| begin |
| -- If Discard_Names or No_Implicit_Heap_Allocations are in effect, |
| -- generate a dummy declaration only. |
| |
| if Restriction_Active (No_Implicit_Heap_Allocations) |
| or else Global_Discard_Names |
| then |
| T_Id := Make_Temporary (Loc, 'J'); |
| Name_Len := 0; |
| |
| return |
| New_List ( |
| Make_Object_Declaration (Loc, |
| Defining_Identifier => T_Id, |
| Object_Definition => New_Occurrence_Of (Standard_String, Loc), |
| Expression => |
| Make_String_Literal (Loc, |
| Strval => String_From_Name_Buffer))); |
| |
| else |
| if Nkind (Id_Ref) = N_Identifier |
| or else Nkind (Id_Ref) = N_Defining_Identifier |
| then |
| -- For a simple variable, the image of the task is built from |
| -- the name of the variable. To avoid possible conflict with the |
| -- anonymous type created for a single protected object, add a |
| -- numeric suffix. |
| |
| T_Id := |
| Make_Defining_Identifier (Loc, |
| New_External_Name (Chars (Id_Ref), 'T', 1)); |
| |
| Get_Name_String (Chars (Id_Ref)); |
| |
| Expr := |
| Make_String_Literal (Loc, |
| Strval => String_From_Name_Buffer); |
| |
| elsif Nkind (Id_Ref) = N_Selected_Component then |
| T_Id := |
| Make_Defining_Identifier (Loc, |
| New_External_Name (Chars (Selector_Name (Id_Ref)), 'T')); |
| Fun := Build_Task_Record_Image (Loc, Id_Ref, Is_Dyn); |
| |
| elsif Nkind (Id_Ref) = N_Indexed_Component then
|