Skip to content

Commit 3552cfb

Browse files
committed
cbmc-library regression tests: generalise pthread to unix
We have further tests that are Unix-specific, not just the pthread-related ones. To avoid confusion, rename the tag to "unix."
1 parent adfd71d commit 3552cfb

File tree

29 files changed

+31
-31
lines changed

29 files changed

+31
-31
lines changed

regression/cbmc-library/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ add_test_pl_tests(
77
"$<TARGET_FILE:cbmc>"
88
"cbmc-library"
99
"$<TARGET_FILE:cbmc>"
10-
"-C;-X;pthread"
10+
"-C;-X;unix"
1111
"CORE"
1212
)
1313
endif()

regression/cbmc-library/Makefile

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,14 @@ include ../../src/config.inc
44
include ../../src/common
55

66
ifeq ($(BUILD_ENV_),MSVC)
7-
no_pthread = -X pthread
7+
unix_only = -X unix
88
endif
99

1010
test:
11-
@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
11+
@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only)
1212

1313
tests.log: ../test.pl
14-
@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
14+
@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only)
1515

1616
clean:
1717
find . -name '*.out' -execdir $(RM) '{}' \;

regression/cbmc-library/pthread_barrier_destroy-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
KNOWNBUG unix
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

regression/cbmc-library/pthread_barrier_init-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
KNOWNBUG unix
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

regression/cbmc-library/pthread_barrier_wait-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
KNOWNBUG unix
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

regression/cbmc-library/pthread_cancel-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
KNOWNBUG unix
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

regression/cbmc-library/pthread_cond_broadcast-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
KNOWNBUG unix
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

regression/cbmc-library/pthread_cond_init-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
KNOWNBUG unix
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

regression/cbmc-library/pthread_cond_signal-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
KNOWNBUG unix
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

regression/cbmc-library/pthread_cond_wait-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE pthread
1+
CORE unix
22
main.c
33
--bounds-check
44
^EXIT=10$

0 commit comments

Comments
 (0)