diff options
| -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 |