From 0f2f082552f219f32faedeffed6db29d96363998 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 25 Feb 2019 16:18:33 +0000
Subject: [PATCH 1/3] 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.
---
 regression/CMakeLists.txt                           |  1 +
 regression/Makefile                                 |  1 +
 regression/cbmc-concurrency/CMakeLists.txt          | 13 +++++++++++++
 regression/cbmc-concurrency/Makefile                | 11 +++++++++--
 .../cbmc-concurrency/atomic_section_sc6/test.desc   |  4 ++--
 .../cbmc-concurrency/conditional_spawn1/test.desc   |  2 +-
 regression/cbmc-concurrency/deadlock1/test.desc     |  2 +-
 regression/cbmc-concurrency/deadlock2/test.desc     |  2 +-
 regression/cbmc-concurrency/malloc1/main.c          |  4 ----
 regression/cbmc-concurrency/malloc2/main.c          |  1 -
 .../cbmc-concurrency/memory_barrier1/test.desc      |  2 +-
 regression/cbmc-concurrency/memory_barrier2/main.c  |  8 ++++++++
 .../cbmc-concurrency/memory_barrier2/test.desc      |  4 +++-
 regression/cbmc-concurrency/mutex2/test.desc        |  2 +-
 regression/cbmc-concurrency/norace_array1/test.desc |  2 +-
 regression/cbmc-concurrency/norace_array2/test.desc |  2 +-
 .../cbmc-concurrency/norace_scalar1/test.desc       |  2 +-
 .../cbmc-concurrency/norace_struct1/test.desc       |  2 +-
 .../cbmc-concurrency/pthread_create_tso1/test.desc  |  2 +-
 regression/cbmc-concurrency/pthread_join1/test.desc |  6 +++---
 regression/cbmc-concurrency/pthread_join2/test.desc |  2 +-
 regression/cbmc-concurrency/sc6/test.desc           |  2 +-
 .../svcomp13_fib_bench_longer_safe/test.desc        |  2 +-
 .../svcomp13_fib_bench_longer_unsafe/test.desc      |  2 +-
 .../cbmc-concurrency/thread_chain_posix1/test.desc  |  2 +-
 .../cbmc-concurrency/thread_chain_posix2/test.desc  |  2 +-
 .../cbmc-concurrency/thread_chain_posix3/test.desc  |  2 +-
 regression/cbmc-concurrency/thread_local1/test.desc |  2 +-
 regression/cbmc-concurrency/trace1/test.desc        |  2 +-
 .../cbmc-concurrency/uf_with_threads1/test.desc     |  2 +-
 30 files changed, 60 insertions(+), 33 deletions(-)
 create mode 100644 regression/cbmc-concurrency/CMakeLists.txt

diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index d8be7b70391..1d6765b5444 100644
--- a/regression/CMakeLists.txt
+++ b/regression/CMakeLists.txt
@@ -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)
diff --git a/regression/Makefile b/regression/Makefile
index 7711fc2e71f..ba29a2d779b 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -7,6 +7,7 @@ DIRS = cbmc \
        ansi-c \
        goto-instrument \
        cpp \
+       cbmc-concurrency \
        cbmc-cover \
        goto-instrument-typedef \
        smt2_solver \
