]> git.ipfire.org Git - thirdparty/gcc.git/commit
[Ada] Keep assertions in internal units enabled for GNATprove
authorpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Thu, 4 Jul 2019 08:05:27 +0000 (08:05 +0000)
committerpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Thu, 4 Jul 2019 08:05:27 +0000 (08:05 +0000)
commitb0c19ea3b6e415251e90df1cfedf3681578c576b
treea214c57ccdb62bcbd45ac510a4760f3b80687ef3
parent90f2b146305d631fa2f551a789f6413ebd63a072
[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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@273048 138bc75d-0d04-0410-961f-82ee72b054a4
gcc/ada/ChangeLog
gcc/ada/opt.adb