diff --git a/regression/cbmc-concurrency/constant_prop1/test.desc b/regression/cbmc-concurrency/constant_prop1/test.desc index 201dc9bdb6e..199f4385d83 100644 --- a/regression/cbmc-concurrency/constant_prop1/test.desc +++ b/regression/cbmc-concurrency/constant_prop1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/alarm1/test.desc b/regression/cbmc-incr-oneloop/alarm1/test.desc index b0164719dbb..bab44d71da8 100644 --- a/regression/cbmc-incr-oneloop/alarm1/test.desc +++ b/regression/cbmc-incr-oneloop/alarm1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-standard-checks --incremental-loop main.0 --unwind-max 15 +--no-standard-checks --incremental-loop main.0 --unwind-max 15 --verbosity 8 activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc b/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc index 904c5d51283..bbc27aea611 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-loop main.0 --unwind-min 5 --unwind-max 10 --json-ui +--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --json-ui --verbosity 8 ^EXIT=10$ ^SIGNAL=0$ "messageText": "VERIFICATION FAILED" diff --git a/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc b/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc index c967c1fb2db..1a909c2f305 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-loop main.0 --unwind-min 5 --unwind-max 10 --xml-ui +--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --xml-ui --verbosity 8 ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED diff --git a/regression/cbmc-incr-oneloop/alarm2/test.desc b/regression/cbmc-incr-oneloop/alarm2/test.desc index e36848a5583..cb52dbde9b5 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-loop main.0 --unwind-min 5 --unwind-max 10 +--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --verbosity 8 activate-multi-line-match Current unwinding: 1 Incremental status: INCONCLUSIVE diff --git a/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc index a6f44007b7e..8e71df0770c 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-standard-checks --unwind-min 6 --unwind-max 8 --incremental-loop main.0 --ignore-properties-before-unwind-min +--no-standard-checks --unwind-min 6 --unwind-max 8 --incremental-loop main.0 --ignore-properties-before-unwind-min --verbosity 8 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc index a3e2750d320..cdfc337c069 100644 --- a/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc @@ -1,6 +1,6 @@ CORE test.c ---no-standard-checks --incremental-loop main.0 --no-propagation +--no-standard-checks --incremental-loop main.0 --no-propagation --verbosity 8 activate-multi-line-match Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc index 11e06f6d641..c4f2f530a5f 100644 --- a/regression/cbmc-incr-oneloop/multiple-asserts/test.desc +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc @@ -1,6 +1,6 @@ CORE test.c ---incremental-loop main.0 +--incremental-loop main.0 --verbosity 8 activate-multi-line-match Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 diff --git a/regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc b/regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc index aec15571868..d8e96ef137c 100644 --- a/regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc +++ b/regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-standard-checks --incremental-loop main.1 --unwind 2 +--no-standard-checks --incremental-loop main.1 --unwind 2 --verbosity 8 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc b/regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc index 26902aa1c10..bc35b96607c 100644 --- a/regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc +++ b/regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-standard-checks --incremental-loop main.3 --unwindset main.1:2,main.2:8 +--no-standard-checks --incremental-loop main.3 --unwindset main.1:2,main.2:8 --verbosity 8 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/valid-asserts/test.desc b/regression/cbmc-incr-oneloop/valid-asserts/test.desc index 36ddf206c3a..9c92daf149b 100644 --- a/regression/cbmc-incr-oneloop/valid-asserts/test.desc +++ b/regression/cbmc-incr-oneloop/valid-asserts/test.desc @@ -1,6 +1,6 @@ CORE test.c ---incremental-loop main.0 +--incremental-loop main.0 --verbosity 8 activate-multi-line-match Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 Incremental status: INCONCLUSIVE\nCurrent unwinding: 10 diff --git a/regression/cbmc-library/memcpy-01/constant-propagation.desc b/regression/cbmc-library/memcpy-01/constant-propagation.desc index ff632e2c948..9762ce62b88 100644 --- a/regression/cbmc-library/memcpy-01/constant-propagation.desc +++ b/regression/cbmc-library/memcpy-01/constant-propagation.desc @@ -1,6 +1,6 @@ CORE main.c ---no-standard-checks +--no-standard-checks --verbosity 8 ^Generated 1\d* VCC\(s\), 0 remaining after simplification$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/memmove-01/constant.desc b/regression/cbmc-library/memmove-01/constant.desc index 4ee247447a3..34cbd42b8c2 100644 --- a/regression/cbmc-library/memmove-01/constant.desc +++ b/regression/cbmc-library/memmove-01/constant.desc @@ -1,6 +1,6 @@ CORE constant.c ---no-standard-checks --unwind 17 +--no-standard-checks --unwind 17 --verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-shadow-memory/constchar-param1/test.desc b/regression/cbmc-shadow-memory/constchar-param1/test.desc index a654f77e6d1..442a0d46c5c 100644 --- a/regression/cbmc-shadow-memory/constchar-param1/test.desc +++ b/regression/cbmc-shadow-memory/constchar-param1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 11 +--unwind 11 --verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-with-incr/Fixedbv4/test.desc b/regression/cbmc-with-incr/Fixedbv4/test.desc index dcd58b05b14..9eb49c77aa0 100644 --- a/regression/cbmc-with-incr/Fixedbv4/test.desc +++ b/regression/cbmc-with-incr/Fixedbv4/test.desc @@ -1,6 +1,6 @@ FUTURE main.c ---fixedbv +--fixedbv --verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Array_Propagation1/test.desc b/regression/cbmc/Array_Propagation1/test.desc index c7996d86f9f..a06e6301f9f 100644 --- a/regression/cbmc/Array_Propagation1/test.desc +++ b/regression/cbmc/Array_Propagation1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/BV_Arithmetic3/test.desc b/regression/cbmc/BV_Arithmetic3/test.desc index 9c7dfb426dd..1d107739188 100644 --- a/regression/cbmc/BV_Arithmetic3/test.desc +++ b/regression/cbmc/BV_Arithmetic3/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--verbosity 8 ^EXIT=0$ ^SIGNAL=0$ (Starting CEGAR Loop|^Generated 68 VCC\(s\), 0 remaining after simplification$) diff --git a/regression/cbmc/Bool/bool5-full-slice.desc b/regression/cbmc/Bool/bool5-full-slice.desc index cff6a9ffa72..48f1ccfca1c 100644 --- a/regression/cbmc/Bool/bool5-full-slice.desc +++ b/regression/cbmc/Bool/bool5-full-slice.desc @@ -1,6 +1,6 @@ CORE bool5.c ---full-slice +--full-slice --verbosity 8 Generated 10 VCC\(s\), 0 remaining after simplification ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/Bool/bool5.desc b/regression/cbmc/Bool/bool5.desc index a27559ad37a..d08b348f789 100644 --- a/regression/cbmc/Bool/bool5.desc +++ b/regression/cbmc/Bool/bool5.desc @@ -1,6 +1,6 @@ CORE bool5.c - +--verbosity 8 Generated 10 VCC\(s\), 0 remaining after simplification ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/Fixedbv4/test.desc b/regression/cbmc/Fixedbv4/test.desc index 65535fe6331..c84068a008d 100644 --- a/regression/cbmc/Fixedbv4/test.desc +++ b/regression/cbmc/Fixedbv4/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--unwind 8 --verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Float-equality2/test.desc b/regression/cbmc/Float-equality2/test.desc index 17fba7951a0..61073ec9c9e 100644 --- a/regression/cbmc/Float-equality2/test.desc +++ b/regression/cbmc/Float-equality2/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--verbosity 8 (Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$) ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/Pointer_comparison5/test.desc b/regression/cbmc/Pointer_comparison5/test.desc index fe094259f78..d1e040b0f6b 100644 --- a/regression/cbmc/Pointer_comparison5/test.desc +++ b/regression/cbmc/Pointer_comparison5/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--verbosity 8 ^Generated \d+ VCC\(s\), 1 remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/Struct_Propagation1/test.desc b/regression/cbmc/Struct_Propagation1/test.desc index 42e6505e2d3..763e1fda23d 100644 --- a/regression/cbmc/Struct_Propagation1/test.desc +++ b/regression/cbmc/Struct_Propagation1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 5 +--unwind 5 --verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/bounds_check2/test.desc b/regression/cbmc/bounds_check2/test.desc index 86b25cb3b31..70dbf32237a 100644 --- a/regression/cbmc/bounds_check2/test.desc +++ b/regression/cbmc/bounds_check2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---retain-trivial-checks +--retain-trivial-checks --verbosity 8 ^Generated \d+ VCC\(s\), 0 remaining after simplification$ ^\[main.array_bounds.1\] line 4 array 'A' (lower|upper) bound in A\[(\(signed (long (long )?)?int\))?1\]: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/condition-propagation-1/test.desc b/regression/cbmc/condition-propagation-1/test.desc index cc3baab01eb..439f6867798 100644 --- a/regression/cbmc/condition-propagation-1/test.desc +++ b/regression/cbmc/condition-propagation-1/test.desc @@ -1,6 +1,6 @@ CORE test.c - +--verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/condition-propagation-2/test.desc b/regression/cbmc/condition-propagation-2/test.desc index cc3baab01eb..439f6867798 100644 --- a/regression/cbmc/condition-propagation-2/test.desc +++ b/regression/cbmc/condition-propagation-2/test.desc @@ -1,6 +1,6 @@ CORE test.c - +--verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/condition-propagation-3/test.desc b/regression/cbmc/condition-propagation-3/test.desc index cc3baab01eb..439f6867798 100644 --- a/regression/cbmc/condition-propagation-3/test.desc +++ b/regression/cbmc/condition-propagation-3/test.desc @@ -1,6 +1,6 @@ CORE test.c - +--verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/condition-propagation-4/test.desc b/regression/cbmc/condition-propagation-4/test.desc index cc3baab01eb..439f6867798 100644 --- a/regression/cbmc/condition-propagation-4/test.desc +++ b/regression/cbmc/condition-propagation-4/test.desc @@ -1,6 +1,6 @@ CORE test.c - +--verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/constant_folding3/test.desc b/regression/cbmc/constant_folding3/test.desc index 85f89ddbb1a..a44f7cb56a9 100644 --- a/regression/cbmc/constant_folding3/test.desc +++ b/regression/cbmc/constant_folding3/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--verbosity 8 ^Generated 1 VCC\(s\), 0 remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/field-sensitivity14/test.desc b/regression/cbmc/field-sensitivity14/test.desc index 1661a8e4505..f7ced0523ed 100644 --- a/regression/cbmc/field-sensitivity14/test.desc +++ b/regression/cbmc/field-sensitivity14/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c - +--verbosity 8 ^Generated \d+ VCC\(s\), \d remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/gcc_builtin_sub_overflow/simplify.desc b/regression/cbmc/gcc_builtin_sub_overflow/simplify.desc index 554a1ff19cd..275435ccdd1 100644 --- a/regression/cbmc/gcc_builtin_sub_overflow/simplify.desc +++ b/regression/cbmc/gcc_builtin_sub_overflow/simplify.desc @@ -1,6 +1,6 @@ CORE simplify.c - +--verbosity 8 ^Generated 2 VCC\(s\), 0 remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/json-interface1/test.desc b/regression/cbmc/json-interface1/test.desc index 083df61a021..3178df58264 100644 --- a/regression/cbmc/json-interface1/test.desc +++ b/regression/cbmc/json-interface1/test.desc @@ -1,6 +1,6 @@ CORE --json-interface -< test.json +--verbosity 8 < test.json activate-multi-line-match ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/no-propagation/test.desc b/regression/cbmc/no-propagation/test.desc index abf436bb9e3..4273c33d9a9 100644 --- a/regression/cbmc/no-propagation/test.desc +++ b/regression/cbmc/no-propagation/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-propagation +--no-propagation --verbosity 8 Generated 1 VCC\(s\), 1 remaining after simplification ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/null8/test.desc b/regression/cbmc/null8/test.desc index f2bcf68da06..793bc205451 100644 --- a/regression/cbmc/null8/test.desc +++ b/regression/cbmc/null8/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--verbosity 8 Generated 1 VCC\(s\), 0 remaining after simplification ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/runtime-profiling/test.desc b/regression/cbmc/runtime-profiling/test.desc index a6a504aa5b0..24159500111 100644 --- a/regression/cbmc/runtime-profiling/test.desc +++ b/regression/cbmc/runtime-profiling/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-standard-checks +--no-standard-checks --verbosity 8 ^EXIT=0$ ^SIGNAL=0$ ^Runtime Symex:.*$ diff --git a/regression/cbmc/self_loops_to_assumptions1/default.desc b/regression/cbmc/self_loops_to_assumptions1/default.desc index 5cec41df787..07aeb94d223 100644 --- a/regression/cbmc/self_loops_to_assumptions1/default.desc +++ b/regression/cbmc/self_loops_to_assumptions1/default.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 1 --unwinding-assertions +--unwind 1 --unwinding-assertions --verbosity 8 ^replacing self-loop at file main.c line 3 function main by assume\(FALSE\)$ ^no unwinding assertion will be generated for self-loop at file main.c line 3 function main$ ^EXIT=0$ diff --git a/regression/cbmc/simplify-union/test.desc b/regression/cbmc/simplify-union/test.desc index b9fde5dbf30..45562922248 100644 --- a/regression/cbmc/simplify-union/test.desc +++ b/regression/cbmc/simplify-union/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-malloc-may-fail +--no-malloc-may-fail --verbosity 8 ^Generated 13 VCC\(s\), 0 remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/union13/no-arch.desc b/regression/cbmc/union13/no-arch.desc index b43b43ef367..2484362f62a 100644 --- a/regression/cbmc/union13/no-arch.desc +++ b/regression/cbmc/union13/no-arch.desc @@ -1,6 +1,6 @@ CORE main.c ---arch none --little-endian +--arch none --little-endian --verbosity 8 (Starting CEGAR Loop|^Generated 1 VCC\(s\), 1 remaining after simplification$) ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/union18/test.desc b/regression/cbmc/union18/test.desc index e61cb7256ba..5ffd9b01340 100644 --- a/regression/cbmc/union18/test.desc +++ b/regression/cbmc/union18/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--verbosity 8 ^Generated 1 VCC\(s\), 0 remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/unreachable-goto1/test-vccs.desc b/regression/cbmc/unreachable-goto1/test-vccs.desc index 9091c97751a..e5193c7e9ed 100644 --- a/regression/cbmc/unreachable-goto1/test-vccs.desc +++ b/regression/cbmc/unreachable-goto1/test-vccs.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure test.c ---show-vcc +--show-vcc --verbosity 8 ^Generated 1 VCC\(s\), 1 remaining after simplification$ ^\{1\} false$ ^EXIT=0$ diff --git a/regression/cbmc/unreachable-goto2/test-vccs.desc b/regression/cbmc/unreachable-goto2/test-vccs.desc index d18e596fd5f..75a82c3b065 100644 --- a/regression/cbmc/unreachable-goto2/test-vccs.desc +++ b/regression/cbmc/unreachable-goto2/test-vccs.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure test.c ---show-vcc +--show-vcc --verbosity 8 ^Generated 1 VCC\(s\), 1 remaining after simplification$ ^\{1\} goto_symex::\\guard#1$ ^EXIT=0$ diff --git a/regression/cbmc/unreachable-goto3/test-vccs.desc b/regression/cbmc/unreachable-goto3/test-vccs.desc index 54f5a88444d..33384b61f19 100644 --- a/regression/cbmc/unreachable-goto3/test-vccs.desc +++ b/regression/cbmc/unreachable-goto3/test-vccs.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure test.c ---show-vcc +--show-vcc --verbosity 8 ^Generated 1 VCC\(s\), 1 remaining after simplification$ ^\{1\} false$ ^EXIT=0$ diff --git a/regression/cbmc/unreachable-goto4/test-vccs.desc b/regression/cbmc/unreachable-goto4/test-vccs.desc index 434b0b05cd0..feabf37efae 100644 --- a/regression/cbmc/unreachable-goto4/test-vccs.desc +++ b/regression/cbmc/unreachable-goto4/test-vccs.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure test.c ---show-vcc +--show-vcc --verbosity 8 ^Generated 1 VCC\(s\), 1 remaining after simplification$ ^\{1\} false$ ^EXIT=0$ diff --git a/regression/cbmc/unreachable-goto5/test-vccs.desc b/regression/cbmc/unreachable-goto5/test-vccs.desc index dc7ef0de936..f69439b6bb5 100644 --- a/regression/cbmc/unreachable-goto5/test-vccs.desc +++ b/regression/cbmc/unreachable-goto5/test-vccs.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure test.c ---show-vcc +--show-vcc --verbosity 8 ^Generated 1 VCC\(s\), 1 remaining after simplification$ ^\{1\} false$ ^EXIT=0$ diff --git a/regression/cbmc/unreachable-goto6/test-vccs.desc b/regression/cbmc/unreachable-goto6/test-vccs.desc index dcfb2c2a5e3..93f88787edb 100644 --- a/regression/cbmc/unreachable-goto6/test-vccs.desc +++ b/regression/cbmc/unreachable-goto6/test-vccs.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure test.c ---show-vcc +--show-vcc --verbosity 8 ^Generated 1 VCC\(s\), 1 remaining after simplification$ ^\{1\} false$ ^EXIT=0$ diff --git a/regression/cbmc/xml-interface1/test.desc b/regression/cbmc/xml-interface1/test.desc index 7f33c189af2..c4a5b2532ee 100644 --- a/regression/cbmc/xml-interface1/test.desc +++ b/regression/cbmc/xml-interface1/test.desc @@ -1,6 +1,6 @@ CORE --xml-interface -< test.xml +--verbosity 8 < test.xml ^EXIT=10$ ^SIGNAL=0$ Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0 diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc index 20b56e58877..3fbc7b5739f 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-goto-functions --pointer-check +--show-goto-functions --pointer-check --verbosity 8 ^Removal of function pointers and virtual functions$ ^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ ^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc index ef4794c6913..beb6b575dfd 100644 --- a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-goto-functions --pointer-check +--show-goto-functions --pointer-check --verbosity 8 ^Removal of function pointers and virtual functions$ ^\s*ASSERT false // no candidates for dereferenced function pointer ^EXIT=0$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc index 027977038b9..a773197ea62 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-goto-functions --pointer-check +--show-goto-functions --pointer-check --verbosity 8 ^Removal of function pointers and virtual functions$ ^\s*ASSERT false // no candidates for dereferenced function pointer ^EXIT=0$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc index a376a6fb940..084ead835ed 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-goto-functions --pointer-check +--show-goto-functions --pointer-check --verbosity 8 ^Removal of function pointers and virtual functions$ ^\s*ASSERT false // dereferenced function pointer must be one of \[(f[1-9], ){8}f[1-9]\]$ replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc index a376a6fb940..084ead835ed 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-goto-functions --pointer-check +--show-goto-functions --pointer-check --verbosity 8 ^Removal of function pointers and virtual functions$ ^\s*ASSERT false // dereferenced function pointer must be one of \[(f[1-9], ){8}f[1-9]\]$ replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc index 65e2f401b56..4bf0155236f 100644 --- a/regression/goto-analyzer/no-match-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-null/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-goto-functions --pointer-check +--show-goto-functions --pointer-check --verbosity 8 ^Removal of function pointers and virtual functions$ ^\s*ASSERT false // no candidates for dereferenced function pointer function func: replacing function pointer by 0 possible targets diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc index 027977038b9..a773197ea62 100644 --- a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-goto-functions --pointer-check +--show-goto-functions --pointer-check --verbosity 8 ^Removal of function pointers and virtual functions$ ^\s*ASSERT false // no candidates for dereferenced function pointer ^EXIT=0$ diff --git a/regression/goto-analyzer/value-set-function-pointers-arrays/test.desc b/regression/goto-analyzer/value-set-function-pointers-arrays/test.desc index 3eca46105ab..bf9f5769e72 100644 --- a/regression/goto-analyzer/value-set-function-pointers-arrays/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-arrays/test.desc @@ -1,6 +1,6 @@ CORE main.c ---variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --three-way-merge +--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --three-way-merge --verbosity 8 ^file main.c line 29 function main: replacing function pointer by 2 possible targets$ ^file main.c line 40 function main: replacing function pointer by 2 possible targets$ ^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end diff --git a/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc b/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc index d1ff293516a..1a092db3f5d 100644 --- a/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check +--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check --verbosity 8 ^file main.c line 28 function main: replacing function pointer by 2 possible targets$ ^main::1::fun_incremented_show \(\) -> value-set-begin: TOP :value-set-end ^EXIT=0$ diff --git a/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc b/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc index 1cb8f3ff001..119f100cb7a 100644 --- a/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc @@ -1,6 +1,6 @@ CORE main.c ---variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check +--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check --verbosity 8 ^file main.c line 32 function main: replacing function pointer by 3 possible targets$ ^main::1::fun_incremented_show \(\) -> value-set-begin: TOP, ptr ->\(h\) :value-set-end ^EXIT=0$ diff --git a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc index 604658c3d80..2139adad327 100644 --- a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc @@ -1,6 +1,6 @@ CORE main.c ---variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --three-way-merge +--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --three-way-merge --verbosity 8 ^file main.c line 25 function main: replacing function pointer by 2 possible targets$ ^file main.c line 28 function main: replacing function pointer by 2 possible targets$ ^file main.c line 33 function main: replacing function pointer by 2 possible targets$ diff --git a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc index 20d6e0f8275..67de292e3c8 100644 --- a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc @@ -1,6 +1,6 @@ CORE main.c ---variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check +--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --verbosity 8 ^file main.c line 38 function main: replacing function pointer by 2 possible targets$ ^file main.c line 46 function main: replacing function pointer by 2 possible targets$ ^file main.c line 54 function main: replacing function pointer by 2 possible targets$ diff --git a/regression/goto-instrument/unwind-continue-as-loops1/test.desc b/regression/goto-instrument/unwind-continue-as-loops1/test.desc index 7f4b4a94a08..b9d1d7ac887 100644 --- a/regression/goto-instrument/unwind-continue-as-loops1/test.desc +++ b/regression/goto-instrument/unwind-continue-as-loops1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 5 --continue-as-loops +--verbosity 10 --unwind 5 --continue-as-loops _ --verbosity 8 ^Unwinding loop.*iteration 5 ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/unwind-unwindset2/test.desc b/regression/goto-instrument/unwind-unwindset2/test.desc index 98698c90483..daf99d6ac1f 100644 --- a/regression/goto-instrument/unwind-unwindset2/test.desc +++ b/regression/goto-instrument/unwind-unwindset2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwindset main.0:10 --unwinding-assertions +--unwindset main.0:10 --unwinding-assertions _ --verbosity 8 ^Unwinding loop ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/unwind-unwindset3/test.desc b/regression/goto-instrument/unwind-unwindset3/test.desc index 58a253c1062..d767d55e4f6 100644 --- a/regression/goto-instrument/unwind-unwindset3/test.desc +++ b/regression/goto-instrument/unwind-unwindset3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 10 --unwindset main.0: +--unwind 10 --unwindset main.0: _ --verbosity 8 ^Unwinding loop ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/unwind-zero-unwind2/test.desc b/regression/goto-instrument/unwind-zero-unwind2/test.desc index dfed669b9e5..6c8dc90d040 100644 --- a/regression/goto-instrument/unwind-zero-unwind2/test.desc +++ b/regression/goto-instrument/unwind-zero-unwind2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 0 --continue-as-loops +--unwind 0 --continue-as-loops _ --verbosity 8 ^Unwinding loop.*iteration 10 ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/value-set-fi-fp-removal4/test.desc b/regression/goto-instrument/value-set-fi-fp-removal4/test.desc index 3dcd00d81c1..111a905eac3 100644 --- a/regression/goto-instrument/value-set-fi-fp-removal4/test.desc +++ b/regression/goto-instrument/value-set-fi-fp-removal4/test.desc @@ -1,6 +1,6 @@ CORE test.c ---value-set-fi-fp-removal _ --no-standard-checks +--value-set-fi-fp-removal --verbosity 8 _ --no-standard-checks ^EXIT=10$ ^SIGNAL=0$ ^file test.c line 20 function main: replacing function pointer by 2 possible targets$ diff --git a/regression/goto-instrument/value-set-fi-fp-removal5/test.desc b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc index 8dc63364085..a18de12a0e7 100644 --- a/regression/goto-instrument/value-set-fi-fp-removal5/test.desc +++ b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc @@ -1,6 +1,6 @@ CORE test.c ---value-set-fi-fp-removal _ --no-standard-checks +--value-set-fi-fp-removal --verbosity 8 _ --no-standard-checks ^EXIT=10$ ^SIGNAL=0$ ^file test.c line 19 function main: replacing function pointer by 0 possible targets$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 8c4a6d6fcd9..6548067d791 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -500,7 +500,7 @@ int cbmc_parse_optionst::doit() get_command_line_options(options); messaget::eval_verbosity( - cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); + cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler); log_version_and_architecture("CBMC"); @@ -1081,7 +1081,7 @@ void cbmc_parse_optionst::help() HELP_JSON_INTERFACE HELP_GOTO_TRACE HELP_FLUSH - " {y--verbosity} {u#} \t verbosity level\n" + " {y--verbosity} {u#} \t verbosity level (default 6)\n" HELP_TIMESTAMP "\n"); // clang-format on diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 830f3f9f509..605c93421cb 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -408,7 +408,7 @@ int goto_analyzer_parse_optionst::doit() optionst options; get_command_line_options(options); messaget::eval_verbosity( - cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); + cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler); log_version_and_architecture("GOTO-ANALYZER"); diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 627ae6e3d41..25aa59c10ac 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -85,7 +85,7 @@ int goto_diff_parse_optionst::doit() optionst options; get_command_line_options(options); messaget::eval_verbosity( - cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); + cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler); log_version_and_architecture("GOTO-DIFF"); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3d85e200efc..868d2027a16 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -125,7 +125,7 @@ int goto_instrument_parse_optionst::doit() } messaget::eval_verbosity( - cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); + cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler); { register_languages(); diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index 3e4f3fe4dbc..93f264fd24e 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -58,7 +58,7 @@ int goto_synthesizer_parse_optionst::doit() } messaget::eval_verbosity( - cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); + cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler); register_languages(); diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp index dd9a2d79dba..58f87fa9dda 100644 --- a/src/symtab2gb/symtab2gb_parse_options.cpp +++ b/src/symtab2gb/symtab2gb_parse_options.cpp @@ -66,7 +66,7 @@ static void run_symtab2gb( stream_message_handlert message_handler{std::cerr}; messaget::eval_verbosity( - cmdline_verbosity, messaget::M_STATISTICS, message_handler); + cmdline_verbosity, messaget::M_STATUS, message_handler); auto const symtab_language = new_json_symtab_language();