diff mbox

[Ada] Switch -gnatp should have no effect in GNATprove mode

Message ID 20141031114320.GA3125@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 31, 2014, 11:43 a.m. UTC
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  <moy@adacore.com>

	* gnat1drv.adb (Adjust_Global_Switches): Explicitly mark language
	checks as not suppressed in GNATprove mode.
diff mbox

Patch

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.