[Ada] Analyze pre/post expression for correctness in formal verification mode

[Arnaud Charlet]

Since expansion of pre/post is skipped in formal verification mode, the
analysis of pre/post expressions for correctness, and to complete nodes with
their types, was missing. Now corrected.

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

2011-08-29  Yannick Moy  <m...@adacore.com>

        * sem_prag.adb (Check_Precondition_Postcondition): In formal
        verification mode, analyze pragma expression for correctness, for
        pre/post on library-level subprogram, as it is not expanded later.


Index: sem_prag.adb
===================================================================
--- sem_prag.adb        (revision 178155)
+++ sem_prag.adb        (working copy)
@@ -1884,6 +1884,15 @@
          --  See if it is in the pragmas after a library level subprogram
 
          elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then
+
+            --  In formal verification mode, analyze pragma expression for
+            --  correctness, as it is not expanded later.
+
+            if ALFA_Mode then
+               Analyze_PPC_In_Decl_Part
+                 (N, Defining_Entity (Unit (Parent (Parent (N)))));
+            end if;
+
             Chain_PPC (Unit (Parent (Parent (N))));
             return;
          end if;