[multiple changes]

2011-08-29  Robert Dewar  <dewar@adacore.com>

	* sem_ch10.adb, a-coorse.adb, exp_dist.adb, exp_ch3.adb: Minor
	reformatting.
	* gcc-interface/Make-lang.in: Update dependencies.

2011-08-29  Yannick Moy  <moy@adacore.com>

	* alfa.ads (Name_Of_Heap_Variable): New constant name.
	* lib-xref-alfa.adb, lib-xref.adb, lib-xref.ads (Drefs): New global
	table to hold dereferences.
	(Add_ALFA_Xrefs): Take into account dereferences as special
	reads/writes to the variable "HEAP".
	(Enclosing_Subprogram_Or_Package): Move subprogram here.
	(Generate_Dereference): New procedure to store a read/write dereferencew
	in the table Drefs.
	* put_alfa.adb (Put_ALFA): Use different default than (0,0) used for
	the special "HEAP" var.
	* sem_ch4.adb (Analyze_Explicit_Dereference): Store read dereference
	in ALFA mode.
	* sem_util.adb (Note_Possible_Modification): Store write dereference
	in ALFA mode.

From-SVN: r178252

gcc/ada/ChangeLog

+2011-08-29  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch10.adb, a-coorse.adb, exp_dist.adb, exp_ch3.adb: Minor
+	reformatting.
+	* gcc-interface/Make-lang.in: Update dependencies.
+
+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* alfa.ads (Name_Of_Heap_Variable): New constant name.
+	* lib-xref-alfa.adb, lib-xref.adb, lib-xref.ads (Drefs): New global
+	table to hold dereferences.
+	(Add_ALFA_Xrefs): Take into account dereferences as special
+	reads/writes to the variable "HEAP".
+	(Enclosing_Subprogram_Or_Package): Move subprogram here.
+	(Generate_Dereference): New procedure to store a read/write dereferencew
+	in the table Drefs.
+	* put_alfa.adb (Put_ALFA): Use different default than (0,0) used for
+	the special "HEAP" var.
+	* sem_ch4.adb (Analyze_Explicit_Dereference): Store read dereference
+	in ALFA mode.
+	* sem_util.adb (Note_Possible_Modification): Store write dereference
+	in ALFA mode.
+
 2011-08-29  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* exp_ch3.adb (Freeze_Type): Generate an accessibility check which

gcc/ada/a-coorse.adb

@@ -535,9 +535,10 @@ package body Ada.Containers.Ordered_Sets is
       if Object.Container = null then
          return No_Element;
       else
-         return Cursor'(
-          Object.Container.all'Unrestricted_Access,
-            Object.Container.Tree.First);
+         return
+           Cursor'(
+             Object.Container.all'Unrestricted_Access,
+             Object.Container.Tree.First);
       end if;
    end First;
 
@@ -1171,19 +1172,20 @@ package body Ada.Containers.Ordered_Sets is
    begin
       if Container.Tree.Last = null then
          return No_Element;
+      else
+         return Cursor'(Container'Unrestricted_Access, Container.Tree.Last);
       end if;
-
-      return Cursor'(Container'Unrestricted_Access, Container.Tree.Last);
    end Last;
 
    function Last (Object : Iterator) return Cursor is
    begin
       if Object.Container = null then
          return No_Element;
+      else
+         return Cursor'(
+           Object.Container.all'Unrestricted_Access,
+                        Object.Container.Tree.Last);
       end if;
-
-      return Cursor'(
-        Object.Container.all'Unrestricted_Access, Object.Container.Tree.Last);
    end Last;
 
    ------------------
@@ -1194,9 +1196,9 @@ package body Ada.Containers.Ordered_Sets is
    begin
       if Container.Tree.Last = null then
          raise Constraint_Error with "set is empty";
+      else
+         return Container.Tree.Last.Element;
       end if;
-
-      return Container.Tree.Last.Element;
    end Last_Element;
 
    ----------
@@ -1300,13 +1302,12 @@ package body Ada.Containers.Ordered_Sets is
       declare
          Node : constant Node_Access :=
                   Tree_Operations.Previous (Position.Node);
-
       begin
          if Node = null then
             return No_Element;
+         else
+            return Cursor'(Position.Container, Node);
          end if;
-
-         return Cursor'(Position.Container, Node);
       end;
    end Previous;
 

gcc/ada/alfa.ads

