From 6e0ecbcc33bcacfd2e7711726e67def980e5b15a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 31 Aug 2021 17:19:47 +0200
Subject: [PATCH] [Eva] Renames message category "missing-loop-unroll" to
 "loop-unroll:missing".

---
 src/plugins/value/value_parameters.ml   | 4 ++--
 tests/misc/oracle/audit-out.json        | 4 ++--
 tests/value/loopfun.i                   | 2 +-
 tests/value/oracle/loopfun.1.res.oracle | 6 +++---
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 8f5c01931e9..541665b1fd3 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -102,9 +102,9 @@ let wkey_loop_unroll_auto = register_warn_category "loop-unroll:auto"
 let () = set_warn_status wkey_loop_unroll_auto Log.Wfeedback
 let wkey_loop_unroll_partial = register_warn_category "loop-unroll:partial"
 let () = set_warn_status wkey_loop_unroll_partial Log.Wfeedback
-let wkey_missing_loop_unroll = register_warn_category "missing-loop-unroll"
+let wkey_missing_loop_unroll = register_warn_category "loop-unroll:missing"
 let () = set_warn_status wkey_missing_loop_unroll Log.Winactive
-let wkey_missing_loop_unroll_for = register_warn_category "missing-loop-unroll:for"
+let wkey_missing_loop_unroll_for = register_warn_category "loop-unroll:missing:for"
 let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive
 let wkey_signed_overflow = register_warn_category "signed-overflow"
 let wkey_invalid_assigns = register_warn_category "invalid-assigns"
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 9b5a8483c1c..144491fa6a5 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -44,8 +44,8 @@
       ],
       "disabled": [
         "garbled-mix", "invalid-assigns", "loop-unroll:auto",
-        "loop-unroll:partial", "malloc:weak", "missing-loop-unroll",
-        "missing-loop-unroll:for"
+        "loop-unroll:missing", "loop-unroll:missing:for",
+        "loop-unroll:partial", "malloc:weak"
       ]
     }
   },
diff --git a/tests/value/loopfun.i b/tests/value/loopfun.i
index 2db5a9837a5..74d9162e27f 100644
--- a/tests/value/loopfun.i
+++ b/tests/value/loopfun.i
@@ -1,6 +1,6 @@
 /* run.config*
    STDOPT: +"-eva-slevel 50 -eva-no-results"
-   STDOPT: +"-eva-warn-key=missing-loop-unroll=feedback -eva-warn-key=missing-loop-unroll:for=active -main main2"
+   STDOPT: +"-eva-warn-key=loop-unroll:missing=feedback -eva-warn-key=loop-unroll:missing:for=active -main main2"
 */
 static int a = 7;
 
diff --git a/tests/value/oracle/loopfun.1.res.oracle b/tests/value/oracle/loopfun.1.res.oracle
index d6802166c97..27f3fd32103 100644
--- a/tests/value/oracle/loopfun.1.res.oracle
+++ b/tests/value/oracle/loopfun.1.res.oracle
@@ -5,11 +5,11 @@
 [eva:initial-state] Values of globals at initialization
   v ∈ [--..--]
   a ∈ {7}
-[eva:missing-loop-unroll] tests/value/loopfun.i:23: 
+[eva:loop-unroll:missing] tests/value/loopfun.i:23: 
   while loop without unroll annotation
-[eva:missing-loop-unroll:for] tests/value/loopfun.i:26: Warning: 
+[eva:loop-unroll:missing:for] tests/value/loopfun.i:26: Warning: 
   for loop without unroll annotation
-[eva:missing-loop-unroll] tests/value/loopfun.i:27: 
+[eva:loop-unroll:missing] tests/value/loopfun.i:27: 
   dowhile loop without unroll annotation
 [eva] Recording results for main2
 [eva] done for function main2
-- 
GitLab