diff options
| author | Yannick Moy <moy@adacore.com> | 2017-09-11 08:06:46 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-09-11 10:06:46 +0200 |
| commit | 6afd4d646d9b262fdb409274af69d2c7ad3f53db (patch) | |
| tree | 9eeabd151b8644ddec572e45cf68a30d14695621 | |
| parent | 16707e90f935452e4ce65e04e0a2047b6b083eb3 (diff) | |
| download | gcc-6afd4d646d9b262fdb409274af69d2c7ad3f53db.zip gcc-6afd4d646d9b262fdb409274af69d2c7ad3f53db.tar.gz gcc-6afd4d646d9b262fdb409274af69d2c7ad3f53db.tar.bz2 | |
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
| -rw-r--r-- | gcc/ada/ChangeLog | 7 | ||||
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/opt.ads | 2 |
3 files changed, 10 insertions, 1 deletions
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 |