The cross references generated for formal verification in GNATprove mode
did not include constant objects. The needs have changed, and these should
be included now, with a specific type character 'c' to distinguish them
from references to non-constant objects.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-27 Yannick Moy <m...@adacore.com>
* get_spark_xrefs.adb (Get_SPARK_Xrefs): Accept new type 'c' for
reference.
* lib-xref-spark_specific.adb (Is_Global_Constant): Remove useless
function now.
(Add_SPARK_Xrefs): Include references to constants.
* spark_xrefs.ads Document new character 'c' for references to
constants.
Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb (revision 207120)
+++ lib-xref-spark_specific.adb (working copy)
@@ -334,10 +334,6 @@
S : Scope_Index) return Boolean;
-- Check whether entity E is in SPARK_Scope_Table at index S or higher
- function Is_Global_Constant (E : Entity_Id) return Boolean;
- -- Return True if E is a global constant for which we should ignore
- -- reads in SPARK.
-
function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
-- Comparison function for Sort call
@@ -440,14 +436,6 @@
if Ekind (E) in Overloadable_Kind then
return Typ = 's';
- -- References to constant objects are not considered in SPARK
- -- section, as these will be translated as constants in the
- -- intermediate language for formal verification, and should
- -- therefore never appear in frame conditions.
-
- elsif Is_Constant_Object (E) then
- return False;
-
-- Objects of Task type or protected type are not SPARK references
elsif Present (Etype (E))
@@ -526,16 +514,6 @@
return False;
end Is_Future_Scope_Entity;
- ------------------------
- -- Is_Global_Constant --
- ------------------------
-
- function Is_Global_Constant (E : Entity_Id) return Boolean is
- begin
- return Ekind (E) = E_Constant
- and then Ekind_In (Scope (E), E_Package, E_Package_Body);
- end Is_Global_Constant;
-
--------
-- Lt --
--------
@@ -726,7 +704,6 @@
and then SPARK_References (Ref.Typ)
and then Is_SPARK_Scope (Ref.Ent_Scope)
and then Is_SPARK_Scope (Ref.Ref_Scope)
- and then not Is_Global_Constant (Ref.Ent)
and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
-- Discard references from unknown scopes, e.g. generic scopes
@@ -805,6 +782,7 @@
declare
Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
Ref : Xref_Key renames Ref_Entry.Key;
+ Typ : Character;
begin
-- If this assertion fails, the scope which we are looking for is
@@ -844,6 +822,17 @@
Col := Int (Get_Column_Number (Ref_Entry.Def));
end if;
+ -- References to constant objects are considered specially in
+ -- SPARK section, because these will be translated as constants in
+ -- the intermediate language for formal verification, and should
+ -- therefore never appear in frame conditions.
+
+ if Is_Constant_Object (Ref.Ent) then
+ Typ := 'c';
+ else
+ Typ := Ref.Typ;
+ end if;
+
SPARK_Xref_Table.Append (
(Entity_Name => Ref_Name,
Entity_Line => Line,
@@ -852,7 +841,7 @@
File_Num => Dependency_Num (Ref.Lun),
Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
Line => Int (Get_Logical_Line_Number (Ref.Loc)),
- Rtype => Ref.Typ,
+ Rtype => Typ,
Col => Int (Get_Column_Number (Ref.Loc))));
end;
end loop;
Index: spark_xrefs.ads
===================================================================
--- spark_xrefs.ads (revision 207120)
+++ spark_xrefs.ads (working copy)
@@ -177,6 +177,7 @@
-- m = modification
-- r = reference
+ -- c = reference to constant object
-- s = subprogram reference in a static call
-- Special entries for reads and writes to memory reference a special
@@ -229,6 +230,7 @@
Rtype : Character;
-- Indicates type of reference, using code used in ALI file:
-- r = reference
+ -- c = reference to constant object
-- m = modification
-- s = call
Index: get_spark_xrefs.adb
===================================================================
--- get_spark_xrefs.adb (revision 207120)
+++ get_spark_xrefs.adb (working copy)
@@ -455,6 +455,7 @@
pragma Assert
(Rtype = 'r' or else
+ Rtype = 'c' or else
Rtype = 'm' or else
Rtype = 's');
