From bfd7425d993ad711e9fc86460cdfa239379ef5a5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 15 Apr 2019 14:58:08 +0200
Subject: [PATCH] [Eva] Restores the feedback when a loop is not completely
unrolled.
---
src/plugins/value/engine/partition.ml | 7 ++++++-
tests/value/oracle/partitioning-annots.0.res.oracle | 6 ++++++
2 files changed, 12 insertions(+), 1 deletion(-)
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index 8c690af3db9..fcf0088095c 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -418,8 +418,13 @@ struct
begin match k.loops with
| [] -> raise InvalidAction
| (h, limit) :: tl ->
- if h >= limit then
+ if h >= limit then begin
+ if limit > 0 then
+ Value_parameters.warning ~once:true ~current:true
+ ~wkey:Value_parameters.wkey_loop_unroll
+ "loop not completely unrolled";
k
+ end
else
{ k with loops = (h + 1, limit) :: tl }
end
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index a94f8e71bdc..49addb21756 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -4,9 +4,15 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
+[eva:loop-unroll] tests/value/partitioning-annots.c:26:
+ loop not completely unrolled
[eva] tests/value/partitioning-annots.c:26: starting to merge loop iterations
+[eva:loop-unroll] tests/value/partitioning-annots.c:34:
+ loop not completely unrolled
[eva] tests/value/partitioning-annots.c:34: starting to merge loop iterations
[eva] tests/value/partitioning-annots.c:36: starting to merge loop iterations
+[eva:loop-unroll] tests/value/partitioning-annots.c:50:
+ loop not completely unrolled
[eva] tests/value/partitioning-annots.c:50: starting to merge loop iterations
[eva] Recording results for test_unroll
[eva] done for function test_unroll
--
GitLab