[Ada] Do not expand dynamic subtypes for expressions in GNATprove_mode

[Arnaud Charlet]

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;