[multiple changes]
2014-11-20 Ed Schonberg <schonberg@adacore.com> * exp_ch3.adb (Expand_N_Object_Declaration): Handle properly a type invariant check on an object with default initialization and an address clause. 2014-11-20 Robert Dewar <dewar@adacore.com> * sem_elab.adb (Check_A_Call): Handle variable ref case in SPARK (Check_Elab_Call): ditto (Find_Elab_Reference): ditto (Get_Referenced_Ent): ditto. * sem_elab.ads: Comment fixes to account for the fact that we now deal with variable references in SPARK mode. * sem_res.adb (Resolve_Entity_Name): In SPARK_Mode Call Check_Elab_Call for variable. 2014-11-20 Yannick Moy <moy@adacore.com> * a-cofove.ads (Copy): Fix precondition, which should allow Capacity = 0. (First_To_Previous, Current_To_Last): Add necessary preconditions. From-SVN: r217878
This commit is contained in:
parent
8c691dc68e
commit
de4899bb19
|
@ -1,3 +1,25 @@
|
|||
2014-11-20 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* exp_ch3.adb (Expand_N_Object_Declaration): Handle properly
|
||||
a type invariant check on an object with default initialization
|
||||
and an address clause.
|
||||
|
||||
2014-11-20 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* sem_elab.adb (Check_A_Call): Handle variable ref case in
|
||||
SPARK (Check_Elab_Call): ditto (Find_Elab_Reference): ditto
|
||||
(Get_Referenced_Ent): ditto.
|
||||
* sem_elab.ads: Comment fixes to account for the fact that we
|
||||
now deal with variable references in SPARK mode.
|
||||
* sem_res.adb (Resolve_Entity_Name): In SPARK_Mode Call
|
||||
Check_Elab_Call for variable.
|
||||
|
||||
2014-11-20 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* a-cofove.ads (Copy): Fix precondition, which should allow
|
||||
Capacity = 0.
|
||||
(First_To_Previous, Current_To_Last): Add necessary preconditions.
|
||||
|
||||
2014-11-20 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* exp_ch3.adb (Build_Initialization_Call): Reimplement the
|
||||
|
|
|
@ -114,7 +114,7 @@ is
|
|||
Capacity : Capacity_Range := 0) return Vector
|
||||
with
|
||||
Global => null,
|
||||
Pre => (if Bounded then Length (Source) <= Capacity);
|
||||
Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity));
|
||||
|
||||
function Element
|
||||
(Container : Vector;
|
||||
|
@ -195,7 +195,9 @@ is
|
|||
Global => null;
|
||||
|
||||
function Has_Element
|
||||
(Container : Vector; Position : Extended_Index) return Boolean with
|
||||
(Container : Vector;
|
||||
Position : Extended_Index) return Boolean
|
||||
with
|
||||
Global => null;
|
||||
|
||||
generic
|
||||
|
@ -215,14 +217,16 @@ is
|
|||
Current : Index_Type) return Vector
|
||||
with
|
||||
Ghost,
|
||||
Global => null;
|
||||
Global => null,
|
||||
Pre => Current in First_Index (Container) .. Last_Index (Container);
|
||||
|
||||
function Current_To_Last
|
||||
(Container : Vector;
|
||||
Current : Index_Type) return Vector
|
||||
with
|
||||
Ghost,
|
||||
Global => null;
|
||||
Global => null,
|
||||
Pre => Current in First_Index (Container) .. Last_Index (Container);
|
||||
-- First_To_Previous returns a container containing all elements preceding
|
||||
-- Current (excluded) in Container. Current_To_Last returns a container
|
||||
-- containing all elements following Current (included) in Container.
|
||||
|
|
|
@ -23,6 +23,7 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Checks; use Checks;
|
||||
with Einfo; use Einfo;
|
||||
|
@ -5462,9 +5463,24 @@ package body Exp_Ch3 is
|
|||
and then not Has_Init_Expression (N)
|
||||
and then not No_Initialization (N)
|
||||
then
|
||||
-- If entity has an address clause or aspect, make invariant
|
||||
-- call into a freeze action for the explicit freeze node for
|
||||
-- object. Otherwise insert invariant check after declaration.
|
||||
|
||||
if Present (Following_Address_Clause (N))
|
||||
or else Has_Aspect (Def_Id, Aspect_Address)
|
||||
then
|
||||
Ensure_Freeze_Node (Def_Id);
|
||||
Set_Has_Delayed_Freeze (Def_Id);
|
||||
Set_Is_Frozen (Def_Id, False);
|
||||
Append_Freeze_Action (Def_Id,
|
||||
Make_Invariant_Call (New_Occurrence_Of (Def_Id, Loc)));
|
||||
|
||||
else
|
||||
Insert_After (N,
|
||||
Make_Invariant_Call (New_Occurrence_Of (Def_Id, Loc)));
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Default_Initialize_Object (Init_After);
|
||||
|
||||
|
|
|
@ -184,7 +184,11 @@ package body Sem_Elab is
|
|||
-- E is the entity of the called subprogram, or instantiated generic unit,
|
||||
-- or subprogram referenced by 'Access.
|
||||
--
|
||||
-- The flag Outer_Scope is the outer level scope for the original call.
|
||||
-- In SPARK mode, N can also be a variable reference, since in SPARK this
|
||||
-- also triggers a requirement for Elaborate_All, and in this case E is the
|
||||
-- entity being referenced.
|
||||
--
|
||||
-- Outer_Scope is the outer level scope for the original reference.
|
||||
-- Inter_Unit_Only is set if the call is only to be checked in the
|
||||
-- case where it is to another unit (and skipped if within a unit).
|
||||
-- Generate_Warnings is set to False to suppress warning messages about
|
||||
|
@ -194,6 +198,11 @@ package body Sem_Elab is
|
|||
-- procedure (since the referenced subprogram may be called later
|
||||
-- indirectly). Flag In_Init_Proc should be set whenever the current
|
||||
-- context is a type init proc.
|
||||
--
|
||||
-- Note: this might better be called Check_A_Reference to recognize the
|
||||
-- variable case for SPARK, but we prefer to retain the historical name
|
||||
-- since in practice this is mostly about checking calls for the possible
|
||||
-- occurrence of an access-before-elaboration exception.
|
||||
|
||||
procedure Check_Bad_Instantiation (N : Node_Id);
|
||||
-- N is a node for an instantiation (if called with any other node kind,
|
||||
|
@ -287,6 +296,9 @@ package body Sem_Elab is
|
|||
-- this is a call to a protected subprogram, the entity is a selected
|
||||
-- component. The callable entity may be absent, in which case Empty is
|
||||
-- returned. This happens with non-analyzed calls in nested generics.
|
||||
--
|
||||
-- If SPARK_Mode is On, then N can also be a reference to an E_Variable
|
||||
-- entity, in which case, the value returned is simply this entity.
|
||||
|
||||
procedure Set_Elaboration_Constraint
|
||||
(Call : Node_Id;
|
||||
|
@ -601,10 +613,22 @@ package body Sem_Elab is
|
|||
return;
|
||||
end if;
|
||||
|
||||
-- Go to parent for derived subprogram, or to original subprogram in the
|
||||
-- case of a renaming (Alias covers both these cases).
|
||||
|
||||
Ent := E;
|
||||
|
||||
-- For a variable reference, just set Body_Acts_As_Spec to False
|
||||
|
||||
if Nkind (N) in N_Has_Entity
|
||||
and then Present (Entity (N))
|
||||
and then Ekind (Entity (N)) = E_Variable
|
||||
then
|
||||
Body_Acts_As_Spec := False;
|
||||
|
||||
-- Additional checks for all other cases
|
||||
|
||||
else
|
||||
-- Go to parent for derived subprogram, or to original subprogram in
|
||||
-- the case of a renaming (Alias covers both these cases).
|
||||
|
||||
loop
|
||||
if (Suppress_Elaboration_Warnings (Ent)
|
||||
or else Elaboration_Checks_Suppressed (Ent))
|
||||
|
@ -628,19 +652,22 @@ package body Sem_Elab is
|
|||
if Nkind (Decl) = N_Subprogram_Body then
|
||||
Body_Acts_As_Spec := True;
|
||||
|
||||
elsif Nkind_In (Decl, N_Subprogram_Declaration, N_Subprogram_Body_Stub)
|
||||
elsif Nkind_In (Decl, N_Subprogram_Declaration,
|
||||
N_Subprogram_Body_Stub)
|
||||
or else Inst_Case
|
||||
then
|
||||
Body_Acts_As_Spec := False;
|
||||
|
||||
-- If we have none of an instantiation, subprogram body or subprogram
|
||||
-- declaration, then it is not a case that we want to check. (One case
|
||||
-- is a call to a generic formal subprogram, where we do not want the
|
||||
-- check in the template).
|
||||
-- declaration, or in the SPARK case, a variable reference, then
|
||||
-- it is not a case that we want to check. (One case is a call to a
|
||||
-- generic formal subprogram, where we do not want the check in the
|
||||
-- template).
|
||||
|
||||
else
|
||||
return;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
E_Scope := Ent;
|
||||
loop
|
||||
|
@ -941,6 +968,16 @@ package body Sem_Elab is
|
|||
Elab_Warning
|
||||
("", "info: access to & during elaboration?$?", Ent);
|
||||
|
||||
-- Variable reference in SPARK mode
|
||||
|
||||
elsif SPARK_Mode = On
|
||||
and then Nkind (N) in N_Has_Entity
|
||||
and then Present (Entity (N))
|
||||
and then Ekind (Entity (N)) = E_Variable
|
||||
then
|
||||
Error_Msg_NE
|
||||
("reference to & during elaboration in SPARK", N, Ent);
|
||||
|
||||
-- Subprogram call case
|
||||
|
||||
else
|
||||
|
@ -1207,9 +1244,9 @@ package body Sem_Elab is
|
|||
P : Node_Id;
|
||||
|
||||
begin
|
||||
-- If the call does not come from the main unit, there is nothing to
|
||||
-- check. Elaboration call from units in the context of the main unit
|
||||
-- will lead to semantic dependencies when those units are compiled.
|
||||
-- If the reference is not in the main unit, there is nothing to check.
|
||||
-- Elaboration call from units in the context of the main unit will lead
|
||||
-- to semantic dependencies when those units are compiled.
|
||||
|
||||
if not In_Extended_Main_Code_Unit (N) then
|
||||
return;
|
||||
|
@ -1222,15 +1259,22 @@ package body Sem_Elab is
|
|||
then
|
||||
Check_Restriction (No_Entry_Calls_In_Elaboration_Code, N);
|
||||
|
||||
-- Nothing to do if this is not a call or attribute reference (happens
|
||||
-- Nothing to do if this is not an expected type of reference (happens
|
||||
-- in some error conditions, and in some cases where rewriting occurs).
|
||||
|
||||
elsif Nkind (N) not in N_Subprogram_Call
|
||||
and then Nkind (N) /= N_Attribute_Reference
|
||||
and then (SPARK_Mode /= On
|
||||
or else Nkind (N) not in N_Has_Entity
|
||||
or else No (Entity (N))
|
||||
or else Ekind (Entity (N)) /= E_Variable)
|
||||
then
|
||||
return;
|
||||
|
||||
-- Nothing to do if this is a call already rewritten for elab checking
|
||||
-- Nothing to do if this is a call already rewritten for elab checking.
|
||||
-- Such calls appear as the targets of If_Expressions.
|
||||
|
||||
-- This check MUST be wrong, it catches far too much
|
||||
|
||||
elsif Nkind (Parent (N)) = N_If_Expression then
|
||||
return;
|
||||
|
@ -1260,10 +1304,10 @@ package body Sem_Elab is
|
|||
return;
|
||||
end if;
|
||||
|
||||
-- Here we have a call at elaboration time which must be checked
|
||||
-- Here we have a reference at elaboration time which must be checked
|
||||
|
||||
if Debug_Flag_LL then
|
||||
Write_Str (" Check_Elab_Call: ");
|
||||
Write_Str (" Check_Elab_Ref: ");
|
||||
|
||||
if Nkind (N) = N_Attribute_Reference then
|
||||
if not Is_Entity_Name (Prefix (N)) then
|
||||
|
@ -1271,6 +1315,7 @@ package body Sem_Elab is
|
|||
else
|
||||
Write_Name (Chars (Entity (Prefix (N))));
|
||||
end if;
|
||||
|
||||
Write_Str ("'Access");
|
||||
|
||||
elsif No (Name (N)) or else not Is_Entity_Name (Name (N)) then
|
||||
|
@ -1280,20 +1325,21 @@ package body Sem_Elab is
|
|||
Write_Name (Chars (Entity (Name (N))));
|
||||
end if;
|
||||
|
||||
Write_Str (" call at ");
|
||||
Write_Str (" reference at ");
|
||||
Write_Location (Sloc (N));
|
||||
Write_Eol;
|
||||
end if;
|
||||
|
||||
-- Climb up the tree to make sure we are not inside default expression
|
||||
-- of a parameter specification or a record component, since in both
|
||||
-- these cases, we will be doing the actual call later, not now, and it
|
||||
-- is at the time of the actual call (statically speaking) that we must
|
||||
-- do our static check, not at the time of its initial analysis).
|
||||
-- these cases, we will be doing the actual reference later, not now,
|
||||
-- and it is at the time of the actual reference (statically speaking)
|
||||
-- that we must do our static check, not at the time of its initial
|
||||
-- analysis).
|
||||
|
||||
-- However, we have to check calls within component definitions (e.g.
|
||||
-- a function call that determines an array component bound), so we
|
||||
-- terminate the loop in that case.
|
||||
-- However, we have to check references within component definitions
|
||||
-- (e.g. a function call that determines an array component bound),
|
||||
-- so we terminate the loop in that case.
|
||||
|
||||
P := Parent (N);
|
||||
while Present (P) loop
|
||||
|
@ -1302,7 +1348,7 @@ package body Sem_Elab is
|
|||
then
|
||||
return;
|
||||
|
||||
-- The call occurs within the constraint of a component,
|
||||
-- The reference occurs within the constraint of a component,
|
||||
-- so it must be checked.
|
||||
|
||||
elsif Nkind (P) = N_Component_Definition then
|
||||
|
@ -1333,7 +1379,7 @@ package body Sem_Elab is
|
|||
|
||||
if From_Elab_Code then
|
||||
|
||||
-- Complain if call that comes from source in preelaborated unit
|
||||
-- Complain if ref that comes from source in preelaborated unit
|
||||
-- and we are not inside a subprogram (i.e. we are in elab code).
|
||||
|
||||
if Comes_From_Source (N)
|
||||
|
@ -1415,8 +1461,8 @@ package body Sem_Elab is
|
|||
|
||||
-- We are not in elaboration code, but we are doing
|
||||
-- dynamic elaboration checks, in this case, we still
|
||||
-- need to do the call, since the subprogram we are in
|
||||
-- could be called from another unit, also in dynamic
|
||||
-- need to do the reference, since the subprogram we are
|
||||
-- in could be called from another unit, also in dynamic
|
||||
-- elaboration check mode, at elaboration time.
|
||||
|
||||
elsif Dynamic_Elaboration_Checks then
|
||||
|
@ -1482,23 +1528,23 @@ package body Sem_Elab is
|
|||
end if;
|
||||
end loop;
|
||||
|
||||
-- See if we need to analyze this call. We analyze it if either of
|
||||
-- See if we need to analyze this reference. We analyze it if either of
|
||||
-- the following conditions is met:
|
||||
|
||||
-- It is an inner level call (since in this case it was triggered
|
||||
-- by an outer level call from elaboration code), but only if the
|
||||
-- call is within the scope of the original outer level call.
|
||||
|
||||
-- It is an outer level call from elaboration code, or the called
|
||||
-- entity is in the same elaboration scope.
|
||||
-- It is an outer level reference from elaboration code, or a call to
|
||||
-- an entity is in the same elaboration scope.
|
||||
|
||||
-- And in these cases, we will check both inter-unit calls and
|
||||
-- intra-unit (within a single unit) calls.
|
||||
|
||||
C_Scope := Current_Scope;
|
||||
|
||||
-- If not outer level call, then we follow it if it is within the
|
||||
-- original scope of the outer call.
|
||||
-- If not outer level reference, then we follow it if it is within the
|
||||
-- original scope of the outer reference.
|
||||
|
||||
if Present (Outer_Scope)
|
||||
and then Within (Scope (Ent), Outer_Scope)
|
||||
|
@ -2088,6 +2134,17 @@ package body Sem_Elab is
|
|||
Check_Elab_Call (N, Outer_Scope);
|
||||
return OK;
|
||||
|
||||
-- In SPARK mode, if we have an entity reference to a variable, then
|
||||
-- check it. For now we consider any reference.
|
||||
|
||||
elsif SPARK_Mode = On
|
||||
and then Nkind (N) in N_Has_Entity
|
||||
and then Present (Entity (N))
|
||||
and then Ekind (Entity (N)) = E_Variable
|
||||
then
|
||||
Check_Elab_Call (N, Outer_Scope);
|
||||
return OK;
|
||||
|
||||
-- If we have a generic instantiation, check it
|
||||
|
||||
elsif Nkind (N) in N_Generic_Instantiation then
|
||||
|
@ -2760,6 +2817,13 @@ package body Sem_Elab is
|
|||
Nam : Node_Id;
|
||||
|
||||
begin
|
||||
if Nkind (N) in N_Has_Entity
|
||||
and then Present (Entity (N))
|
||||
and then Ekind (Entity (N)) = E_Variable
|
||||
then
|
||||
return Entity (N);
|
||||
end if;
|
||||
|
||||
if Nkind (N) = N_Attribute_Reference then
|
||||
Nam := Prefix (N);
|
||||
else
|
||||
|
|
|
@ -35,41 +35,48 @@ package Sem_Elab is
|
|||
-- Description of Approach --
|
||||
-----------------------------
|
||||
|
||||
-- Every non-static call that is encountered by Sem_Res results in
|
||||
-- a call to Check_Elab_Call, with N being the call node, and Outer
|
||||
-- set to its default value of True.
|
||||
-- Every non-static call that is encountered by Sem_Res results in a call
|
||||
-- to Check_Elab_Call, with N being the call node, and Outer set to its
|
||||
-- default value of True. In addition X'Access is treated like a call
|
||||
-- for the access-to-procedure case, and in SPARK mode only we also
|
||||
-- check variable references.
|
||||
|
||||
-- The goal of Check_Elab_Call is to determine whether or not the
|
||||
-- call in question can generate an access before elaboration
|
||||
-- error (raising Program_Error) either by directly calling a
|
||||
-- subprogram whose body has not yet been elaborated, or indirectly,
|
||||
-- by calling a subprogram whose body has been elaborated, but which
|
||||
-- contains a call to such a subprogram.
|
||||
-- The goal of Check_Elab_Call is to determine whether or not the reference
|
||||
-- in question can generate an access before elaboration error (raising
|
||||
-- Program_Error) either by directly calling a subprogram whose body
|
||||
-- has not yet been elaborated, or indirectly, by calling a subprogram
|
||||
-- whose body has been elaborated, but which contains a call to such a
|
||||
-- subprogram.
|
||||
|
||||
-- The only calls that we need to look at at the outer level are
|
||||
-- calls that occur in elaboration code. There are two cases. The
|
||||
-- call can be at the outer level of elaboration code, or it can
|
||||
-- In addition, in SPARK mode, we are checking for a variable reference in
|
||||
-- another package, which requires an explicit Elaborate_All pragma.
|
||||
|
||||
-- The only references that we need to look at at the outer level are
|
||||
-- references that occur in elaboration code. There are two cases. The
|
||||
-- reference can be at the outer level of elaboration code, or it can
|
||||
-- be within another unit, e.g. the elaboration code of a subprogram.
|
||||
|
||||
-- In the case of an elaboration call at the outer level, we must
|
||||
-- trace all calls to outer level routines either within the current
|
||||
-- unit or to other units that are with'ed. For calls within the
|
||||
-- current unit, we can determine if the body has been elaborated
|
||||
-- or not, and if it has not, then a warning is generated.
|
||||
-- In the case of an elaboration call at the outer level, we must trace
|
||||
-- all calls to outer level routines either within the current unit or to
|
||||
-- other units that are with'ed. For calls within the current unit, we can
|
||||
-- determine if the body has been elaborated or not, and if it has not,
|
||||
-- then a warning is generated.
|
||||
|
||||
-- Note that there are two subcases. If the original call directly
|
||||
-- calls a subprogram whose body has not been elaborated, then we
|
||||
-- know that an ABE will take place, and we replace the call by
|
||||
-- a raise of Program_Error. If the call is indirect, then we don't
|
||||
-- know that the PE will be raised, since the call might be guarded
|
||||
-- by a conditional. In this case we set Do_Elab_Check on the call
|
||||
-- so that a dynamic check is generated, and output a warning.
|
||||
-- Note that there are two subcases. If the original call directly calls a
|
||||
-- subprogram whose body has not been elaborated, then we know that an ABE
|
||||
-- will take place, and we replace the call by a raise of Program_Error.
|
||||
-- If the call is indirect, then we don't know that the PE will be raised,
|
||||
-- since the call might be guarded by a conditional. In this case we set
|
||||
-- Do_Elab_Check on the call so that a dynamic check is generated, and
|
||||
-- output a warning.
|
||||
|
||||
-- For calls to a subprogram in a with'ed unit, we require that
|
||||
-- a pragma Elaborate_All or pragma Elaborate be present, or that
|
||||
-- the referenced unit have a pragma Preelaborate, pragma Pure, or
|
||||
-- pragma Elaborate_Body. If none of these conditions is met, then
|
||||
-- a warning is generated that a pragma Elaborate_All may be needed.
|
||||
-- For calls to a subprogram in a with'ed unit or a 'Access or variable
|
||||
-- refernece (SPARK mode case), we require that a pragma Elaborate_All
|
||||
-- or pragma Elaborate be present, or that the referenced unit have a
|
||||
-- pragma Preelaborate, pragma Pure, or pragma Elaborate_Body. If none
|
||||
-- of these conditions is met, then a warning is generated that a pragma
|
||||
-- Elaborate_All may be needed (error in the SPARK case), or an implicit
|
||||
-- pragma is generated.
|
||||
|
||||
-- For the case of an elaboration call at some inner level, we are
|
||||
-- interested in tracing only calls to subprograms at the same level,
|
||||
|
@ -86,9 +93,8 @@ package Sem_Elab is
|
|||
-- Elaborate on a with'ed unit guarantees that subprograms within the
|
||||
-- unit can be called without causing an ABE. This is not in fact the
|
||||
-- case since pragma Elaborate does not guarantee the transitive
|
||||
-- coverage guaranteed by Elaborate_All. However, we leave this issue
|
||||
-- up to the binder, which has generates warnings if there are possible
|
||||
-- problems in the use of pragma Elaborate.
|
||||
-- coverage guaranteed by Elaborate_All. However, we decide to trust
|
||||
-- the user in this case.
|
||||
|
||||
--------------------------------------
|
||||
-- Instantiation Elaboration Errors --
|
||||
|
@ -124,11 +130,21 @@ package Sem_Elab is
|
|||
In_Init_Proc : Boolean := False);
|
||||
-- Check a call for possible elaboration problems. The node N is either an
|
||||
-- N_Function_Call or N_Procedure_Call_Statement node or an access
|
||||
-- attribute reference whose prefix is a subprogram. The Outer_Scope
|
||||
-- argument indicates whether this is an outer level call from Sem_Res
|
||||
-- (Outer_Scope set to Empty), or an internal recursive call (Outer_Scope
|
||||
-- set to entity of outermost call, see body). Flag In_Init_Proc should be
|
||||
-- set whenever the current context is a type init proc.
|
||||
-- attribute reference whose prefix is a subprogram.
|
||||
--
|
||||
-- If SPARK_Mode is On, then N can also be a variablr reference, since
|
||||
-- SPARK requires the use of Elaborate_All for references to variables
|
||||
-- in other packages.
|
||||
|
||||
-- The Outer_Scope argument indicates whether this is an outer level
|
||||
-- call from Sem_Res (Outer_Scope set to Empty), or an internal recursive
|
||||
-- call (Outer_Scope set to entity of outermost call, see body). The flag
|
||||
-- In_Init_Proc should be set whenever the current context is a type
|
||||
-- init proc.
|
||||
|
||||
-- Note: this might better be called Check_Elab_Reference (to recognize
|
||||
-- the SPARK case), but we prefer to keep the original name, since this
|
||||
-- is primarily used for checking for calls that could generate an ABE).
|
||||
|
||||
procedure Check_Elab_Calls;
|
||||
-- Not all the processing for Check_Elab_Call can be done at the time
|
||||
|
|
|
@ -7172,8 +7172,8 @@ package body Sem_Res is
|
|||
if SPARK_Mode = On
|
||||
and then Is_Object (E)
|
||||
and then Is_Effectively_Volatile (E)
|
||||
and then
|
||||
(Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
|
||||
and then (Async_Writers_Enabled (E)
|
||||
or else Effective_Reads_Enabled (E))
|
||||
and then Comes_From_Source (N)
|
||||
then
|
||||
-- The effectively volatile objects appears in a "non-interfering
|
||||
|
@ -7197,6 +7197,12 @@ package body Sem_Res is
|
|||
if Is_Ghost_Entity (E) and then Comes_From_Source (N) then
|
||||
Check_Ghost_Context (E, N);
|
||||
end if;
|
||||
|
||||
-- In SPARK mode, need to check possible elaboration issues
|
||||
|
||||
if SPARK_Mode = On and then Ekind (E) = E_Variable then
|
||||
Check_Elab_Call (N);
|
||||
end if;
|
||||
end Resolve_Entity_Name;
|
||||
|
||||
-------------------
|
||||
|
|
Loading…
Reference in New Issue