diff mbox

[Ada] Define unique entity for parameter (used in Alfa mode)

Message ID 20111107162246.GA7683@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Nov. 7, 2011, 4:22 p.m. UTC 
For the formal verification backend, to be used in Alfa mode, define the unique
entity representing a parameter.

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

2011-11-07  Yannick Moy  <moy@adacore.com>

	* sem_util.adb (Unique_Entity): For a parameter on a subprogram
	body that has a corresponding parameter on the subprogram
	declaration, define the unique entity as being the declaration
	one.
diff mbox

Patch

Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 181090)
+++ sem_util.adb	(working copy)
@@ -12835,6 +12835,11 @@ 
                U := Corresponding_Spec (P);
             end if;
 
+         when Formal_Kind =>
+            if Present (Spec_Entity (E)) then
+               U := Spec_Entity (E);
+            end if;
+
          when others =>
             null;
       end case;