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

login
register
mail settings
Submitter Arnaud Charlet
Date Nov. 7, 2011, 4:22 p.m.
Message ID <20111107162246.GA7683@adacore.com>
Download mbox | patch
Permalink /patch/124126/
State New
Headers show

Comments

Arnaud Charlet - Nov. 7, 2011, 4:22 p.m.
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.

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;