===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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
===================================================================
@@ -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