diff mbox

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

Message ID 20110829082209.GA13955@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 29, 2011, 8:22 a.m. UTC 
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  <moy@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.
diff mbox

Patch

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;