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

Submitted by Arnaud Charlet on Aug. 29, 2011, 8:22 a.m.

Details

Message ID 20110829082215.GA14609@adacore.com
State New
Headers show

Commit Message

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 hide | download patch | download mbox

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