Patchwork [Ada] Remove IN parameters from Alfa section in ALI

login
register
mail settings
Submitter Arnaud Charlet
Date Sept. 2, 2011, 9:22 a.m.
Message ID <20110902092223.GA11331@adacore.com>
Download mbox | patch
Permalink /patch/113065/
State New
Headers show

Comments

Arnaud Charlet - Sept. 2, 2011, 9:22 a.m.
References to IN parameters are not considered in Alfa section, as these will
be translated as constants in the intermediate language for formal
verification.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-09-02  Yannick Moy  <moy@adacore.com>

	* lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa
	references.

Patch

Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb	(revision 178438)
+++ lib-xref-alfa.adb	(working copy)
@@ -608,11 +608,20 @@ 
             --  On non-callable entities, the only references of interest are
             --  reads and writes.
 
-            if Ekind (E) in Overloadable_Kind then
-               return Typ = 's';
-            else
-               return Typ = 'r' or else Typ = 'm';
-            end if;
+            case Ekind (E) is
+               when Overloadable_Kind =>
+                  return Typ = 's';
+
+               --  References to IN parameters are not considered in Alfa
+               --  section, as these will be translated as constants in the
+               --  intermediate language for formal verification.
+
+               when E_In_Parameter =>
+                  return False;
+
+               when others =>
+                  return Typ = 'r' or else Typ = 'm';
+            end case;
          end Is_Alfa_Reference;
 
          -------------------