[Eva] Restores the feedback when a loop is not completely unrolled.

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

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