diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index aa0be86c0bb64f3d80441a05509ce8adab7a4037..34b0444509ec51b8be814ba930caf101aba28cd9 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -110,7 +110,25 @@ module Make_Dataflow
let unroll (stmt : stmt) : int =
let local_unroll = match Unroll_annots.get_unroll_terms stmt with
- | [] -> None
+ | [] ->
+ let loop_attr_and_wkey =
+ if Cil.hasAttribute "for" stmt.sattr then
+ Some ("for", Value_parameters.wkey_missing_loop_unroll_for)
+ else if Cil.hasAttribute "while" stmt.sattr then
+ Some ("while", Value_parameters.wkey_missing_loop_unroll)
+ else if Cil.hasAttribute "dowhile" stmt.sattr then
+ Some ("dowhile", Value_parameters.wkey_missing_loop_unroll)
+ else None
+ in
+ begin
+ match loop_attr_and_wkey with
+ | None -> ()
+ | Some (loop_kind, wkey) ->
+ Value_parameters.warning
+ ~wkey ~source:(fst (Cil_datatype.Stmt.loc stmt)) ~once:true
+ "%s loop without unroll annotation" loop_kind
+ end;
+ None
| [t] ->
(* Inlines the value of const variables in [t]. *)
let global_init vi =
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 5e3234f75f8b2094bf7900a1f20b1b64516d4849..1b3c2394532c85b589273531c5d0f10e827adabc 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -92,6 +92,10 @@ let wkey_builtins_override = register_warn_category "builtins:override"
let wkey_libc_unsupported_spec = register_warn_category "libc:unsupported-spec"
let wkey_loop_unrolling = register_warn_category "loop-unrolling"
let () = set_warn_status wkey_loop_unrolling Log.Wfeedback
+let wkey_missing_loop_unroll = register_warn_category "missing-loop-unroll"
+let () = set_warn_status wkey_missing_loop_unroll Log.Winactive
+let wkey_missing_loop_unroll_for = register_warn_category "missing-loop-unroll:for"
+let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive
module ForceValues =
WithOutput
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 65bf98a6d20653d1cb99aeba7e07282495bbbe1f..fe93680004168418a7ae3433cf17d6ce6a33cf6d 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -182,6 +182,12 @@ val wkey_libc_unsupported_spec : warn_category
(** Warning category used for "loop not completely unrolled" *)
val wkey_loop_unrolling : warn_category
+(** Warning category used to identify loops without unroll annotations *)
+val wkey_missing_loop_unroll : warn_category
+
+(** Warning category used to identify for loops without unroll annotations *)
+val wkey_missing_loop_unroll_for : warn_category
+
(** Debug category used to print information about invalid pointer comparisons*)
val dkey_pointer_comparison: category
diff --git a/tests/value/loopfun.i b/tests/value/loopfun.i
index afca12398b58e22ba8f07032f43d5496f389a541..030e2654b43ef017571f659a983d660c59ed3315 100644
--- a/tests/value/loopfun.i
+++ b/tests/value/loopfun.i
@@ -1,7 +1,7 @@
/* run.config*
STDOPT: +"-slevel 50 -no-results"
+ STDOPT: +"-eva-warn-key=missing-loop-unroll=feedback -eva-warn-key=missing-loop-unroll:for=active -main main2"
*/
-
static int a = 7;
int test()
@@ -17,3 +17,12 @@ int main()
}
return 0;
}
+
+volatile int v;
+void main2() {
+ while (v) {}
+ //@ loop unroll 1;
+ for(;v;);
+ for(;v;);
+ do {} while(v);
+}
diff --git a/tests/value/oracle/loopfun.res.oracle b/tests/value/oracle/loopfun.0.res.oracle
similarity index 91%
rename from tests/value/oracle/loopfun.res.oracle
rename to tests/value/oracle/loopfun.0.res.oracle
index 949c06bca9bffff7b2f504eeba7c281521451645..0bdd232311e43a73cfd47f9f9c9c32418786bada 100644
--- a/tests/value/oracle/loopfun.res.oracle
+++ b/tests/value/oracle/loopfun.0.res.oracle
@@ -3,6 +3,7 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
a ∈ {7}
[eva] computing for function test <- main.
Called from tests/value/loopfun.i:14.
@@ -41,12 +42,16 @@
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[from] Computing for function main2
+[from] Done for function main2
[from] Computing for function test
[from] Done for function test
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function main2:
+ FROMTOP
[from] Function test:
FROMTOP
\result FROM ANYTHING(origin:Unknown)
@@ -54,6 +59,10 @@
FROMTOP
\result FROM ANYTHING(origin:Unknown)
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main2:
+ \nothing
+[inout] Inputs for function main2:
+ v
[inout] Out (internal) for function test:
tmp; a
[inout] Inputs for function test:
diff --git a/tests/value/oracle/loopfun.1.res.oracle b/tests/value/oracle/loopfun.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d6802166c97a9854d3af41680bfd20dcf57d94fe
--- /dev/null
+++ b/tests/value/oracle/loopfun.1.res.oracle
@@ -0,0 +1,29 @@
+[kernel] Parsing tests/value/loopfun.i (no preprocessing)
+[eva] Analyzing a complete application starting at main2
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
+ a ∈ {7}
+[eva:missing-loop-unroll] tests/value/loopfun.i:23:
+ while loop without unroll annotation
+[eva:missing-loop-unroll:for] tests/value/loopfun.i:26: Warning:
+ for loop without unroll annotation
+[eva:missing-loop-unroll] tests/value/loopfun.i:27:
+ dowhile loop without unroll annotation
+[eva] Recording results for main2
+[eva] done for function main2
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main2:
+
+[from] Computing for function main2
+[from] Done for function main2
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function main2:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main2:
+ \nothing
+[inout] Inputs for function main2:
+ v