@@ -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;
@@ -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,