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