blob: c344dc1e7062af89c94a4ec718c1d20b67b8c0d1 [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- E X P _ S P A R K --
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2023, 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 Atree; use Atree;
with Checks; use Checks;
with Einfo; use Einfo;
with Einfo.Entities; use Einfo.Entities;
with Einfo.Utils; use Einfo.Utils;
with Exp_Attr;
with Exp_Ch3;
with Exp_Ch4;
with Exp_Ch5; use Exp_Ch5;
with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
with Ghost; use Ghost;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
with Opt; use Opt;
with Restrict; use Restrict;
with Rident; use Rident;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8;
with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
with Sinfo.Utils; use Sinfo.Utils;
with Snames; use Snames;
with Stand; use Stand;
with Tbuild; use Tbuild;
with Uintp; use Uintp;
package body Exp_SPARK is
-----------------------
-- Local Subprograms --
-----------------------
procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
-- Perform attribute-reference-specific expansion
procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id);
-- Perform delta-aggregate-specific expansion
procedure Expand_SPARK_N_Freeze_Entity (N : Node_Id);
-- Do a minimal expansion of freeze entities required by GNATprove. It is
-- a subset of what is done for GNAT in Exp_Ch13.Expand_N_Freeze_Entity.
-- Those two routines should be kept in sync.
procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
-- Perform loop-statement-specific expansion
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
-- Perform object-declaration-specific expansion
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
-- Perform name evaluation for a renamed object
procedure Expand_SPARK_N_Op_Ne (N : Node_Id);
-- Rewrite operator /= based on operator = when defined explicitly
procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id);
-- Common expansion for attribute Update and delta aggregates
procedure SPARK_Freeze_Type (N : Node_Id);
-- Do a minimal type freezing required by GNATprove. It is a subset of what
-- is done for GNAT in Exp_Ch3.Freeze_Type. Those two routines should be
-- kept in sync.
--
-- Currently in freezing we build the spec of dispatching equality. This
-- spec is needed to properly resolve references to the equality operator.
-- The body is not needed, because proof knows how to directly synthesize a
-- logical meaning for it. Also, for tagged types with extension the
-- expanded body would compare the _parent component, which is
-- intentionally not generated in the GNATprove mode.
--
-- We build the DIC and Type_Invariant procedure bodies here as well.
------------------
-- Expand_SPARK --
------------------
procedure Expand_SPARK (N : Node_Id) is
begin
case Nkind (N) is
-- Qualification of entity names in formal verification mode
-- is limited to the addition of a suffix for homonyms (see
-- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
-- as full expansion does, but this was removed as this prevents the
-- verification back-end from using a short name for debugging and
-- user interaction. The verification back-end already takes care
-- of qualifying names when needed.
when N_Block_Statement
| N_Entry_Declaration
| N_Package_Body
| N_Package_Declaration
| N_Protected_Type_Declaration
| N_Subprogram_Body
| N_Task_Type_Declaration
=>
Qualify_Entity_Names (N);
-- Replace occurrences of System'To_Address by calls to
-- System.Storage_Elements.To_Address.
when N_Attribute_Reference =>
Expand_SPARK_N_Attribute_Reference (N);
when N_Delta_Aggregate =>
Expand_SPARK_N_Delta_Aggregate (N);
when N_Expanded_Name
| N_Identifier
=>
Expand_SPARK_Potential_Renaming (N);
-- Loop iterations over arrays need to be expanded, to avoid getting
-- two names referring to the same object in memory (the array and
-- the iterator) in GNATprove, especially since both can be written
-- (thus possibly leading to interferences due to aliasing). No such
-- problem arises with quantified expressions over arrays, which are
-- dealt with specially in GNATprove.
when N_Loop_Statement =>
Expand_SPARK_N_Loop_Statement (N);
when N_Object_Declaration =>
Expand_SPARK_N_Object_Declaration (N);
when N_Object_Renaming_Declaration =>
Expand_SPARK_N_Object_Renaming_Declaration (N);
when N_Op_Ne =>
Expand_SPARK_N_Op_Ne (N);
when N_Freeze_Entity =>
-- Currently we only expand type freeze entities, so ignore other
-- freeze entites, because it is expensive to create a suitable
-- freezing environment.
if Is_Type (Entity (N)) then
Expand_SPARK_N_Freeze_Entity (N);
end if;
-- In SPARK mode, no other constructs require expansion
when others =>
null;
end case;
end Expand_SPARK;
----------------------------------
-- Expand_SPARK_Delta_Or_Update --
----------------------------------
procedure Expand_SPARK_Delta_Or_Update
(Typ : Entity_Id;
Aggr : Node_Id)
is
Assoc : Node_Id;
Comp : Node_Id;
Comp_Id : Entity_Id;
Comp_Type : Entity_Id;
Expr : Node_Id;
Index : Node_Id;
Index_Typ : Entity_Id;
New_Assoc : Node_Id;
begin
-- Apply scalar range checks on the updated components, if needed
if Is_Array_Type (Typ) then
-- Multidimensional arrays
if Present (Next_Index (First_Index (Typ))) then
Assoc := First (Component_Associations (Aggr));
while Present (Assoc) loop
Expr := Expression (Assoc);
Comp_Type := Component_Type (Typ);
if Is_Scalar_Type (Comp_Type) then
Apply_Scalar_Range_Check (Expr, Comp_Type);
end if;
-- The current association contains a sequence of indexes
-- denoting an element of a multidimensional array:
--
-- (Index_1, ..., Index_N)
Expr := First (Choices (Assoc));
pragma Assert (Nkind (Aggr) = N_Aggregate);
while Present (Expr) loop
Index := First (Expressions (Expr));
Index_Typ := First_Index (Typ);
while Present (Index_Typ) loop
Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
Next (Index);
Next_Index (Index_Typ);
end loop;
Next (Expr);
end loop;
Next (Assoc);
end loop;
-- One-dimensional arrays
else
Assoc := First (Component_Associations (Aggr));
while Present (Assoc) loop
Expr := Expression (Assoc);
Comp_Type := Component_Type (Typ);
-- Analyze expression of the iterated_component_association
-- with its index parameter in scope.
if Nkind (Assoc) = N_Iterated_Component_Association then
Push_Scope (Scope (Defining_Identifier (Assoc)));
Enter_Name (Defining_Identifier (Assoc));
Analyze_And_Resolve (Expr, Comp_Type);
end if;
if Is_Scalar_Type (Comp_Type) then
Apply_Scalar_Range_Check (Expr, Comp_Type);
end if;
-- Restore scope of the iterated_component_association
if Nkind (Assoc) = N_Iterated_Component_Association then
End_Scope;
end if;
Index := First (Choice_List (Assoc));
Index_Typ := First_Index (Typ);
while Present (Index) loop
-- If the index denotes a range of elements or a constrained
-- subtype indication, then their low and high bounds
-- already have range checks applied.
if Nkind (Index) in N_Range | N_Subtype_Indication then
null;
-- Otherwise the index denotes a single expression where
-- range checks need to be applied or a subtype name
-- (without range constraints) where applying checks is
-- harmless.
--
-- In delta_aggregate and Update attribute on array the
-- others_choice is not allowed.
else pragma Assert (Nkind (Index) in N_Subexpr);
Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
end if;
Next (Index);
end loop;
Next (Assoc);
end loop;
end if;
else pragma Assert (Is_Record_Type (Typ));
-- If the aggregate has multiple component choices, e.g.:
--
-- X'Update (A | B | C => 123)
--
-- then each component might be of a different type and might or
-- might not require a range check. We first rewrite associations
-- into single-component choices, e.g.:
--
-- X'Update (A => 123, B => 123, C => 123)
--
-- and then apply range checks to individual copies of the
-- expressions. We do the same for delta aggregates, accordingly.
-- Iterate over associations of the original aggregate
Assoc := First (Component_Associations (Aggr));
-- Rewrite into a new aggregate and decorate
case Nkind (Aggr) is
when N_Aggregate =>
Rewrite
(Aggr,
Make_Aggregate
(Sloc => Sloc (Aggr),
Component_Associations => New_List));
when N_Delta_Aggregate =>
Rewrite
(Aggr,
Make_Delta_Aggregate
(Sloc => Sloc (Aggr),
Expression => Expression (Aggr),
Component_Associations => New_List));
when others =>
raise Program_Error;
end case;
Set_Etype (Aggr, Typ);
-- Populate the new aggregate with component associations
while Present (Assoc) loop
Expr := Expression (Assoc);
Comp := First (Choices (Assoc));
while Present (Comp) loop
Comp_Id := Entity (Comp);
Comp_Type := Etype (Comp_Id);
New_Assoc :=
Make_Component_Association
(Sloc => Sloc (Assoc),
Choices =>
New_List
(New_Occurrence_Of (Comp_Id, Sloc (Comp))),
Expression => New_Copy_Tree (Expr));
-- New association must be attached to the aggregate before we
-- analyze it.
Append (New_Assoc, Component_Associations (Aggr));
Analyze_And_Resolve (Expression (New_Assoc), Comp_Type);
if Is_Scalar_Type (Comp_Type) then
Apply_Scalar_Range_Check
(Expression (New_Assoc), Comp_Type);
end if;
Next (Comp);
end loop;
Next (Assoc);
end loop;
end if;
end Expand_SPARK_Delta_Or_Update;
----------------------------------
-- Expand_SPARK_N_Freeze_Entity --
----------------------------------
procedure Expand_SPARK_N_Freeze_Entity (N : Entity_Id) is
E : constant Entity_Id := Entity (N);
Action : Node_Id;
E_Scope : Entity_Id;
In_Other_Scope : Boolean;
In_Outer_Scope : Boolean;
begin
-- Here E is a type or a subprogram
E_Scope := Scope (E);
-- This is an error protection against previous errors
if No (E_Scope) then
Check_Error_Detected;
return;
end if;
-- The entity may be a subtype declared for a constrained record
-- component, in which case the relevant scope is the scope of
-- the record. This happens for class-wide subtypes created for
-- a constrained type extension with inherited discriminants.
if Is_Type (E_Scope)
and then not Is_Concurrent_Type (E_Scope)
then
E_Scope := Scope (E_Scope);
-- The entity may be a subtype declared for an iterator
elsif Ekind (E_Scope) = E_Loop then
E_Scope := Scope (E_Scope);
end if;
-- If we are freezing entities defined in protected types, they belong
-- in the enclosing scope, given that the original type has been
-- expanded away. The same is true for entities in task types, in
-- particular the parameter records of entries (Entities in bodies are
-- all frozen within the body). If we are in the task body, this is a
-- proper scope. If we are within a subprogram body, the proper scope
-- is the corresponding spec. This may happen for itypes generated in
-- the bodies of protected operations.
if Ekind (E_Scope) = E_Protected_Type
or else (Ekind (E_Scope) = E_Task_Type
and then not Has_Completion (E_Scope))
then
E_Scope := Scope (E_Scope);
elsif Ekind (E_Scope) = E_Subprogram_Body then
E_Scope := Corresponding_Spec (Unit_Declaration_Node (E_Scope));
end if;
-- If the scope of the entity is in open scopes, it is the current one
-- or an enclosing one, including a loop, a block, or a subprogram.
if In_Open_Scopes (E_Scope) then
In_Other_Scope := False;
In_Outer_Scope := E_Scope /= Current_Scope;
-- Otherwise it is a local package or a different compilation unit
else
In_Other_Scope := True;
In_Outer_Scope := False;
end if;
-- If the entity being frozen is defined in a scope that is not
-- currently on the scope stack, we must establish the proper
-- visibility before freezing the entity and related subprograms.
if In_Other_Scope then
Push_Scope (E_Scope);
-- Finalizers are little odd in terms of freezing. The spec of the
-- procedure appears in the declarations while the body appears in
-- the statement part of a single construct. Since the finalizer must
-- be called by the At_End handler of the construct, the spec is
-- manually frozen right after its declaration. The only side effect
-- of this action appears in contexts where the construct is not in
-- its final resting place. These contexts are:
-- * Entry bodies - The declarations and statements are moved to
-- the procedure equivalen of the entry.
-- * Protected subprograms - The declarations and statements are
-- moved to the non-protected version of the subprogram.
-- * Task bodies - The declarations and statements are moved to the
-- task body procedure.
-- * Blocks that will be rewritten as subprograms when unnesting
-- is in effect.
-- Visible declarations do not need to be installed in these three
-- cases since it does not make semantic sense to do so. All entities
-- referenced by a finalizer are visible and already resolved, plus
-- the enclosing scope may not have visible declarations at all.
if Ekind (E) = E_Procedure
and then Is_Finalizer (E)
and then
(Is_Entry (E_Scope)
or else (Is_Subprogram (E_Scope)
and then Is_Protected_Type (Scope (E_Scope)))
or else Is_Task_Type (E_Scope)
or else Ekind (E_Scope) = E_Block)
then
null;
else
Install_Visible_Declarations (E_Scope);
end if;
if Is_Concurrent_Type (E_Scope)
or else Is_Package_Or_Generic_Package (E_Scope)
then
Install_Private_Declarations (E_Scope);
end if;
-- If the entity is in an outer scope, then that scope needs to
-- temporarily become the current scope so that operations created
-- during type freezing will be declared in the right scope and
-- can properly override any corresponding inherited operations.
elsif In_Outer_Scope then
Push_Scope (E_Scope);
end if;
-- Remember that we are processing a freezing entity and its freezing
-- nodes. This flag (non-zero = set) is used to avoid the need of
-- climbing through the tree while processing the freezing actions (ie.
-- to avoid generating spurious warnings or to avoid killing constant
-- indications while processing the code associated with freezing
-- actions). We use a counter to deal with nesting.
Inside_Freezing_Actions := Inside_Freezing_Actions + 1;
-- Currently only types require freezing in SPARK
SPARK_Freeze_Type (N);
-- Analyze actions in freeze node, if any
Action := First (Actions (N));
while Present (Action) loop
Analyze (Action);
Next (Action);
end loop;
-- Pop scope if we installed one for the analysis
if In_Other_Scope then
if Ekind (Current_Scope) = E_Package then
End_Package_Scope (E_Scope);
else
End_Scope;
end if;
elsif In_Outer_Scope then
Pop_Scope;
end if;
-- Restore previous value of the nesting-level counter that records
-- whether we are inside a (possibly nested) call to this procedure.
Inside_Freezing_Actions := Inside_Freezing_Actions - 1;
end Expand_SPARK_N_Freeze_Entity;
----------------------------------------
-- Expand_SPARK_N_Attribute_Reference --
----------------------------------------
procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
Aname : constant Name_Id := Attribute_Name (N);
Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
Loc : constant Source_Ptr := Sloc (N);
Pref : constant Node_Id := Prefix (N);
Typ : constant Entity_Id := Etype (N);
Expr : Node_Id;
begin
case Attr_Id is
when Attribute_To_Address =>
-- Extract and convert argument to expected type for call
Expr :=
Make_Type_Conversion (Loc,
Subtype_Mark =>
New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
Expression => Relocate_Node (First (Expressions (N))));
-- Replace attribute reference with call
Rewrite
(N,
Make_Function_Call (Loc,
Name =>
New_Occurrence_Of (RTE (RE_To_Address), Loc),
Parameter_Associations => New_List (Expr)));
Analyze_And_Resolve (N, Typ);
when Attribute_Object_Size
| Attribute_Size
| Attribute_Value_Size
| Attribute_VADS_Size
=>
Exp_Attr.Expand_Size_Attribute (N);
-- For attributes which return Universal_Integer, introduce a
-- conversion to the expected type with the appropriate check flags
-- set.
when Attribute_Aft
| Attribute_Alignment
| Attribute_Bit
| Attribute_Bit_Position
| Attribute_Descriptor_Size
| Attribute_First_Bit
| Attribute_Last_Bit
| Attribute_Length
| Attribute_Max_Alignment_For_Allocation
| Attribute_Max_Size_In_Storage_Elements
| Attribute_Pos
| Attribute_Position
| Attribute_Range_Length
=>
-- If the expected type is Long_Long_Integer, there will be no
-- check flag as the compiler assumes attributes always fit in
-- this type. Since in SPARK_Mode we do not take Storage_Error
-- into account, we cannot make this assumption and need to
-- produce a check. ??? It should be enough to add this check for
-- attributes 'Length, 'Range_Length and 'Pos when the type is as
-- big as Long_Long_Integer.
declare
Typ : Entity_Id;
begin
if Attr_Id in Attribute_Pos | Attribute_Range_Length then
Typ := Etype (Prefix (N));
elsif Attr_Id = Attribute_Length then
Typ := Get_Index_Subtype (N);
else
Typ := Empty;
end if;
Apply_Universal_Integer_Attribute_Checks (N);
if Present (Typ)
and then Known_RM_Size (Typ)
and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
then
-- ??? This should rather be a range check, but this would
-- crash GNATprove which somehow recovers the proper kind
-- of check anyway.
Set_Do_Overflow_Check (N);
end if;
end;
when Attribute_Constrained =>
-- If the prefix is an access to object, the attribute applies to
-- the designated object, so rewrite with an explicit dereference.
if Is_Access_Type (Etype (Pref))
and then
(not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref)))
then
Rewrite (Pref,
Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
Analyze_And_Resolve (N, Standard_Boolean);
end if;
when Attribute_Update =>
Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N)));
when others =>
null;
end case;
end Expand_SPARK_N_Attribute_Reference;
------------------------------------
-- Expand_SPARK_N_Delta_Aggregate --
------------------------------------
procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id) is
begin
Expand_SPARK_Delta_Or_Update (Etype (N), N);
end Expand_SPARK_N_Delta_Aggregate;
-----------------------------------
-- Expand_SPARK_N_Loop_Statement --
-----------------------------------
procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is
Scheme : constant Node_Id := Iteration_Scheme (N);
begin
-- Loop iterations over arrays need to be expanded, to avoid getting
-- two names referring to the same object in memory (the array and the
-- iterator) in GNATprove, especially since both can be written (thus
-- possibly leading to interferences due to aliasing). No such problem
-- arises with quantified expressions over arrays, which are dealt with
-- specially in GNATprove.
if Present (Scheme)
and then Present (Iterator_Specification (Scheme))
and then Is_Iterator_Over_Array (Iterator_Specification (Scheme))
then
Expand_Iterator_Loop_Over_Array (N);
end if;
end Expand_SPARK_N_Loop_Statement;
---------------------------------------
-- Expand_SPARK_N_Object_Declaration --
---------------------------------------
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
Obj_Id : constant Entity_Id := Defining_Identifier (N);
Typ : constant Entity_Id := Etype (Obj_Id);
Call : Node_Id;
begin
-- If the object declaration denotes a variable without initialization
-- whose type is subject to pragma Default_Initial_Condition, create
-- and analyze a dummy call to the DIC procedure of the type in order
-- to detect potential elaboration issues.
if Comes_From_Source (Obj_Id)
and then Ekind (Obj_Id) = E_Variable
and then Has_DIC (Typ)
and then Present (DIC_Procedure (Typ))
and then not Has_Init_Expression (N)
then
Call := Build_DIC_Call (Loc, New_Occurrence_Of (Obj_Id, Loc), Typ);
-- Partially insert the call into the tree by setting its parent
-- pointer.
Set_Parent (Call, N);
Analyze (Call);
end if;
end Expand_SPARK_N_Object_Declaration;
------------------------------------------------
-- Expand_SPARK_N_Object_Renaming_Declaration --
------------------------------------------------
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
CFS : constant Boolean := Comes_From_Source (N);
Loc : constant Source_Ptr := Sloc (N);
Obj_Id : constant Entity_Id := Defining_Entity (N);
Nam : constant Node_Id := Name (N);
Typ : constant Entity_Id := Etype (Obj_Id);
begin
-- Transform a renaming of the form
-- Obj_Id : <subtype mark> renames <function call>;
-- into
-- Obj_Id : constant <subtype mark> := <function call>;
-- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
-- a temporary to capture the function result. Once potential renamings
-- are rewritten for SPARK, the temporary may be leaked out into source
-- constructs and lead to confusing error diagnostics. Using an object
-- declaration prevents this unwanted side effect.
if Nkind (Nam) = N_Function_Call then
Rewrite (N,
Make_Object_Declaration (Loc,
Defining_Identifier => Obj_Id,
Constant_Present => True,
Object_Definition => New_Occurrence_Of (Typ, Loc),
Expression => Nam));
-- Inherit the original Comes_From_Source status of the renaming
Set_Comes_From_Source (N, CFS);
-- Sever the link to the renamed function result because the entity
-- will no longer alias anything.
Set_Renamed_Object (Obj_Id, Empty);
-- Remove the entity of the renaming declaration from visibility as
-- the analysis of the object declaration will reintroduce it again.
Remove_Entity_And_Homonym (Obj_Id);
Analyze (N);
-- Otherwise unconditionally remove all side effects from the name
else
Evaluate_Name (Nam);
end if;
end Expand_SPARK_N_Object_Renaming_Declaration;
--------------------------
-- Expand_SPARK_N_Op_Ne --
--------------------------
procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is
Typ : constant Entity_Id := Etype (Left_Opnd (N));
begin
-- Case of elementary type with standard operator
if Is_Elementary_Type (Typ)
and then Sloc (Entity (N)) = Standard_Location
then
null;
else
Exp_Ch4.Expand_N_Op_Ne (N);
end if;
end Expand_SPARK_N_Op_Ne;
-------------------------------------
-- Expand_SPARK_Potential_Renaming --
-------------------------------------
procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
function In_Insignificant_Pragma (Nod : Node_Id) return Boolean;
-- Determine whether arbitrary node Nod appears within a significant
-- pragma for SPARK.
-----------------------------
-- In_Insignificant_Pragma --
-----------------------------
function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is
Par : Node_Id;
begin
-- Climb the parent chain looking for an enclosing pragma
Par := Nod;
while Present (Par) loop
if Nkind (Par) = N_Pragma then
return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par));
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
Par := Parent (Par);
end loop;
return False;
end In_Insignificant_Pragma;
-- Local variables
Loc : constant Source_Ptr := Sloc (N);
Obj_Id : constant Entity_Id := Entity (N);
Typ : constant Entity_Id := Etype (N);
Ren : Node_Id;
-- Start of processing for Expand_SPARK_Potential_Renaming
begin
-- Replace a reference to a renaming with the actual renamed object.
-- Protect against previous errors leaving no entity in N.
if Present (Obj_Id)
and then Is_Object (Obj_Id)
then
Ren := Renamed_Object (Obj_Id);
if Present (Ren) then
-- Do not process a reference when it appears within a pragma of
-- no significance to SPARK. It is assumed that the replacement
-- will violate the semantics of the pragma and cause a spurious
-- error.
if In_Insignificant_Pragma (N) then
return;
-- Instantiations and inlining of subprograms employ "prologues"
-- which map actual to formal parameters by means of renamings.
-- Replace a reference to a formal by the corresponding actual
-- parameter.
elsif Nkind (Ren) in N_Entity then
Rewrite (N, New_Occurrence_Of (Ren, Loc));
-- Otherwise the renamed object denotes a name
else
Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc));
Reset_Analyzed_Flags (N);
end if;
Analyze_And_Resolve (N, Typ);
end if;
end if;
end Expand_SPARK_Potential_Renaming;
-----------------------
-- SPARK_Freeze_Type --
-----------------------
procedure SPARK_Freeze_Type (N : Entity_Id) is
Typ : constant Entity_Id := Entity (N);
Renamed_Eq : Entity_Id;
-- Defining unit name for the predefined equality function in the case
-- where the type has a primitive operation that is a renaming of
-- predefined equality (but only if there is also an overriding
-- user-defined equality function). Used to pass this entity from
-- Make_Predefined_Primitive_Specs to Predefined_Primitive_Bodies.
Decl : Node_Id;
Eq_Spec : Node_Id := Empty;
Predef_List : List_Id;
Wrapper_Decl_List : List_Id;
Wrapper_Body_List : List_Id := No_List;
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
begin
-- The type being frozen may be subject to pragma Ghost. Set the mode
-- now to ensure that any nodes generated during freezing are properly
-- marked as Ghost.
Set_Ghost_Mode (Typ);
-- Generate the [spec and] body of the invariant procedure tasked with
-- the runtime verification of all invariants that pertain to the type.
-- This includes invariants on the partial and full view, inherited
-- class-wide invariants from parent types or interfaces, and invariants
-- on array elements or record components. But skip internal types.
if Is_Itype (Typ) then
null;
elsif Is_Interface (Typ) then
-- Interfaces are treated as the partial view of a private type in
-- order to achieve uniformity with the general case. As a result, an
-- interface receives only a "partial" invariant procedure which is
-- never called.
if Has_Own_Invariants (Typ) then
Build_Invariant_Procedure_Body
(Typ => Typ,
Partial_Invariant => Is_Interface (Typ));
end if;
-- Non-interface types
-- Do not generate invariant procedure within other assertion
-- subprograms, which may involve local declarations of local
-- subtypes to which these checks do not apply.
else
if Has_Invariants (Typ) then
if not Predicate_Check_In_Scope (Typ)
or else (Ekind (Current_Scope) = E_Function
and then Is_Predicate_Function (Current_Scope))
then
null;
else
Build_Invariant_Procedure_Body (Typ);
end if;
end if;
-- Generate the [spec and] body of the procedure tasked with the
-- run-time verification of pragma Default_Initial_Condition's
-- expression.
if Has_DIC (Typ) then
Build_DIC_Procedure_Body (Typ);
end if;
end if;
if Ekind (Typ) = E_Record_Type
and then Is_Tagged_Type (Typ)
and then not Is_Interface (Typ)
and then not Is_Limited_Type (Typ)
then
if Is_CPP_Class (Root_Type (Typ))
and then Convention (Typ) = Convention_CPP
then
null;
-- Do not add the spec of the predefined primitives if we are
-- compiling under restriction No_Dispatching_Calls.
elsif not Restriction_Active (No_Dispatching_Calls) then
Set_Is_Frozen (Typ, False);
Predef_List := New_List;
Exp_Ch3.Make_Predefined_Primitive_Eq_Spec
(Typ, Predef_List, Renamed_Eq);
Eq_Spec := First (Predef_List);
Insert_List_Before_And_Analyze (N, Predef_List);
Set_Is_Frozen (Typ);
-- Remove link from the parent list to the spec and body of
-- the dispatching equality, but keep the link in the opposite
-- direction, to allow up-traversal of the AST.
if Present (Eq_Spec) then
Decl := Parent (Eq_Spec);
Remove (Eq_Spec);
Set_Parent (Eq_Spec, Decl);
end if;
end if;
end if;
if Ekind (Typ) = E_Record_Type
and then Is_Tagged_Type (Typ)
and then not Is_CPP_Class (Typ)
then
-- Ada 2005 (AI-391): For a nonabstract null extension, create
-- wrapper functions for each nonoverridden inherited function
-- with a controlling result of the type. The wrapper for such
-- a function returns an extension aggregate that invokes the
-- parent function.
if Ada_Version >= Ada_2005
and then not Is_Abstract_Type (Typ)
and then Is_Null_Extension (Typ)
then
Exp_Ch3.Make_Controlling_Function_Wrappers
(Typ, Wrapper_Decl_List, Wrapper_Body_List);
Insert_List_Before_And_Analyze (N, Wrapper_Decl_List);
end if;
-- Ada 2005 (AI-391): If any wrappers were created for nonoverridden
-- inherited functions, then add their bodies to the AST, so they
-- will be processed like ordinary subprogram bodies (even though the
-- compiler adds them into the freezing action).
if not Is_Interface (Typ) then
Insert_List_Before_And_Analyze (N, Wrapper_Body_List);
end if;
end if;
Restore_Ghost_Region (Saved_GM, Saved_IGR);
end SPARK_Freeze_Type;
end Exp_SPARK;