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');
 

Reply via email to