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