[Ada] Keep assertions in internal units enabled for GNATprove
authorPiotr Trojanek <trojanek@adacore.com>
Thu, 4 Jul 2019 08:05:27 +0000 (08:05 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 4 Jul 2019 08:05:27 +0000 (08:05 +0000)
commitd8be36d2873dd1cf9586790ff6c91dc17f37daa6
treea214c57ccdb62bcbd45ac510a4760f3b80687ef3
parenta0766a8258f014ac2715d8c49fcaf83b3eb62a00
[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
gcc/ada/ChangeLog
gcc/ada/opt.adb