Fixed cbmc-concurrency regressions

esteffin · esteffin · commit 9d094fc7423b · 2023-12-14T18:02:12.000Z
diff --git a/regression/cbmc-concurrency/atomic_section_sc3/test.desc b/regression/cbmc-concurrency/atomic_section_sc3/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/deadlock1/test.desc b/regression/cbmc-concurrency/deadlock1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/deadlock2/test.desc b/regression/cbmc-concurrency/deadlock2/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-concurrency/dirty_local1/test.desc b/regression/cbmc-concurrency/dirty_local1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-concurrency/dirty_local2/test.desc b/regression/cbmc-concurrency/dirty_local2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-concurrency/dirty_local3/test-local.desc b/regression/cbmc-concurrency/dirty_local3/test-local.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
--Dlocals_bug
+--no-standard-checks -Dlocals_bug
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/dirty_local3/test.desc b/regression/cbmc-concurrency/dirty_local3/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/invalid_object1/test.desc b/regression/cbmc-concurrency/invalid_object1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-concurrency/memory_barrier1/test.desc b/regression/cbmc-concurrency/memory_barrier1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
---unwind 1 --no-unwinding-assertions
+--no-standard-checks --unwind 1 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/norace_array1/test.desc b/regression/cbmc-concurrency/norace_array1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/norace_array2/test.desc b/regression/cbmc-concurrency/norace_array2/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/norace_scalar1/test.desc b/regression/cbmc-concurrency/norace_scalar1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/norace_struct1/test.desc b/regression/cbmc-concurrency/norace_struct1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/pthread_create_tso1/test.desc b/regression/cbmc-concurrency/pthread_create_tso1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
---mm tso
+--no-pointer-check --mm tso
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/regression/cbmc-concurrency/pthread_join1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
---all-properties
+--no-standard-checks --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line 21 assertion i==1: FAILURE$
diff --git a/regression/cbmc-concurrency/pthread_join2/test.desc b/regression/cbmc-concurrency/pthread_join2/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
---unwind 2
+--no-standard-checks --unwind 2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-concurrency/sc6/test.desc b/regression/cbmc-concurrency/sc6/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/stack1/test.desc b/regression/cbmc-concurrency/stack1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/struct_and_array1/test.desc b/regression/cbmc-concurrency/struct_and_array1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc b/regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
---error-label ERROR
+--no-standard-checks --error-label ERROR
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc b/regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
---error-label ERROR
+--no-standard-checks --error-label ERROR
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-concurrency/svcomp13_qrcu_safe/test.desc b/regression/cbmc-concurrency/svcomp13_qrcu_safe/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind 2 --no-unwinding-assertions
+--no-standard-checks --unwind 2 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/thread_chain_cbmc1/test.desc b/regression/cbmc-concurrency/thread_chain_cbmc1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/thread_chain_cbmc2/test.desc b/regression/cbmc-concurrency/thread_chain_cbmc2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
--D_SANITY_CHECK_
+--no-standard-checks -D_SANITY_CHECK_
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-concurrency/thread_chain_posix1/test.desc b/regression/cbmc-concurrency/thread_chain_posix1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-concurrency/thread_local1/test.desc b/regression/cbmc-concurrency/thread_local1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-concurrency/uf_with_threads1/test.desc b/regression/cbmc-concurrency/uf_with_threads1/test.desc
@@ -1,6 +1,6 @@
 CORE pthread
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