@@ -175,6 +175,11 @@ package ALFA is
    --        r = reference
    --        s = subprogram reference in a static call
 
+   --  Special entries for reads and writes to memory reference a special
+   --  variable called "HEAP". These special entries are present in every scope
+   --  where reads and writes to memory are present. Line and column for this
+   --  special variable are always 0.
+
    --    Examples: ??? add examples here
 
    ----------------
@@ -327,6 +332,14 @@ package ALFA is
      Table_Initial        => 20,
      Table_Increment      => 200);
 
+   ---------------
+   -- Constants --
+   ---------------
+
+   Name_Of_Heap_Variable : constant String := "HEAP";
+   --  Name of special variable used in effects to denote reads and writes
+   --  through explicit dereference.
+
    -----------------
    -- Subprograms --
    -----------------

gcc/ada/exp_ch3.adb

@@ -6607,10 +6607,12 @@ package body Exp_Ch3 is
 
             --  When compiling in Ada 2012 mode, ensure that the accessibility
             --  level of the subpool access type is not deeper than that of the
-            --  pool_with_subpools.
+            --  pool_with_subpools. This check is not performed on .NET/JVM
+            --  since those targets do not support pools.
 
             elsif Ada_Version >= Ada_2012
               and then Present (Associated_Storage_Pool (Def_Id))
+              and then VM_Target = No_VM
             then
                declare
                   Loc   : constant Source_Ptr := Sloc (Def_Id);
@@ -6642,7 +6644,7 @@ package body Exp_Ch3 is
                      --  Dynamic case: when the pool is of a class-wide type,
                      --  it may or may not support subpools depending on the
                      --  path of derivation. Generate:
-                     --
+
                      --    if Def_Id in RSPWS'Class then
                      --       raise Program_Error;
                      --    end if;

gcc/ada/exp_dist.adb

@@ -10550,6 +10550,7 @@ package body Exp_Dist is
                                        Add_Params_For_Variant_Components;
                                        J := J + Uint_1;
                                     end loop;
+
                                     Choice_Index :=
                                       Choice_Index + UI_To_Int (H - L) + 1;
                                  end;
@@ -10591,10 +10592,9 @@ package body Exp_Dist is
                                  Add_Params_For_Variant_Components;
                                  Choice_Index := Choice_Index + 1;
 
-                              when others =>
-
-                                 --  Case of an explicit choice
+                              --  Case of an explicit choice
 
+                              when others =>
                                  declare
                                     Exp : constant Node_Id :=
                                             New_Copy_Tree (Choice);

gcc/ada/lib-xref-alfa.adb

@@ -25,6 +25,7 @@
 
 with ALFA;        use ALFA;
 with Einfo;       use Einfo;
+with Nmake;       use Nmake;
 with Put_ALFA;
 with GNAT.HTable;
 
@@ -143,6 +144,22 @@ package body ALFA is
    type Entity_Hashed_Range is range 0 .. 255;
    --  Size of hash table headers
 
+   ---------------------
+   -- Local Variables --
+   ---------------------
+
+   package Drefs is new Table.Table (
+     Table_Component_Type => Xref_Entry,
+     Table_Index_Type     => Xref_Entry_Number,
+     Table_Low_Bound      => 1,
+     Table_Initial        => Alloc.Xrefs_Initial,
+     Table_Increment      => Alloc.Xrefs_Increment,
+     Table_Name           => "Drefs");
+   --  Table of cross-references for reads and writes through explicit
+   --  dereferences, that are output as reads/writes to the special variable
+   --  "HEAP". These references are added to the regular references when
+   --  computing ALFA cross-references.
+
    -----------------------
    -- Local Subprograms --
    -----------------------
@@ -400,7 +417,9 @@ package body ALFA is
       --  when we eliminate duplicate reference entries as well as references
       --  not suitable for local cross-references.
 
-      Rnums : array (0 .. Nrefs) of Nat;
+      Nrefs_Add : constant Nat := Drefs.Last;
+
+      Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
       --  This array contains numbers of references in the Xrefs table. This
       --  list is sorted in output order. The extra 0'th entry is convenient
       --  for the call to sort. When we sort the table, we move the entries in
@@ -506,6 +525,8 @@ package body ALFA is
          Rnums (Nat (To)) := Rnums (Nat (From));
       end Move;
 
