In GNATprove mode for formal verification, the presence or absence of
switch -gnatp should have not effect. This was not the case, leading to
missing proofs in GNATprove for overflow/range/division checks when
-gnatp was used. Now fixed.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-10-31 Yannick Moy <[email protected]>
* gnat1drv.adb (Adjust_Global_Switches): Explicitly mark language
checks as not suppressed in GNATprove mode.
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb (revision 216925)
+++ gnat1drv.adb (working copy)
@@ -363,6 +363,12 @@
-- happens anyway because this expansion is simply not done in the
-- SPARK version of the expander.
+ -- On the contrary, we need to enable explicitly all language checks,
+ -- as they may have been marked as suppressed by the use of switch
+ -- -gnatp
+
+ Suppress_Options.Suppress := (others => False);
+
-- Turn off dynamic elaboration checks: generates inconsistencies in
-- trees between specs compiled as part of a main unit or as part of
-- a with-clause.
