diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2019-07-04 08:05:27 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-04 08:05:27 +0000 |
| commit | d8be36d2873dd1cf9586790ff6c91dc17f37daa6 (patch) | |
| tree | a214c57ccdb62bcbd45ac510a4760f3b80687ef3 | |
| parent | a0766a8258f014ac2715d8c49fcaf83b3eb62a00 (diff) | |
| download | gcc-d8be36d2873dd1cf9586790ff6c91dc17f37daa6.zip gcc-d8be36d2873dd1cf9586790ff6c91dc17f37daa6.tar.gz gcc-d8be36d2873dd1cf9586790ff6c91dc17f37daa6.tar.bz2 | |
[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 <trojanek@adacore.com>
gcc/ada/
* opt.adb (Set_Config_Switches): Keep assertions policy as
enabled when analysing internal units in GNATprove mode.
From-SVN: r273048
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/opt.adb | 8 |
2 files changed, 12 insertions, 1 deletions
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 <trojanek@adacore.com> + + * opt.adb (Set_Config_Switches): Keep assertions policy as + enabled when analysing internal units in GNATprove mode. + 2019-07-04 Arnaud Charlet <charlet@adacore.com> * 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; |