+      Heap : Entity_Id;
+
       --  Start of processing for Add_ALFA_Xrefs
    begin
 
@@ -520,6 +541,31 @@ package body ALFA is
          Rnums (J) := J;
       end loop;
 
+      --  Add dereferences to the set of regular references, by creating a
+      --  special "HEAP" variable for these special references.
+
+      Name_Len := Name_Of_Heap_Variable'Length;
+      Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
+
+      Atree.Unlock;
+      Nlists.Unlock;
+      Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
+      Atree.Lock;
+      Nlists.Lock;
+
+      Set_Ekind         (Heap, E_Variable);
+      Set_Is_Internal   (Heap, True);
+      Set_Has_Fully_Qualified_Name (Heap);
+
+      for J in Drefs.First .. Drefs.Last loop
+         Xrefs.Increment_Last;
+         Xrefs.Table (Xrefs.Last)     := Drefs.Table (J);
+         Xrefs.Table (Xrefs.Last).Ent := Heap;
+
+         Nrefs         := Nrefs + 1;
+         Rnums (Nrefs) := Xrefs.Last;
+      end loop;
+
       --  Eliminate entries not appropriate for ALFA. Done prior to sorting
       --  cross-references, as it discards useless references which do not have
       --  a proper format for the comparison function (like no location).
@@ -762,16 +808,29 @@ package body ALFA is
                  new String'(Unique_Name (XE.Ent));
             end if;
 
-            ALFA_Xref_Table.Append (
-              (Entity_Name => Cur_Entity_Name,
-               Entity_Line => Int (Get_Logical_Line_Number (XE.Def)),
-               Etype       => Get_Entity_Type (XE.Ent),
-               Entity_Col  => Int (Get_Column_Number (XE.Def)),
-               File_Num    => Dependency_Num (XE.Lun),
-               Scope_Num   => Get_Scope_Num (XE.Ref_Scope),
-               Line        => Int (Get_Logical_Line_Number (XE.Loc)),
-               Rtype       => XE.Typ,
-               Col         => Int (Get_Column_Number (XE.Loc))));
+            if XE.Ent = Heap then
+               ALFA_Xref_Table.Append (
+                 (Entity_Name => Cur_Entity_Name,
+                  Entity_Line => 0,
+                  Etype       => Get_Entity_Type (XE.Ent),
+                  Entity_Col  => 0,
+                  File_Num    => Dependency_Num (XE.Lun),
+                  Scope_Num   => Get_Scope_Num (XE.Ref_Scope),
+                  Line        => Int (Get_Logical_Line_Number (XE.Loc)),
+                  Rtype       => XE.Typ,
+                  Col         => Int (Get_Column_Number (XE.Loc))));
+            else
+               ALFA_Xref_Table.Append (
+                 (Entity_Name => Cur_Entity_Name,
+                  Entity_Line => Int (Get_Logical_Line_Number (XE.Def)),
+                  Etype       => Get_Entity_Type (XE.Ent),
+                  Entity_Col  => Int (Get_Column_Number (XE.Def)),
+                  File_Num    => Dependency_Num (XE.Lun),
+                  Scope_Num   => Get_Scope_Num (XE.Ref_Scope),
+                  Line        => Int (Get_Logical_Line_Number (XE.Loc)),
+                  Rtype       => XE.Typ,
+                  Col         => Int (Get_Column_Number (XE.Loc))));
+            end if;
          end Add_One_Xref;
       end loop;
 
@@ -877,6 +936,84 @@ package body ALFA is
       end if;
    end Detect_And_Add_ALFA_Scope;
 
