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 <m...@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.
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;