change default verbosity to M_STATUS

kroening · kroening · commit 2632b69d976a · 2024-06-15T11:07:33.000-07:00
This changes the default verbosity from M_STATISTICS to M_STATUS, in an
effort to reduce the amount of console output.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/sat-solver/test.desc b/regression/cbmc/sat-solver/test.desc
@@ -1,6 +1,6 @@
 CORE broken-z3-smt-backend broken-cprover-smt-backend no-new-smt
 test.c
---sat-solver cadical
+--sat-solver cadical --verbosity 8
 ^EXIT=10$
 ^SIGNAL=0$
 Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind 5 --continue-as-loops
+--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
@@ -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
@@ -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
diff --git a/regression/goto-instrument/value-set-fi-fp-removal4/test.desc b/regression/goto-instrument/value-set-fi-fp-removal4/test.desc
diff --git a/regression/goto-instrument/value-set-fi-fp-removal5/test.desc b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp
