[Ada] Special expansion in ALFA for pragma check/precondition/postcondition

[Ada] Special expansion in ALFA for pragma check/precondition/postcondition

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 517 bytes --]

In ALFA mode, we modify expansion so that pragma check are kept in the code,
while pre- and postconditions are kept attached to entities rather than
being inserted in the code.

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

2011-08-04  Yannick Moy  <moy@adacore.com>

	* exp_prag.adb (Expand_Pragma_Check): in ALFA mode, return without
	performing expansion.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper,
	Analyze_Generic_Subprogram_Body): protect call to Process_PCCs so that
	it is not called in ALFA mode.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 2759 bytes --]

Index: exp_prag.adb
===================================================================
--- exp_prag.adb	(revision 177274)
+++ exp_prag.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -321,6 +321,12 @@
       --  be an explicit conditional in the source, not an implicit if, so we
       --  do not call Make_Implicit_If_Statement.
 
+      --  In formal verification mode, we keep the pragma check in the code
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Case where we generate a direct raise
 
       if ((Debug_Flag_Dot_G
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 177371)
+++ sem_ch6.adb	(working copy)
@@ -962,8 +962,16 @@
          end if;
 
          Set_Actual_Subtypes (N, Current_Scope);
-         Process_PPCs (N, Gen_Id, Body_Id);
 
+         --  Deal with preconditions and postconditions. In formal verification
+         --  mode, we keep pre- and postconditions attached to entities rather
+         --  than inserted in the code, in order to facilitate a distinct
+         --  treatment for them.
+
+         if not ALFA_Mode then
+            Process_PPCs (N, Gen_Id, Body_Id);
+         end if;
+
          --  If the generic unit carries pre- or post-conditions, copy them
          --  to the original generic tree, so that they are properly added
          --  to any instantiation.
@@ -2663,9 +2671,14 @@
       HSS := Handled_Statement_Sequence (N);
       Set_Actual_Subtypes (N, Current_Scope);
 
-      --  Deal with preconditions and postconditions
+      --  Deal with preconditions and postconditions. In formal verification
+      --  mode, we keep pre- and postconditions attached to entities rather
+      --  than inserted in the code, in order to facilitate a distinct
+      --  treatment for them.
 
-      Process_PPCs (N, Spec_Id, Body_Id);
+      if not ALFA_Mode then
+         Process_PPCs (N, Spec_Id, Body_Id);
+      end if;
 
       --  Add a declaration for the Protection object, renaming declarations
       --  for discriminals and privals and finally a declaration for the entry