Skip to content

Commit ef4144b

Browse files
committed
Replace new-smt-backend tag with inverted no-new-smt tag
This makes it somewhat more straight forward to find tests where the new smt backend is not currently run. It also helps with testing with the new smt support on new tests by default. The tags in the `.desc` files are flipped using a one-off python script. I am including it here below in the commit message body rather than in a separate commit as it is intended for a singular usage and it may be more straight forward to review the script than the `.desc` file updates. ``` import os import sys from pathlib import Path def usage(): print("Usage " + sys.argv[0] + " [directory]") print("Processes all test tags within a [directory].") def update_file(file_path) -> bool: with file_path.open("rt") as file: lines = file.readlines() if len(lines) == 0: print("File " + file_path + " is empty") return False if "CORE" not in lines[0]: return False if " new-smt-backend" not in lines[0] and " no-new-smt" not in lines[0]: lines[0] = lines[0].replace("\n", " no-new-smt\n") else: lines[0] = lines[0].replace(" new-smt-backend", "") with file_path.open("wt") as file: file.writelines(lines) return True def main() -> int: if len(sys.argv) != 2: usage() return os.EX_USAGE directory = Path(sys.argv[1]) if not directory.is_absolute(): directory = Path(os.getcwd()) / directory print("Running against directory " + os.fspath(directory)) if not directory.is_dir(): print("Error - This is not a directory.") return os.EX_IOERR files = directory.glob("*/*.desc") tests_updated = 0 for file_path in files: if not file_path.is_file(): print(os.fspath(file_path) + " was expected to be a file but is " "not a file") continue if update_file(file_path): tests_updated += 1 if tests_updated == 0: print("Error - No tests updated") return os.EX_NOTFOUND print(str(tests_updated) + " tests updated.") return os.EX_OK if __name__ == '__main__': sys.exit(main()) ```
1 parent cb62568 commit ef4144b

File tree

1,119 files changed

+1119
-1119
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,119 files changed

+1119
-1119
lines changed

regression/book-examples/abs/C1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
abs.c
33
--function abs
44
^EXIT=0$

regression/book-examples/abs/C13.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
abs.c
33
--function abs --signed-overflow-check --show-goto-functions
44
^EXIT=0$

regression/book-examples/abs/C2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
abs.c
33
--function abs --signed-overflow-check
44
^EXIT=10$

regression/book-examples/abs/C3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
abs.c
33
--function abs --signed-overflow-check --trace
44
^EXIT=10$

regression/book-examples/binsearch/C4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
binsearch.c
33
--function binsearch --unwind 6 --bounds-check --unwinding-assertions
44
^EXIT=0$

regression/book-examples/lock/depth.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
lock.c
33
--depth 10
44
^EXIT=0$

regression/book-examples/lock/unwind1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
lock.c
33
--unwind 1
44
^EXIT=0$

regression/book-examples/lock/unwind2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
lock.c
33
--unwind 2
44
^EXIT=10$

regression/book-examples/login/C5.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
login.c
33
--unwind 20 --bounds-check
44
^EXIT=10$

regression/book-examples/login/C6.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
login.c
33
--show-properties --bounds-check --pointer-check
44
^EXIT=0$

0 commit comments

Comments
 (0)