Enable cbmc-concurrency regression tests by default
For some reason we had not included these in our standard set of regression tests, and sure enough they got out of sync and one actual regression happened.
This commit is contained in:
parent
5ab4e4aa5d
commit
0f2f082552
|
@ -29,6 +29,7 @@ add_subdirectory(goto-analyzer)
|
|||
add_subdirectory(ansi-c)
|
||||
add_subdirectory(goto-instrument)
|
||||
add_subdirectory(cpp)
|
||||
add_subdirectory(cbmc-concurrency)
|
||||
add_subdirectory(cbmc-cover)
|
||||
add_subdirectory(goto-instrument-typedef)
|
||||
add_subdirectory(smt2_solver)
|
||||
|
|
|
@ -7,6 +7,7 @@ DIRS = cbmc \
|
|||
ansi-c \
|
||||
goto-instrument \
|
||||
cpp \
|
||||
cbmc-concurrency \
|
||||
cbmc-cover \
|
||||
goto-instrument-typedef \
|
||||
smt2_solver \
|
||||
|
|
|
@ -0,0 +1,13 @@
|
|||
if(NOT WIN32)
|
||||
add_test_pl_tests(
|
||||
"$<TARGET_FILE:cbmc>"
|
||||
)
|
||||
else()
|
||||
add_test_pl_tests(
|
||||
"$<TARGET_FILE:cbmc>"
|
||||
"cbmc-concurrency"
|
||||
"$<TARGET_FILE:cbmc>"
|
||||
"-C;-X;pthread"
|
||||
"CORE"
|
||||
)
|
||||
endif()
|
|
@ -1,10 +1,17 @@
|
|||
default: tests.log
|
||||
|
||||
include ../../src/config.inc
|
||||
include ../../src/common
|
||||
|
||||
ifeq ($(BUILD_ENV_),MSVC)
|
||||
no_pthread = -X pthread
|
||||
endif
|
||||
|
||||
test:
|
||||
@../test.pl -c ../../../src/cbmc/cbmc
|
||||
@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
|
||||
|
||||
tests.log: ../test.pl
|
||||
@../test.pl -c ../../../src/cbmc/cbmc
|
||||
@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
|
||||
|
||||
show:
|
||||
@for dir in *; do \
|
||||
|
|
|
@ -1,8 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=10$
|
||||
^EXIT=6$
|
||||
^SIGNAL=0$
|
||||
^file main.c line 12 function spawn: start_thread in atomic section detected$
|
||||
^spawning threads out of atomic sections is not allowed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
|
||||
^EXIT=10$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
|
||||
^EXIT=10$
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
#include <stdlib.h>
|
||||
#include <pthread.h>
|
||||
|
||||
#define BUG
|
||||
|
||||
|
@ -13,12 +12,9 @@ void* set_x(void* arg) {
|
|||
}
|
||||
|
||||
int main() {
|
||||
pthread_t thread;
|
||||
x = malloc(sizeof(int));
|
||||
#ifdef BUG
|
||||
__CPROVER_ASYNC_1: set_x(NULL);
|
||||
//pthread_create(&thread,NULL,set_x,NULL);
|
||||
//pthread_join(thread,NULL);
|
||||
__CPROVER_assume(set_done);
|
||||
#else
|
||||
set_x(NULL);
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
#include <stdlib.h>
|
||||
#include <pthread.h>
|
||||
|
||||
_Bool set_done;
|
||||
int *ptr;
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
--unwind 1 --no-unwinding-assertions
|
||||
^EXIT=0$
|
||||
|
|
|
@ -9,7 +9,11 @@ volatile int flag1 = 0, flag2 = 0; // boolean flags
|
|||
void* thr1(void * arg) { // frontend produces 12 transitions from this thread. It would be better if it would produce only 8!
|
||||
flag1 = 1;
|
||||
turn = 1;
|
||||
#ifdef __GNUC__
|
||||
__asm__ __volatile__ ("mfence": : :"memory");
|
||||
#else
|
||||
__CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
|
||||
#endif
|
||||
__CPROVER_assume(! (flag2==1 && turn==1) );
|
||||
// begin: critical section
|
||||
x = 0;
|
||||
|
@ -21,7 +25,11 @@ void* thr1(void * arg) { // frontend produces 12 transitions from this thread. I
|
|||
void* thr2(void * arg) {
|
||||
flag2 = 1;
|
||||
turn = 0;
|
||||
#ifdef __GNUC__
|
||||
__asm__ __volatile__ ("mfence": : :"memory");
|
||||
#else
|
||||
__CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
|
||||
#endif
|
||||
__CPROVER_assume(! (flag1==1 && turn==0) );
|
||||
// begin: critical section
|
||||
x = 1;
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
KNOWNBUG
|
||||
main.c
|
||||
--mm tso
|
||||
^EXIT=0$
|
||||
|
@ -6,3 +6,5 @@ main.c
|
|||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
Some past change broke this test such that we now report verification failures.
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
-DMUTEX
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
KNOWNBUG pthread
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
KNOWNBUG pthread
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
KNOWNBUG pthread
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
--mm tso
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
--all-properties
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main\.assertion\.1\] assertion i==1: FAILURE$
|
||||
^\[main\.assertion\.2\] assertion i==2: SUCCESS$
|
||||
^\[main\.assertion\.1\] line 21 assertion i==1: FAILURE$
|
||||
^\[main\.assertion\.2\] line 22 assertion i==2: SUCCESS$
|
||||
^\*\* 1 of 2 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
--unwind 2
|
||||
^EXIT=10$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
--error-label ERROR
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
--error-label ERROR
|
||||
^EXIT=10$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
|
||||
^EXIT=10$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
KNOWNBUG pthread
|
||||
main.c
|
||||
-D_ENABLE_CHAIN_ --unwind 2
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
KNOWNBUG pthread
|
||||
main.c
|
||||
-D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2
|
||||
^EXIT=10$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
^[[:space:]]*r2=1u \(.*\)$
|
||||
^[[:space:]]*r2=1u(l)? \(.*\)$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
CORE pthread
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
Loading…
Reference in New Issue