===================================================================
@@ -10506,6 +10506,13 @@
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))))
===================================================================
@@ -175,6 +175,11 @@
-- 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 @@
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 --
-----------------
===================================================================
@@ -1761,6 +1761,13 @@
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);
===================================================================
@@ -153,8 +153,11 @@
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
===================================================================
@@ -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 @@
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 @@
-- 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 @@
Rnums (Nat (To)) := Rnums (Nat (From));
end Move;
+ Heap : Entity_Id;
+
-- Start of processing for Add_ALFA_Xrefs
begin
@@ -520,6 +541,31 @@
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 @@
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 @@
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 @@
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 --
------------------------------------
===================================================================
@@ -112,9 +112,6 @@
-- 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 @@
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 @@
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;
===================================================================
@@ -590,6 +590,15 @@
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