diff --git a/regression/cbmc-concurrency/CMakeLists.txt b/regression/cbmc-concurrency/CMakeLists.txt
new file mode 100644
index 00000000000..474d43f5e8f
--- /dev/null
+++ b/regression/cbmc-concurrency/CMakeLists.txt
@@ -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()
diff --git a/regression/cbmc-concurrency/Makefile b/regression/cbmc-concurrency/Makefile
index bf0682a5381..0938189c76d 100644
--- a/regression/cbmc-concurrency/Makefile
+++ b/regression/cbmc-concurrency/Makefile
@@ -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 \
diff --git a/regression/cbmc-concurrency/atomic_section_sc6/test.desc b/regression/cbmc-concurrency/atomic_section_sc6/test.desc
index ba6a0ba4418..9da4f1f46cb 100644
--- a/regression/cbmc-concurrency/atomic_section_sc6/test.desc
+++ b/regression/cbmc-concurrency/atomic_section_sc6/test.desc
@@ -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
diff --git a/regression/cbmc-concurrency/conditional_spawn1/test.desc b/regression/cbmc-concurrency/conditional_spawn1/test.desc
index 6de79559914..a844f976721 100644
--- a/regression/cbmc-concurrency/conditional_spawn1/test.desc
+++ b/regression/cbmc-concurrency/conditional_spawn1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/deadlock1/test.desc b/regression/cbmc-concurrency/deadlock1/test.desc
index 9efefbc7362..8ecf05b6d5c 100644
--- a/regression/cbmc-concurrency/deadlock1/test.desc
+++ b/regression/cbmc-concurrency/deadlock1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/deadlock2/test.desc b/regression/cbmc-concurrency/deadlock2/test.desc
index 6de79559914..a844f976721 100644
--- a/regression/cbmc-concurrency/deadlock2/test.desc
+++ b/regression/cbmc-concurrency/deadlock2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/malloc1/main.c b/regression/cbmc-concurrency/malloc1/main.c
index 089a949e211..75ae2170167 100644
--- a/regression/cbmc-concurrency/malloc1/main.c
+++ b/regression/cbmc-concurrency/malloc1/main.c
@@ -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);
diff --git a/regression/cbmc-concurrency/malloc2/main.c b/regression/cbmc-concurrency/malloc2/main.c
index 8634e886ccf..1e5a3f47a86 100644
--- a/regression/cbmc-concurrency/malloc2/main.c
+++ b/regression/cbmc-concurrency/malloc2/main.c
@@ -1,5 +1,4 @@
 #include <stdlib.h>
-#include <pthread.h>
 
 _Bool set_done;
 int *ptr;
