OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

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
This commit is contained in:
Yannick Moy 2017-09-11 08:06:46 +00:00 committed by Arnaud Charlet
parent 16707e90f9
commit 6afd4d646d
3 changed files with 10 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
gcc/ada/ChangeLog
View File

@ -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

2
gcc/ada/gnat1drv.adb
View File

@ -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.

2
gcc/ada/opt.ads
View File

@ -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