diff mbox

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

Message ID 20140224150950.GA1348@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Feb. 24, 2014, 3:09 p.m. UTC 
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  <kanig@adacore.com>

	* exp_util.adb (Expand_Subtype_From_Expr): Do not expand subtypes in
	GNATprove_mode, gnat2why doesn't need nor use these types.
diff mbox

Patch

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;