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