[multiple changes]
authorArnaud Charlet <charlet@gcc.gnu.org>
Thu, 20 Nov 2014 15:47:33 +0000 (16:47 +0100)
committerArnaud Charlet <charlet@gcc.gnu.org>
Thu, 20 Nov 2014 15:47:33 +0000 (16:47 +0100)
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

gcc/ada/ChangeLog
gcc/ada/a-cofove.ads
gcc/ada/exp_ch3.adb
gcc/ada/sem_elab.adb
gcc/ada/sem_elab.ads
gcc/ada/sem_res.adb

index 45870c365d8e1f6979b1fea2e92885775225b811..e43d191f67a645c13566fc591efd7982e5769f87 100644 (file)
@@ -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
index 5bbd18c2cdd894d866917cc51d7e626caa4f21b0..6ddd24b9fcad24343832984aa35e9da16539e684 100644 (file)
@@ -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.
index 8bbbdc32374dddd359d8f99873d4ee5f4653ace8..f2f42d4d9fdbbab207bc5939a09d074000da9637 100644 (file)
@@ -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);
index a57a477539de314b3e4baa412da158b8d3959737..c84d04b30c9c3ac450bd663e8b39b4924c3400ef 100644 (file)
@@ -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
index 797e04a98adf2853faf9214f91e6329f0b989e9a..49ea85ec904c444394c5aba31fa707066de17840 100644 (file)
@@ -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
index e0b1b0e20d497b818a8ed8a4caf77fee0aec4318..8b0f6585f882bdc80207e0758a25068a7bb8a396 100644 (file)
@@ -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;
 
    -------------------