diff mbox

[Ada] Filter constants from effect information in ALI files

Message ID 20110905130327.GA14177@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Sept. 5, 2011, 1:03 p.m. UTC 
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  <kanig@adacore.com>

	* lib-xref-alfa.adb (Is_Alfa_Reference): Filter constants from effect
	information.
diff mbox

Patch

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;