diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index 8f5c01931e95ef38f95dcb13c2f74257ed6124f2..541665b1fd31aa9c5f7ed058c5e250985d19a737 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 9b5a8483c1c1b4ac789b73542c165e71bfd37a65..144491fa6a5834a1f5605477986cab4a7ad975b6 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 2db5a9837a566a70e3ab9b52f690bedb21f26e14..74d9162e27fbb18fbbd95f7f94a3322bb77ed002 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 d6802166c97a9854d3af41680bfd20dcf57d94fe..27f3fd32103e401203e9400d3434efcc110bd788 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