From 252d4872810084c8edf9a212fcada43a64895926 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 3 Jan 2019 18:30:40 +0100
Subject: [PATCH] [Eva] rename debug key to "-loop-unroll" for better
 consistency

---
 doc/value/main.tex                            | 4 ++--
 src/plugins/value/engine/loop_partitioning.ml | 2 +-
 src/plugins/value/value_parameters.ml         | 4 ++--
 src/plugins/value/value_parameters.mli        | 2 +-
 tests/misc/oracle/unroll_annots.res.oracle    | 4 ++--
 5 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/doc/value/main.tex b/doc/value/main.tex
index 2d5124ad23a..15d5553fb0a 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 a6700d0c890..de4edd65e01 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 1b3c2394532..554a0c1a5b3 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 fe936800041..2c3562255f5 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 4c2129811bc..0e37020e665 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
-- 
GitLab