diff --git a/doc/value/main.tex b/doc/value/main.tex
index 2d5124ad23a4639fa25509a1de053eaf6842253f..15d5553fb0a48ebc63c5c0bc8f0ab51525505895 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3289,7 +3289,7 @@ remaining \lstinline|-eva-slevel| may be used to unroll more iterations.
 
 While it is sometimes useful to unroll only the first iterations, the usual
 objective is full unrolling; the user can enable option
-\lstinline|-value-msg-key=loop-unrolling| to be informed whenever the specified
+\lstinline|-value-msg-key=loop-unroll| to be informed whenever the specified
 unrolling value is insufficient to unroll the loop entirely:
 
 \begin{lstlisting}
@@ -3301,7 +3301,7 @@ void main() {
 \end{lstlisting}
 
 \begin{lstlisting}
-[eva:loop-unrolling] insuf-loop.c:3: loop not completely unrolled
+[eva:loop-unroll] insuf-loop.c:3: loop not completely unrolled
 \end{lstlisting}
 
 Note that using an unrolling parameter which is higher than the actual number
diff --git a/src/plugins/value/engine/loop_partitioning.ml b/src/plugins/value/engine/loop_partitioning.ml
index a6700d0c89021b88247c4f6f692926140260bc04..de4edd65e01a5886c59dd05a23eb0c21d052a66c 100644
--- a/src/plugins/value/engine/loop_partitioning.ml
+++ b/src/plugins/value/engine/loop_partitioning.ml
@@ -522,7 +522,7 @@ struct
               let merge t1 t2 =
                 if not (is_empty_propagation_tree t2) then
                   Value_parameters.warning ~once:true ~current:true
-                    ~wkey:Value_parameters.wkey_loop_unrolling
+                    ~wkey:Value_parameters.wkey_loop_unroll
                     "loop not completely unrolled";
                 join_propagation_tree t1 t2
               in
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index aa0be86c0bb64f3d80441a05509ce8adab7a4037..0fefd04e9a5548e9389a44c2e923766e4395cf23 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -110,7 +110,22 @@ module Make_Dataflow
 
   let unroll (stmt : stmt) : int =
     let local_unroll = match Unroll_annots.get_unroll_terms stmt with
-      | [] -> None
+      | [] ->
+        let is_attribute a = Cil.hasAttribute a stmt.sattr in
+        begin
+          match List.filter is_attribute ["for" ; "while" ; "dowhile"] with
+          | [] -> ()
+          | loop_kind :: _ ->
+            let wkey =
+              if loop_kind = "for"
+              then Value_parameters.wkey_missing_loop_unroll_for
+              else Value_parameters.wkey_missing_loop_unroll
+            in
+            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..554a0c1a5b3093548f03648311874936f6811752 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -90,8 +90,12 @@ let () = set_warn_status wkey_garbled_mix Log.Winactive
 let wkey_builtins_missing_spec = register_warn_category "builtins:missing-spec"
 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_loop_unroll = register_warn_category "loop-unroll"
+let () = set_warn_status wkey_loop_unroll 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..2c3562255f595909a2771e52b17d659db69db1c3 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -180,7 +180,13 @@ val wkey_builtins_override: warn_category
 val wkey_libc_unsupported_spec : warn_category
 
 (** Warning category used for "loop not completely unrolled" *)
-val wkey_loop_unrolling : warn_category
+val wkey_loop_unroll : 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/misc/oracle/unroll_annots.res.oracle b/tests/misc/oracle/unroll_annots.res.oracle
index 4c2129811bc179866cef585c0a1b34d1807ed194..0e37020e66540945660669098c29d1b237ecbb20 100644
--- a/tests/misc/oracle/unroll_annots.res.oracle
+++ b/tests/misc/oracle/unroll_annots.res.oracle
@@ -5,9 +5,9 @@
 [eva:initial-state] Values of globals at initialization
   a[0..9] ∈ {0}
   b[0..9] ∈ {0}
-[eva:loop-unrolling] tests/misc/unroll_annots.c:8: loop not completely unrolled
+[eva:loop-unroll] tests/misc/unroll_annots.c:8: loop not completely unrolled
 [eva] tests/misc/unroll_annots.c:8: starting to merge loop iterations
-[eva:loop-unrolling] tests/misc/unroll_annots.c:14: loop not completely unrolled
+[eva:loop-unroll] tests/misc/unroll_annots.c:14: loop not completely unrolled
 [eva] tests/misc/unroll_annots.c:14: starting to merge loop iterations
 [eva] tests/misc/unroll_annots.c:16: starting to merge loop iterations
 [eva] Recording results for main
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