During expansion, extra subtypes are generated for many expressions.
This is in fact not needed and even harmful for the formal verification
mode controlled by GNATprove_mode. This subtype expansion is now
disabled in GNATprove_mode.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-24 Johannes Kanig <ka...@adacore.com>
* exp_util.adb (Expand_Subtype_From_Expr): Do not expand subtypes in
GNATprove_mode, gnat2why doesn't need nor use these types.
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 208067)
+++ exp_util.adb (working copy)
@@ -2074,19 +2074,15 @@
-- 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, we also need the more precise subtype to be set
+ -- In GNATprove mode, these extra subtypes are not needed
- if not (Expander_Active or GNATprove_Mode)
- and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
- then
+ if GNATprove_Mode then
return;
end if;
- -- In GNATprove mode, Unc_Type might not be complete when analyzing
- -- a generic unit. As generic units are not analyzed directly in
- -- GNATprove, return here rather than failing later.
-
- if GNATprove_Mode and then No (Underlying_Type (Unc_Type)) then
+ if not Expander_Active
+ and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
+ then
return;
end if;
