Skip to content

change default verbosity to M_STATUS #8331

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 18, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion regression/cbmc-concurrency/constant_prop1/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-incr-oneloop/alarm1/test.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-incr-oneloop/alarm2/test-json-output.desc
Original file line number Diff line number Diff line change
@@ -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"
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc
Original file line number Diff line number Diff line change
@@ -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>
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-incr-oneloop/alarm2/test.desc
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-incr-oneloop/minmaxunwind4/test.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-incr-oneloop/multiple-asserts/test.desc
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-incr-oneloop/valid-asserts/test.desc
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-library/memmove-01/constant.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-shadow-memory/constchar-param1/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--unwind 11
--unwind 11 --verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-with-incr/Fixedbv4/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
FUTURE
main.c
--fixedbv
--fixedbv --verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Array_Propagation1/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/BV_Arithmetic3/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--verbosity 8
^EXIT=0$
^SIGNAL=0$
(Starting CEGAR Loop|^Generated 68 VCC\(s\), 0 remaining after simplification$)
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Bool/bool5-full-slice.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Bool/bool5.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
bool5.c

--verbosity 8
Generated 10 VCC\(s\), 0 remaining after simplification
^VERIFICATION SUCCESSFUL$
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Fixedbv4/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--unwind 8 --verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Float-equality2/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--verbosity 8
(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
^VERIFICATION SUCCESSFUL$
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Pointer_comparison5/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--verbosity 8
^Generated \d+ VCC\(s\), 1 remaining after simplification$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Struct_Propagation1/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--unwind 5
--unwind 5 --verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/bounds_check2/test.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/condition-propagation-1/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
test.c

--verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/condition-propagation-2/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
test.c

--verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/condition-propagation-3/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
test.c

--verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/condition-propagation-4/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
test.c

--verbosity 8
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/constant_folding3/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--verbosity 8
^Generated 1 VCC\(s\), 0 remaining after simplification$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/field-sensitivity14/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE no-new-smt
main.c

--verbosity 8
^Generated \d+ VCC\(s\), \d remaining after simplification$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/gcc_builtin_sub_overflow/simplify.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
simplify.c

--verbosity 8
^Generated 2 VCC\(s\), 0 remaining after simplification$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/json-interface1/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
--json-interface
< test.json
--verbosity 8 < test.json
activate-multi-line-match
^EXIT=10$
^SIGNAL=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/no-propagation/test.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/null8/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--verbosity 8
Generated 1 VCC\(s\), 0 remaining after simplification
^EXIT=0$
^SIGNAL=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/runtime-profiling/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--no-standard-checks
--no-standard-checks --verbosity 8
^EXIT=0$
^SIGNAL=0$
^Runtime Symex:.*$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/self_loops_to_assumptions1/default.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/simplify-union/test.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/union13/no-arch.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/union18/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

--verbosity 8
^Generated 1 VCC\(s\), 0 remaining after simplification$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/unreachable-goto1/test-vccs.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/unreachable-goto2/test-vccs.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/unreachable-goto3/test-vccs.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/unreachable-goto4/test-vccs.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/unreachable-goto5/test-vccs.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/unreachable-goto6/test-vccs.desc
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/xml-interface1/test.desc
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -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]$
Expand Down
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Loading
Loading