Constants cannot be modified, and so should never appear in the ALFA section
of ALI files as effects. This patch enforces this property.
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): Filter constants from effect
information.
Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb (revision 178531)
+++ lib-xref-alfa.adb (working copy)
@@ -616,7 +616,9 @@
-- section, as these will be translated as constants in the
-- intermediate language for formal verification.
- when E_In_Parameter =>
+ -- Above comment is incomplete??? what about E_Constant case
+
+ when E_In_Parameter | E_Constant =>
return False;
when others =>
@@ -624,18 +626,13 @@
-- Objects of Task type or protected type are not Alfa
-- references.
- if Present (Etype (E)) then
- case Ekind (Etype (E)) is
- when E_Task_Type | E_Protected_Type =>
- return False;
-
- when others =>
- null;
- end case;
+ if Present (Etype (E))
+ and then Ekind (Etype (E)) in Concurrent_Kind
+ then
+ return False;
end if;
return Typ = 'r' or else Typ = 'm';
-
end case;
end Is_Alfa_Reference;