diff --git a/regression/cbmc-concurrency/memory_barrier1/test.desc b/regression/cbmc-concurrency/memory_barrier1/test.desc
index 4d988589f85..4ea6a9ab003 100644
--- a/regression/cbmc-concurrency/memory_barrier1/test.desc
+++ b/regression/cbmc-concurrency/memory_barrier1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --unwind 1 --no-unwinding-assertions
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/memory_barrier2/main.c b/regression/cbmc-concurrency/memory_barrier2/main.c
index b6cf59e17e8..62c781f2f9e 100644
--- a/regression/cbmc-concurrency/memory_barrier2/main.c
+++ b/regression/cbmc-concurrency/memory_barrier2/main.c
@@ -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;
diff --git a/regression/cbmc-concurrency/memory_barrier2/test.desc b/regression/cbmc-concurrency/memory_barrier2/test.desc
index 50db92e26ba..4c49d4398c6 100644
--- a/regression/cbmc-concurrency/memory_barrier2/test.desc
+++ b/regression/cbmc-concurrency/memory_barrier2/test.desc
@@ -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.
diff --git a/regression/cbmc-concurrency/mutex2/test.desc b/regression/cbmc-concurrency/mutex2/test.desc
index 793ed9c9713..4175753497f 100644
--- a/regression/cbmc-concurrency/mutex2/test.desc
+++ b/regression/cbmc-concurrency/mutex2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 -DMUTEX
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_array1/test.desc b/regression/cbmc-concurrency/norace_array1/test.desc
index 52168c7eba4..c239dca4b31 100644
--- a/regression/cbmc-concurrency/norace_array1/test.desc
+++ b/regression/cbmc-concurrency/norace_array1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_array2/test.desc b/regression/cbmc-concurrency/norace_array2/test.desc
index 52168c7eba4..c239dca4b31 100644
--- a/regression/cbmc-concurrency/norace_array2/test.desc
+++ b/regression/cbmc-concurrency/norace_array2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_scalar1/test.desc b/regression/cbmc-concurrency/norace_scalar1/test.desc
index 9efefbc7362..8ecf05b6d5c 100644
--- a/regression/cbmc-concurrency/norace_scalar1/test.desc
+++ b/regression/cbmc-concurrency/norace_scalar1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_struct1/test.desc b/regression/cbmc-concurrency/norace_struct1/test.desc
index 52168c7eba4..c239dca4b31 100644
--- a/regression/cbmc-concurrency/norace_struct1/test.desc
+++ b/regression/cbmc-concurrency/norace_struct1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/pthread_create_tso1/test.desc b/regression/cbmc-concurrency/pthread_create_tso1/test.desc
index 50db92e26ba..5fbf3fd711b 100644
--- a/regression/cbmc-concurrency/pthread_create_tso1/test.desc
+++ b/regression/cbmc-concurrency/pthread_create_tso1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --mm tso
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/regression/cbmc-concurrency/pthread_join1/test.desc
index bf4baf2d440..64abf7b96fe 100644
--- a/regression/cbmc-concurrency/pthread_join1/test.desc
+++ b/regression/cbmc-concurrency/pthread_join1/test.desc
@@ -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
diff --git a/regression/cbmc-concurrency/pthread_join2/test.desc b/regression/cbmc-concurrency/pthread_join2/test.desc
index df2241a3a99..484196dfc22 100644
--- a/regression/cbmc-concurrency/pthread_join2/test.desc
+++ b/regression/cbmc-concurrency/pthread_join2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --unwind 2
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/sc6/test.desc b/regression/cbmc-concurrency/sc6/test.desc
index 9efefbc7362..8ecf05b6d5c 100644
--- a/regression/cbmc-concurrency/sc6/test.desc
+++ b/regression/cbmc-concurrency/sc6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc b/regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc
index 70ec811e3d7..ca4c96fa52d 100644
--- a/regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc
+++ b/regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --error-label ERROR
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc b/regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc
index e14ade773e5..e1eca94365c 100644
--- a/regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc
+++ b/regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --error-label ERROR
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/thread_chain_posix1/test.desc b/regression/cbmc-concurrency/thread_chain_posix1/test.desc
index 6de79559914..a844f976721 100644
--- a/regression/cbmc-concurrency/thread_chain_posix1/test.desc
+++ b/regression/cbmc-concurrency/thread_chain_posix1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/thread_chain_posix2/test.desc b/regression/cbmc-concurrency/thread_chain_posix2/test.desc
index 144bf7efe01..59567af5127 100644
--- a/regression/cbmc-concurrency/thread_chain_posix2/test.desc
+++ b/regression/cbmc-concurrency/thread_chain_posix2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 -D_ENABLE_CHAIN_ --unwind 2
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/thread_chain_posix3/test.desc b/regression/cbmc-concurrency/thread_chain_posix3/test.desc
index a2481a984ad..c89f16b63ce 100644
--- a/regression/cbmc-concurrency/thread_chain_posix3/test.desc
+++ b/regression/cbmc-concurrency/thread_chain_posix3/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 -D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/thread_local1/test.desc b/regression/cbmc-concurrency/thread_local1/test.desc
index 9efefbc7362..8ecf05b6d5c 100644
--- a/regression/cbmc-concurrency/thread_local1/test.desc
+++ b/regression/cbmc-concurrency/thread_local1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/trace1/test.desc b/regression/cbmc-concurrency/trace1/test.desc
index a6f904e7a86..6ab54d51ab5 100644
--- a/regression/cbmc-concurrency/trace1/test.desc
+++ b/regression/cbmc-concurrency/trace1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^[[:space:]]*r2=1u \(.*\)$
+^[[:space:]]*r2=1u(l)? \(.*\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-concurrency/uf_with_threads1/test.desc b/regression/cbmc-concurrency/uf_with_threads1/test.desc
index 9efefbc7362..8ecf05b6d5c 100644
--- a/regression/cbmc-concurrency/uf_with_threads1/test.desc
+++ b/regression/cbmc-concurrency/uf_with_threads1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$

From fc69353d919f2238a095e52f6f548cd87c47fd91 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 25 Feb 2019 17:27:54 +0000
Subject: [PATCH 2/3] Fix goto-program conversion of fence instructions

Using it->code.set(ID_statement, ...) no longer suffices as it will not set
code.id(), which is ID_nil after initialisation. Thus any such instruction is
removed during goto-program cleanup.

Use the recently added APIs instead, which will ensure proper initialisation.
---
 .../memory_barrier2/test.desc                 |  2 +-
 src/goto-programs/builtin_functions.cpp       | 37 ++++++++-----------
 2 files changed, 17 insertions(+), 22 deletions(-)

diff --git a/regression/cbmc-concurrency/memory_barrier2/test.desc b/regression/cbmc-concurrency/memory_barrier2/test.desc
index 4c49d4398c6..ebbbcd3d211 100644
--- a/regression/cbmc-concurrency/memory_barrier2/test.desc
+++ b/regression/cbmc-concurrency/memory_barrier2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --mm tso
 ^EXIT=0$
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 69703186f7d..0792f2e086e 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1065,15 +1065,14 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    goto_programt::targett t=dest.add_instruction(OTHER);
-    t->source_location=function.source_location();
-    t->code.set(ID_statement, ID_fence);
-
+    codet fence(ID_fence);
     forall_expr(it, arguments)
     {
       const irep_idt kind=get_string_constant(*it);
-      t->code.set(kind, true);
+      fence.set(kind, true);
     }
+
+    dest.add(goto_programt::make_other(fence, function.source_location()));
   }
   else if(identifier=="__builtin_prefetch")
   {
@@ -1268,10 +1267,9 @@ void goto_convertt::do_function_call_symbol(
     t3->code=code_assignt(deref_ptr, op_expr);
 
     // this instruction implies an mfence, i.e., WRfence
-    goto_programt::targett t4=dest.add_instruction(OTHER);
-    t4->source_location=function.source_location();
-    t4->code=codet(ID_fence);
-    t4->code.set(ID_WRfence, true);
+    codet fence(ID_fence);
+    fence.set(ID_WRfence, true);
+    dest.add(goto_programt::make_other(fence, function.source_location()));
 
     goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
     t5->source_location=function.source_location();
@@ -1339,10 +1337,9 @@ void goto_convertt::do_function_call_symbol(
     }
 
     // this instruction implies an mfence, i.e., WRfence
-    goto_programt::targett t4=dest.add_instruction(OTHER);
-    t4->source_location=function.source_location();
-    t4->code=codet(ID_fence);
-    t4->code.set(ID_WRfence, true);
+    codet fence(ID_fence);
+    fence.set(ID_WRfence, true);
+    dest.add(goto_programt::make_other(fence, function.source_location()));
 
     goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
     t5->source_location=function.source_location();
@@ -1410,10 +1407,9 @@ void goto_convertt::do_function_call_symbol(
     t3->code=code_assignt(deref_ptr, if_expr);
 
     // this instruction implies an mfence, i.e., WRfence
-    goto_programt::targett t4=dest.add_instruction(OTHER);
-    t4->source_location=function.source_location();
-    t4->code=codet(ID_fence);
-    t4->code.set(ID_WRfence, true);
+    codet fence(ID_fence);
+    fence.set(ID_WRfence, true);
+    dest.add(goto_programt::make_other(fence, function.source_location()));
 
     goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
     t5->source_location=function.source_location();
@@ -1471,10 +1467,9 @@ void goto_convertt::do_function_call_symbol(
     t3->code=code_assignt(deref_ptr, if_expr);
 
     // this instruction implies an mfence, i.e., WRfence
-    goto_programt::targett t4=dest.add_instruction(OTHER);
-    t4->source_location=function.source_location();
-    t4->code=codet(ID_fence);
-    t4->code.set(ID_WRfence, true);
+    codet fence(ID_fence);
+    fence.set(ID_WRfence, true);
+    dest.add(goto_programt::make_other(fence, function.source_location()));
 
     goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
     t5->source_location=function.source_location();

From 78437a18734021d3c08bd01efa4993c865d33e56 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 25 Feb 2019 20:34:17 +0000
Subject: [PATCH 3/3] Also disable pthread tests on OSX

They all fail with "pointer handling for concurrency is unsound."
---
 regression/cbmc-concurrency/CMakeLists.txt | 2 +-
 regression/cbmc-concurrency/Makefile       | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/regression/cbmc-concurrency/CMakeLists.txt b/regression/cbmc-concurrency/CMakeLists.txt
index 474d43f5e8f..eab4a322066 100644
--- a/regression/cbmc-concurrency/CMakeLists.txt
+++ b/regression/cbmc-concurrency/CMakeLists.txt
@@ -1,4 +1,4 @@
-if(NOT WIN32)
+if((NOT WIN32) AND (NOT APPLE))
 add_test_pl_tests(
     "$<TARGET_FILE:cbmc>"
 )
diff --git a/regression/cbmc-concurrency/Makefile b/regression/cbmc-concurrency/Makefile
index 0938189c76d..ba490831aa4 100644
--- a/regression/cbmc-concurrency/Makefile
+++ b/regression/cbmc-concurrency/Makefile
@@ -3,7 +3,9 @@ default: tests.log
 include ../../src/config.inc
 include ../../src/common
 
-ifeq ($(BUILD_ENV_),MSVC)
+ifeq ($(filter-out OSX MSVC,$(BUILD_ENV_)),)
+	# no POSIX threads on Windows
+	# for OSX we'd need sound handling of pointers in multi-threaded programs
 	no_pthread = -X pthread
 endif