diff mbox series

[Ada] Suppress generation of ABE checks in GNATprove mode

Message ID 20171009195944.GA43490@adacore.com
State New
Headers show
Series [Ada] Suppress generation of ABE checks in GNATprove mode | expand

Commit Message

Pierre-Marie de Rodat Oct. 9, 2017, 7:59 p.m. UTC 
This patch suppresses the generation of ABE checks when compiling for GNATprove
because a) the checks are not needed and b) the checks involve raise statements
which are not supported by GNATprove. No need for a test.

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

2017-10-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb (Install_ABE_Check): Do not generate an ABE check for
	GNATprove.
	(Install_ABE_Failure): Do not generate an ABE failure for GNATprove.
diff mbox series

Patch

Index: sem_elab.adb
===================================================================
--- sem_elab.adb	(revision 253559)
+++ sem_elab.adb	(working copy)
@@ -4199,9 +4199,15 @@ 
       Scop_Id : Entity_Id;
 
    begin
+      --  Nothing to do when compiling for GNATprove because raise statements
+      --  are not supported.
+
+      if GNATprove_Mode then
+         return;
+
       --  Nothing to do when the compilation will not produce an executable
 
-      if Serious_Errors_Detected > 0 then
+      elsif Serious_Errors_Detected > 0 then
          return;
 
       --  Nothing to do for a compilation unit because there is no executable
@@ -4325,9 +4331,15 @@ 
    --  Start for processing for Install_ABE_Check
 
    begin
+      --  Nothing to do when compiling for GNATprove because raise statements
+      --  are not supported.
+
+      if GNATprove_Mode then
+         return;
+
       --  Nothing to do when the compilation will not produce an executable
 
-      if Serious_Errors_Detected > 0 then
+      elsif Serious_Errors_Detected > 0 then
          return;
 
       --  Nothing to do when the target is a protected subprogram because the
@@ -4381,9 +4393,15 @@ 
       Scop_Id : Entity_Id;
 
    begin
+      --  Nothing to do when compiling for GNATprove because raise statements
+      --  are not supported.
+
+      if GNATprove_Mode then
+         return;
+
       --  Nothing to do when the compilation will not produce an executable
 
-      if Serious_Errors_Detected > 0 then
+      elsif Serious_Errors_Detected > 0 then
          return;
 
       --  Do not install an ABE check for a compilation unit because there is