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;

Reply via email to