Patchwork [Ada] Prevent expansion of array aggregates in formal verification mode

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 29, 2011, 8:22 a.m.
Message ID <20110829082215.GA14609@adacore.com>
Download mbox | patch
Permalink /patch/111972/
State New
Headers show

Comments

Arnaud Charlet - Aug. 29, 2011, 8:22 a.m.
The backend for formal verification handles much more easily aggregates that
are not expanded into loops, as this happens with array aggregates, so prevent
expansion in this mode.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-29  Yannick Moy  <moy@adacore.com>

	* exp_aggr.adb (Expand_Array_Aggregate): Do not expand array aggregates
	in formal verification.

Patch

Index: exp_aggr.adb
===================================================================
--- exp_aggr.adb	(revision 178155)
+++ exp_aggr.adb	(working copy)
@@ -4664,6 +4664,12 @@ 
          Check_Same_Aggr_Bounds (N, 1);
       end if;
 
+      --  In formal verification mode, leave the aggregate non-expanded
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  STEP 2
 
       --  Here we test for is packed array aggregate that we can handle at