The test which filters constants objects so that they do not appear in the
ALFA sections of ALI files did not cover all the cases. This patch corrects
the problem.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-09-05 Johannes Kanig <ka...@adacore.com>
* lib-xref-alfa.adb (Is_Alfa_Reference): Improve test for constant
objects and rewrite case statement as /if/elsif/endif.
Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb (revision 178536)
+++ lib-xref-alfa.adb (working copy)
@@ -604,38 +604,36 @@
Typ : Character) return Boolean
is
begin
- -- The only references of interest on callable entities are calls.
- -- On non-callable entities, the only references of interest are
- -- reads and writes.
- case Ekind (E) is
- when Overloadable_Kind =>
- return Typ = 's';
+ if Ekind (E) in Overloadable_Kind then
- -- References to IN parameters and constants are not
- -- considered in Alfa section, as these will be translated
- -- as constants in the intermediate language for formal
- -- verification, and should therefore never appear in frame
- -- conditions.
+ -- The only references of interest on callable entities are
+ -- calls. On non-callable entities, the only references of
+ -- interest are reads and writes.
- -- What about E_Loop_Parameter???
+ return Typ = 's';
- when E_In_Parameter | E_Constant =>
+ elsif Is_Constant_Object (E) then
+
+ -- References to constant objects are not considered in Alfa
+ -- section, as these will be translated as constants in the
+ -- intermediate language for formal verification, and should
+ -- therefore never appear in frame conditions.
+
return False;
- when others =>
+ elsif Present (Etype (E)) and then
+ Ekind (Etype (E)) in Concurrent_Kind then
- -- Objects of Task type or protected type are not Alfa
- -- references.
+ -- Objects of Task type or protected type are not Alfa
+ -- references.
- if Present (Etype (E))
- and then Ekind (Etype (E)) in Concurrent_Kind
- then
- return False;
- end if;
+ return False;
- return Typ = 'r' or else Typ = 'm';
- end case;
+ else
+ return Typ = 'r' or else Typ = 'm';
+
+ end if;
end Is_Alfa_Reference;
-------------------
