gnat1drv.adb (Adjust_Global_Switches): Set Check_Validity_Of_Parameters to False...

2017-09-11  Yannick Moy  <moy@adacore.com>

	* gnat1drv.adb (Adjust_Global_Switches): Set
	Check_Validity_Of_Parameters to False in GNATprove mode.
	* opt.ads (Check_Validity_Of_Parameters): Document switch to
	set option.

From-SVN: r251959

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index dee1897..81a0d9d 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2017-09-11  Yannick Moy  <moy@adacore.com>
+
+       * gnat1drv.adb (Adjust_Global_Switches): Set
+       Check_Validity_Of_Parameters to False in GNATprove mode.
+       * opt.ads (Check_Validity_Of_Parameters): Document switch to
+       set option.
+
 2017-09-09  Pierre-Marie de Rodat  <derodat@adacore.com>
 
        * gcc-interface/decl.c (gnat_to_gnu_entity) <E_Record_Type>: Don't

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index e60d912..3a0ceca 100644 (file)
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -356,6 +356,7 @@ procedure Gnat1drv is
          Reset_Validity_Check_Options;
          Validity_Check_Default       := True;
          Validity_Check_Copies        := True;
+         Check_Validity_Of_Parameters := False;
 
          --  Turn off style check options and ignore any style check pragmas
          --  since we are not interested in any front-end warnings when we are
@@ -508,6 +509,7 @@ procedure Gnat1drv is
          --  data is directly detected by GNATprove's flow analysis.
 
          Validity_Checks_On := False;
+         Check_Validity_Of_Parameters := False;
 
          --  Turn off style check options since we are not interested in any
          --  front-end warnings when we are getting SPARK output.

diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 1c7c0a0..687d1eb 100644 (file)
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -366,7 +366,7 @@ package Opt is
    Check_Validity_Of_Parameters : Boolean := False;
    --  GNAT
    --  Set to True to check for proper scalar initialization of subprogram
-   --  parameters on both entry and exit. Turned on by??? turned off by???
+   --  parameters on both entry and exit. This is turned on by -gnateV.
 
    Check_Withs : Boolean := False;
    --  GNAT