diff --git a/regression/cbmc-concurrency/thread_chain_posix2/test.desc b/regression/cbmc-concurrency/thread_chain_posix2/test.desc index 19fca26941b..144bf7efe01 100644 --- a/regression/cbmc-concurrency/thread_chain_posix2/test.desc +++ b/regression/cbmc-concurrency/thread_chain_posix2/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG 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 8c70666b904..a2481a984ad 100644 --- a/regression/cbmc-concurrency/thread_chain_posix3/test.desc +++ b/regression/cbmc-concurrency/thread_chain_posix3/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c -D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2 ^EXIT=10$ diff --git a/regression/cbmc/realloc3/test.desc b/regression/cbmc/realloc3/test.desc index 9efefbc7362..94f222a4b5f 100644 --- a/regression/cbmc/realloc3/test.desc +++ b/regression/cbmc/realloc3/test.desc @@ -1,8 +1,12 @@ CORE main.c -^EXIT=0$ +^EXIT=6$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +pointer handling for concurrency is unsound -- ^warning: ignoring +-- +The test uses "__CPROVER_ASYNC_1:" and the async-called function foo does +pointer operations over allocated memory - which is not handled in a sound way +in CBMC. diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index dc19af71a89..40612693ed7 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -342,6 +342,10 @@ void goto_symex_statet::assignment( assert_l2_renaming(lhs); assert_l2_renaming(rhs); + // see #305 on GitHub for a simple example and possible discussion + if(is_shared && lhs.type().id() == ID_pointer) + throw "pointer handling for concurrency is unsound"; + // for value propagation -- the RHS is L2 if(!is_shared && record_value && constant_propagation(rhs))