From: Yannick Moy <moy@adacore.com>
Date: Mon, 11 Sep 2017 08:06:46 +0000 (+0000)
Subject: gnat1drv.adb (Adjust_Global_Switches): Set Check_Validity_Of_Parameters to False... 
X-Git-Tag: upstream/12.2.0~37096
X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=6afd4d646d9b262fdb409274af69d2c7ad3f53db;p=platform%2Fupstream%2Fgcc.git

gnat1drv.adb (Adjust_Global_Switches): Set Check_Validity_Of_Parameters to False in GNATprove mode.

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 dee1897e..81a0d9d 100644
--- 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
--- 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
--- 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