diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 22 | ||||
| -rw-r--r-- | gcc/ada/a-cofove.ads | 16 | ||||
| -rw-r--r-- | gcc/ada/exp_ch3.adb | 20 | ||||
| -rw-r--r-- | gcc/ada/sem_elab.adb | 172 | ||||
| -rw-r--r-- | gcc/ada/sem_elab.ads | 98 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 10 |
6 files changed, 233 insertions, 105 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 45870c3..e43d191 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -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 diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads index 5bbd18c..6ddd24b 100644 --- a/gcc/ada/a-cofove.ads +++ b/gcc/ada/a-cofove.ads @@ -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 @@ -212,17 +214,19 @@ is function First_To_Previous (Container : Vector; - Current : Index_Type) return Vector + 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 + 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. diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 8bbbdc3..f2f42d4 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -23,6 +23,7 @@ -- -- ------------------------------------------------------------------------------ +with Aspects; use Aspects; with Atree; use Atree; with Checks; use Checks; with Einfo; use Einfo; @@ -5462,8 +5463,23 @@ package body Exp_Ch3 is and then not Has_Init_Expression (N) and then not No_Initialization (N) then - Insert_After (N, - Make_Invariant_Call (New_Occurrence_Of (Def_Id, Loc))); + -- 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); diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index a57a477..c84d04b 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -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,45 +613,60 @@ 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; - loop - if (Suppress_Elaboration_Warnings (Ent) - or else Elaboration_Checks_Suppressed (Ent)) - and then (Inst_Case or else No (Alias (Ent))) - then - return; - end if; - -- Nothing to do for imported entities + -- For a variable reference, just set Body_Acts_As_Spec to False - if Is_Imported (Ent) then - return; - end if; + 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; - exit when Inst_Case or else No (Alias (Ent)); - Ent := Alias (Ent); - end loop; + -- Additional checks for all other cases - Decl := Unit_Declaration_Node (Ent); + else + -- Go to parent for derived subprogram, or to original subprogram in + -- the case of a renaming (Alias covers both these cases). - if Nkind (Decl) = N_Subprogram_Body then - Body_Acts_As_Spec := True; + loop + if (Suppress_Elaboration_Warnings (Ent) + or else Elaboration_Checks_Suppressed (Ent)) + and then (Inst_Case or else No (Alias (Ent))) + then + return; + end if; - elsif Nkind_In (Decl, N_Subprogram_Declaration, N_Subprogram_Body_Stub) - or else Inst_Case - then - Body_Acts_As_Spec := False; + -- Nothing to do for imported entities - -- 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). + if Is_Imported (Ent) then + return; + end if; - else - return; + exit when Inst_Case or else No (Alias (Ent)); + Ent := Alias (Ent); + end loop; + + Decl := Unit_Declaration_Node (Ent); + + if Nkind (Decl) = N_Subprogram_Body then + Body_Acts_As_Spec := True; + + 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, 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; @@ -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 diff --git a/gcc/ada/sem_elab.ads b/gcc/ada/sem_elab.ads index 797e04a..49ea85e 100644 --- a/gcc/ada/sem_elab.ads +++ b/gcc/ada/sem_elab.ads @@ -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. - - -- 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 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 + -- 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 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. + + -- 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. - - -- 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. + -- 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. + + -- 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 diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index e0b1b0e..8b0f658 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -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; ------------------- |