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/value_parameters.ml b/src/plugins/value/value_parameters.ml index 1b3c2394532c85b589273531c5d0f10e827adabc..554a0c1a5b3093548f03648311874936f6811752 100644 --- a/src/plugins/value/value_parameters.ml +++ b/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" diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli index fe93680004168418a7ae3433cf17d6ce6a33cf6d..2c3562255f595909a2771e52b17d659db69db1c3 100644 --- a/src/plugins/value/value_parameters.mli +++ b/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 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