diff mbox series

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

Message ID 20190821083142.GA71850@adacore.com
State New
Headers show
Series [Ada] Avoid spurious error in GNATprove mode on non-null access types | expand

Commit Message

Pierre-Marie de Rodat Aug. 21, 2019, 8:31 a.m. UTC 
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.

Tested on x86_64-pc-linux-gnu, committed on trunk

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

gcc/ada/

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

Patch

--- gcc/ada/checks.adb
+++ gcc/ada/checks.adb
@@ -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,