+   -------------------------------------
+   -- Enclosing_Subprogram_Or_Package --
+   -------------------------------------
+
+   function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is
+      Result : Entity_Id;
+
+   begin
+      --  If N is the defining identifier for a subprogram, then return the
+      --  enclosing subprogram or package, not this subprogram.
+
+      if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
+        and then Nkind (Parent (N)) in N_Subprogram_Specification
+      then
+         Result := Parent (Parent (Parent (N)));
+      else
+         Result := N;
+      end if;
+
+      loop
+         exit when No (Result);
+
+         case Nkind (Result) is
+            when N_Package_Specification =>
+               Result := Defining_Unit_Name (Result);
+               exit;
+
+            when N_Package_Body =>
+               Result := Defining_Unit_Name (Result);
+               exit;
+
+            when N_Subprogram_Specification =>
+               Result := Defining_Unit_Name (Result);
+               exit;
+
+            when N_Subprogram_Declaration =>
+               Result := Defining_Unit_Name (Specification (Result));
+               exit;
+
+            when N_Subprogram_Body =>
+               Result := Defining_Unit_Name (Specification (Result));
+               exit;
+
+            --  The enclosing subprogram for a pre- or postconditions should be
+            --  the subprogram to which the pragma is attached. This is not
+            --  always the case in the AST, as the pragma may be declared after
+            --  the declaration of the subprogram. Return Empty in this case.
+
+            when N_Pragma =>
+               if Get_Pragma_Id (Result) = Pragma_Precondition
+                    or else
+                  Get_Pragma_Id (Result) = Pragma_Postcondition
+               then
+                  return Empty;
+               else
+                  Result := Parent (Result);
+               end if;
+
+            when others =>
+               Result := Parent (Result);
+         end case;
+      end loop;
+
+      if Nkind (Result) = N_Defining_Program_Unit_Name then
+         Result := Defining_Identifier (Result);
+      end if;
+
+      --  Do no return a scope without a proper location
+
+      if Present (Result)
+        and then Sloc (Result) = No_Location
+      then
+         return Empty;
+      end if;
+
+      return Result;
+   end Enclosing_Subprogram_Or_Package;
+
    -----------------
    -- Entity_Hash --
    -----------------
@@ -887,6 +1024,47 @@ package body ALFA is
         Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
    end Entity_Hash;
 
+   --------------------------
+   -- Generate_Dereference --
+   --------------------------
+
+   procedure Generate_Dereference
+     (N   : Node_Id;
+      Typ : Character := 'r')
+   is
+      Indx      : Nat;
+      Ref       : Source_Ptr;
+      Ref_Scope : Entity_Id;
+
+   begin
+      Ref := Original_Location (Sloc (N));
+
+      if Ref > No_Location then
+         Drefs.Increment_Last;
+         Indx := Drefs.Last;
+
+         Ref_Scope := Enclosing_Subprogram_Or_Package (N);
+
+         --  Entity is filled later on with the special "HEAP" variable
+
+         Drefs.Table (Indx).Ent := Empty;
+
+         Drefs.Table (Indx).Def := No_Location;
+         Drefs.Table (Indx).Loc := Ref;
+         Drefs.Table (Indx).Typ := Typ;
+
+         --  It is as if the special "HEAP" was defined in every scope where it
+         --  is referenced.
+
+         Drefs.Table (Indx).Eun := Get_Source_Unit (Ref);
+         Drefs.Table (Indx).Lun := Get_Source_Unit (Ref);
+
+         Drefs.Table (Indx).Ref_Scope := Ref_Scope;
+         Drefs.Table (Indx).Ent_Scope := Ref_Scope;
+         Drefs.Table (Indx).Ent_Scope_File := Get_Source_Unit (Ref_Scope);
+      end if;
+   end Generate_Dereference;
+
    ------------------------------------
    -- Traverse_All_Compilation_Units --
    ------------------------------------

gcc/ada/lib-xref.adb

@@ -112,9 +112,6 @@ package body Lib.Xref is
    --  Local Subprograms --
    ------------------------
 
-   function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id;
-   --  Return the closest enclosing subprogram of package
-
    procedure Generate_Prim_Op_References (Typ : Entity_Id);
    --  For a tagged type, generate implicit references to its primitive
    --  operations, for source navigation. This is done right before emitting
@@ -124,84 +121,6 @@ package body Lib.Xref is
    function Lt (T1, T2 : Xref_Entry) return Boolean;
    --  Order cross-references
 
