[Ada] Expand type of static expressions in GNATprove mode
authorYannick Moy <moy@adacore.com>
Tue, 9 Jul 2019 07:53:55 +0000 (07:53 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 9 Jul 2019 07:53:55 +0000 (07:53 +0000)
commit5dd6327237996b7f4103e11c76aac01bf2420e19
tree75b40868a79ba88a16cdb312f380f4ee0d5f876d
parenta569f21920e9f53489a59be84c44d6345bbbfa6d
[Ada] Expand type of static expressions in GNATprove mode

In the special mode for GNATprove, expand the type of static expressions
like done during compilation, to both get suitable legality checks and
increase the precision of the formal analysis.

There is no impact on compilation.

2019-07-09  Yannick Moy  <moy@adacore.com>

gcc/ada/

* exp_util.adb (Expand_Subtype_From_Expr): Still expand the type
of static expressions in GNATprove_Mode.
* sem_ch3.adb (Analyze_Object_Declaration): Remove obsolete
special case for GNATprove_Mode.

From-SVN: r273273
gcc/ada/ChangeLog
gcc/ada/exp_util.adb
gcc/ada/sem_ch3.adb