Skip to content

Replace new-smt-backend tag with inverted no-new-smt tag #8002

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.

Sign up for GitHub

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 3 commits into from
Nov 14, 2023
Merged

Replace new-smt-backend tag with inverted no-new-smt tag #8002

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ef4144b
Replace `new-smt-backend` tag with inverted `no-new-smt` tag
thomasspriggs Nov 7, 2023
4452558
Update test runner replace `new-smt-backend` with `no-new-smt`
thomasspriggs Nov 14, 2023
4590da1
Remove double spaces from between test tags
thomasspriggs Nov 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
4 changes: 2 additions & 2 deletions regression/book-examples/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,11 +30,11 @@ add_test_pl_profile(
"CORE"
)

# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
# If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
add_test_pl_profile(
"book-examples-new-smt-backend"
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
"${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
"${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
"CORE"
)

Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ test-paths-lifo:

test-new-smt-backend:
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
-I new-smt-backend \
-X no-new-smt \
-s new-smt-backend $(GCC_ONLY)

tests.log: ../test.pl test
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/abs/C1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
abs.c
--function abs
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/abs/C13.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
abs.c
--function abs --signed-overflow-check --show-goto-functions
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/abs/C2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
abs.c
--function abs --signed-overflow-check
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/abs/C3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
abs.c
--function abs --signed-overflow-check --trace
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/binsearch/C4.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
binsearch.c
--function binsearch --unwind 6 --bounds-check --unwinding-assertions
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/lock/depth.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
lock.c
--depth 10
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/lock/unwind1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
lock.c
--unwind 1
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/lock/unwind2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
lock.c
--unwind 2
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/login/C5.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
login.c
--unwind 20 --bounds-check
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/login/C6.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
login.c
--show-properties --bounds-check --pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/login/C7.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
login.c
--unwind 20 --show-vcc --bounds-check --pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/login/C8.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
login.c
--unwind 20 --bounds-check --pointer-check
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/login/C9.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
login.c
--unwind 20 --bounds-check --pointer-check --trace
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/book-examples/pid/C11.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
CORE no-new-smt
pid.c
--cover mcdc --unwind 6
^EXIT=0$
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc-primitives/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@ if(Z3_EXISTS)
"$<TARGET_FILE:cbmc>"
)

# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
# If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
add_test_pl_profile(
"cbmc-primitives-new-smt-backend"
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
"-I;new-smt-backend;-s;new-smt-backend"
"-X;no-new-smt;-s;new-smt-backend"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks off, but I don't recall the exact syntax here.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not convinced there is anything wrong here? We want to flip to selectively excluding rather than selectively including tests.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I clearly was not really clear. The change from -I to -X is correct, but there remains the -s;new-smt-backend which looks off to me. That said, I don't recall the syntax (and should check).

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess that's ok for it's an arbitrary string to disambiguate log files:

$ regression/test.pl --help
[...]
  -s <suffix>  append <suffix> to all output and log files. Enables concurrent
             testing of the same desc file with different commands or options,
             as runs with different suffixes will operate independently and keep
             independent logs.
[...]

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As per the previous comment the -s disambiguates log files. So updating it to contain "no" for example would seem incorrect/misleading. It would match the tag but appear in the file name of output files where the "no" tag is not present. @TGWDB Ok if I consider this comment to be resolved?

"CORE"
)
else()
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ test:
@../test.pl -e -p -c ../../../src/cbmc/cbmc

test.smt2_incr:
@../test.pl -e -p -I new-smt-backend -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
@../test.pl -e -p -X no-new-smt -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"

tests.log: ../test.pl
@../test.pl -e -p -c ../../../src/cbmc/cbmc
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
CORE no-new-smt
exists_in_forall.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
CORE no-new-smt
forall_in_exists.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--no-simplify --no-propagation
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/dynamic-object-02/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/exists_assume_6231/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
CORE no-new-smt
test.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/exists_assume_6231/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
test2.c
--pointer-check
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
CORE no-new-smt
invalid_index_range.c
--pointer-check
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/exists_memory_checks/negated_exists.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
CORE no-new-smt
negated_exists.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE smt-backend
CORE smt-backend no-new-smt
smt_missing_range_check.c
--pointer-check -z3
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
CORE no-new-smt
valid_index_range.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/forall_6231_1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
test.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/forall_6231_2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
test.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/forall_6231_3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
test.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
test_malloc_less_than_bound.c
--pointer-check
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/forall_6231_4/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
test.c
--div-by-zero-check
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/implication_statement_checks_1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
--div-by-zero-check
test.c
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--no-simplify --no-propagation
^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/pointer-offset-01/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_bug/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check --no-simplify --no-propagation
^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check --no-simplify --no-propagation
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_null/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check --no-simplify --no-propagation
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_null/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_valid/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check --no-simplify --no-propagation
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_valid/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_valid_negated/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check --no-simplify --no-propagation
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/r_w_ok_valid_negated/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/same-object-01/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--no-simplify --no-propagation
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/same-object-01/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/same-object-02/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--no-simplify --no-propagation
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/same-object-02/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/same-object-03/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--no-simplify --no-propagation
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/same-object-03/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/same-object-04/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--no-simplify --no-propagation
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-primitives/same-object-04/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/ACSL/operators.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
CORE no-new-smt
operators.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/ACSL/quantifier-precedence.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
quantifier-precedence.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/ASHR1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Address_of1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--stop-on-fail
^\[main\.assertion
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Address_of2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Anonymous_Struct1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
--pointer-check
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Anonymous_Struct2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Anonymous_Struct3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c
-win32
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Array_Access1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Array_Access2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE new-smt-backend
CORE
main.c

^EXIT=0$
Expand Down
Loading