-   -------------------------------------
-   -- Enclosing_Subprogram_Or_Package --
-   -------------------------------------
-
-   function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is
-      Result : Entity_Id;
-
-   begin
-      --  If N is the defining identifier for a subprogram, then return the
-      --  enclosing subprogram or package, not this subprogram.
-
-      if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
-        and then Nkind (Parent (N)) in N_Subprogram_Specification
-      then
-         Result := Parent (Parent (Parent (N)));
-      else
-         Result := N;
-      end if;
-
-      loop
-         exit when No (Result);
-
-         case Nkind (Result) is
-            when N_Package_Specification =>
-               Result := Defining_Unit_Name (Result);
-               exit;
-
-            when N_Package_Body =>
-               Result := Defining_Unit_Name (Result);
-               exit;
-
-            when N_Subprogram_Specification =>
-               Result := Defining_Unit_Name (Result);
-               exit;
-
-            when N_Subprogram_Declaration =>
-               Result := Defining_Unit_Name (Specification (Result));
-               exit;
-
-            when N_Subprogram_Body =>
-               Result := Defining_Unit_Name (Specification (Result));
-               exit;
-
-            --  The enclosing subprogram for a pre- or postconditions should be
-            --  the subprogram to which the pragma is attached. This is not
-            --  always the case in the AST, as the pragma may be declared after
-            --  the declaration of the subprogram. Return Empty in this case.
-
-            when N_Pragma =>
-               if Get_Pragma_Id (Result) = Pragma_Precondition
-                    or else
-                  Get_Pragma_Id (Result) = Pragma_Postcondition
-               then
-                  return Empty;
-               else
-                  Result := Parent (Result);
-               end if;
-
-            when others =>
-               Result := Parent (Result);
-         end case;
-      end loop;
-
-      if Nkind (Result) = N_Defining_Program_Unit_Name then
-         Result := Defining_Identifier (Result);
-      end if;
-
-      --  Do no return a scope without a proper location
-
-      if Present (Result)
-        and then Sloc (Result) = No_Location
-      then
-         return Empty;
-      end if;
-
-      return Result;
-   end Enclosing_Subprogram_Or_Package;
-
    -------------------------
    -- Generate_Definition --
    -------------------------
@@ -946,8 +865,8 @@ package body Lib.Xref is
          Ref := Original_Location (Sloc (Nod));
          Def := Original_Location (Sloc (Ent));
 
-         Ref_Scope := Enclosing_Subprogram_Or_Package (N);
-         Ent_Scope := Enclosing_Subprogram_Or_Package (Ent);
+         Ref_Scope := ALFA.Enclosing_Subprogram_Or_Package (N);
+         Ent_Scope := ALFA.Enclosing_Subprogram_Or_Package (Ent);
 
          Xrefs.Increment_Last;
          Indx := Xrefs.Last;

gcc/ada/lib-xref.ads

@@ -590,6 +590,15 @@ package Lib.Xref is
 
    package ALFA is
 
+      function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id;
+      --  Return the closest enclosing subprogram of package
+
+      procedure Generate_Dereference
+        (N   : Node_Id;
+         Typ : Character := 'r');
+      --  This procedure is called to record a dereference. N is the location
+      --  of the dereference.
+
       type Node_Processing is access procedure (N : Node_Id);
 
       procedure Traverse_Compilation_Unit

gcc/ada/put_alfa.adb

@@ -153,8 +153,11 @@ begin
                   Write_Info_Char (S.Scope_Name (N));
                end loop;
 
+               --  Default value of (0,0) is used for the special HEAP variable
+               --  so use another default value.
+
                Entity_Line := 0;
-               Entity_Col  := 0;
+               Entity_Col  := 1;
 
                --  Loop through cross reference entries for this scope
 

gcc/ada/sem_ch10.adb

@@ -5041,6 +5041,7 @@ package body Sem_Ch10 is
               ("instantiation depends on itself", Name (With_Clause));
 
          elsif not Is_Visible_Child_Unit (Uname) then
+
             --  Abandon processing in case of previous errors
 
             if No (Scope (Uname)) then

gcc/ada/sem_ch4.adb

@@ -1761,6 +1761,13 @@ package body Sem_Ch4 is
    begin
       Check_SPARK_Restriction ("explicit dereference is not allowed", N);
 
+      --  In formal verification mode, keep track of all reads and writes
+      --  through explicit dereferences.
+
+      if ALFA_Mode then
+         ALFA.Generate_Dereference (N);
+      end if;
+
       Analyze (P);
       Set_Etype (N, Any_Type);
 

gcc/ada/sem_util.adb

@@ -10506,6 +10506,13 @@ package body Sem_Util is
                P : constant Node_Id := Prefix (Exp);
 
             begin
+               --  In formal verification mode, keep track of all reads and
+               --  writes through explicit dereferences.
+
+               if ALFA_Mode then
+                  ALFA.Generate_Dereference (N, 'm');
+               end if;
+
                if Nkind (P) = N_Selected_Component
                  and then Present (
                    Entry_Formal (Entity (Selector_Name (P))))