diff options
| -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, |