[Eva] rename debug key to "-loop-unroll" for better consistency

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

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

src/plugins/value/value_parameters.ml

@@ -90,8 +90,8 @@ 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"

src/plugins/value/value_parameters.mli

@@ -180,7 +180,7 @@ 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

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