[Ada] Avoid spurious error in GNATprove mode on non-null access types

GNATprove directly handles non-null access checks, and requires that the
frontend does not insert explicit checks in the form of conditional
exceptions being raised. Now fixed.

There is no impact on compilation.

2019-08-21  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* checks.adb (Install_Null_Excluding_Check): Do not install
	check in GNATprove mode.

From-SVN: r274780
This commit is contained in:
Yannick Moy 2019-08-21 08:29:51 +00:00 committed by Pierre-Marie de Rodat
parent 570d0072bd
commit 5c34f30d16
2 changed files with 11 additions and 0 deletions

View File

@ -1,3 +1,8 @@
2019-08-21 Yannick Moy <moy@adacore.com>
* checks.adb (Install_Null_Excluding_Check): Do not install
check in GNATprove mode.
2019-08-21 Yannick Moy <moy@adacore.com>
* sem_spark.adb (Process_Path): Do nothing on address of

View File

@ -7964,6 +7964,12 @@ package body Checks is
return;
end if;
-- In GNATprove mode, we do not apply the check
if GNATprove_Mode then
return;
end if;
-- Otherwise install access check
Insert_Action (N,