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 <m...@adacore.com>
* exp_aggr.adb (Expand_Array_Aggregate): Do not expand array aggregates
in formal verification.
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
