diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-09 07:53:55 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-09 07:53:55 +0000 |
| commit | 5dd6327237996b7f4103e11c76aac01bf2420e19 (patch) | |
| tree | 75b40868a79ba88a16cdb312f380f4ee0d5f876d /gcc | |
| parent | a569f21920e9f53489a59be84c44d6345bbbfa6d (diff) | |
| download | gcc-5dd6327237996b7f4103e11c76aac01bf2420e19.zip gcc-5dd6327237996b7f4103e11c76aac01bf2420e19.tar.gz gcc-5dd6327237996b7f4103e11c76aac01bf2420e19.tar.bz2 | |
[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
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 7 | ||||
| -rw-r--r-- | gcc/ada/exp_util.adb | 12 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 8 |
3 files changed, 16 insertions, 11 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ed8dfda..8c07082 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2019-07-09 Yannick Moy <moy@adacore.com> + + * 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. + 2019-07-09 Piotr Trojanek <trojanek@adacore.com> * doc/gnat_rm/the_gnat_library.rst, diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 4206090..6f73ec3 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -5067,9 +5067,15 @@ package body Exp_Util is -- may be constants that depend on the bounds of a string literal, both -- standard string types and more generally arrays of characters. - -- In GNATprove mode, these extra subtypes are not needed - - if GNATprove_Mode then + -- In GNATprove mode, these extra subtypes are not needed, unless Exp is + -- a static expression. In that case, the subtype will be constrained + -- while the original type might be unconstrained, so expanding the type + -- is necessary both for passing legality checks in GNAT and for precise + -- analysis in GNATprove. + + if GNATprove_Mode + and then not Is_Static_Expression (Exp) + then return; end if; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index ec86266..38fab90 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -4592,14 +4592,6 @@ package body Sem_Ch3 is elsif Is_Interface (T) then null; - -- In GNATprove mode, Expand_Subtype_From_Expr does nothing. Thus, - -- we should prevent the generation of another Itype with the - -- same name as the one already generated, or we end up with - -- two identical types in GNATprove. - - elsif GNATprove_Mode then - null; - -- If the type is an unchecked union, no subtype can be built from -- the expression. Rewrite declaration as a renaming, which the -- back-end can handle properly. This is a rather unusual case, |