Merge pull request #8331 from diffblue/change-default-verbosity

change default verbosity to M_STATUS

Author: tautschnig

regression/cbmc-concurrency/constant_prop1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--verbosity 8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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$

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"

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$
 <text>VERIFICATION FAILED</text>

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

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$

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

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

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$

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$

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

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$

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$

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$

regression/cbmc-with-incr/Fixedbv4/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 main.c
---fixedbv
+--fixedbv --verbosity 8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Array_Propagation1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--verbosity 8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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$)

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$

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$

regression/cbmc/Fixedbv4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--unwind 8 --verbosity 8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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$

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$

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$

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$

regression/cbmc/condition-propagation-1/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--verbosity 8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/condition-propagation-2/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--verbosity 8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/condition-propagation-3/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--verbosity 8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/condition-propagation-4/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--verbosity 8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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$

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$

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$

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$

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$

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$

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:.*$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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

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]$

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$

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$

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