From 3751a20df2bb2c60158f7d6a60c82e92ee1d50cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 18 Jun 2020 11:29:59 +0200
Subject: [PATCH] [Eva] The automatic loop unrolling finds loop exit conditions
in blocks.
---
src/plugins/value/partitioning/auto_loop_unroll.ml | 1 +
tests/value/oracle/auto_loop_unroll.1.res.oracle | 7 ++-----
2 files changed, 3 insertions(+), 5 deletions(-)
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index 9cb77831f79..c012563e68e 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -72,6 +72,7 @@ let find_loop_exit_condition loop =
if is_break b1
then (cond, true) :: aux (b2.bstmts @ tl)
else (cond, false) :: aux (b1.bstmts @ tl)
+ | Block b -> aux (b.bstmts @ tl)
| _ -> aux tl
in
aux loop.bstmts
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index a1ed5bef663..9b5007dda77 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -349,11 +349,8 @@
[eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_0_13: [0..13]
[eva:loop-unroll] tests/value/auto_loop_unroll.c:208: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:211: Frama_C_show_each_0_14: [0..14]
-[eva] tests/value/auto_loop_unroll.c:214: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:217: Warning:
- signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:219:
- Frama_C_show_each_0_15: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:214: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_0_15: [0..15]
[eva:loop-unroll] tests/value/auto_loop_unroll.c:221: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:221:
Trace partitioning superposing up to 100 states
--
GitLab