From d8be36d2873dd1cf9586790ff6c91dc17f37daa6 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Thu, 4 Jul 2019 08:05:27 +0000 Subject: [PATCH] [Ada] Keep assertions in internal units enabled for GNATprove In GNATprove mode the assertion policy is now always enabled, even when analysing internal units. Otherwise, assertion expressions (e.g. Default_Initial_Condition) in internal units (e.g. Ada.Text_IO) disappear in the semantic analysis phase of the frontend and the GNATprove backend can't see them. No frontend test provided, because only the GNATprove backend is affected (and there appear to be no difference in the output with -gnatG switch, because the expansion of Default_Initial_Condition is not attached to the AST). 2019-07-04 Piotr Trojanek gcc/ada/ * opt.adb (Set_Config_Switches): Keep assertions policy as enabled when analysing internal units in GNATprove mode. From-SVN: r273048 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/opt.adb | 8 +++++++- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1a86a4d..ea1d75d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-04 Piotr Trojanek + + * opt.adb (Set_Config_Switches): Keep assertions policy as + enabled when analysing internal units in GNATprove mode. + 2019-07-04 Arnaud Charlet * exp_ch4.adb (Expand_Short_Circuit_Operator): Strip diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb index 43d340b..05f9059 100644 --- a/gcc/ada/opt.adb +++ b/gcc/ada/opt.adb @@ -248,7 +248,13 @@ package body Opt is SPARK_Mode_Pragma := SPARK_Mode_Pragma_Config; else - if GNAT_Mode_Config then + -- In GNATprove mode assertions should be always enabled, even + -- when analysing internal units. + + if GNATprove_Mode then + pragma Assert (Assertions_Enabled); + null; + elsif GNAT_Mode_Config then Assertions_Enabled := Assertions_Enabled_Config; else Assertions_Enabled := False; -- 2.7.4