From 26b13ae43fa9fca8078061f987e7087528502142 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 1 Jan 2017 14:12:28 +0000 Subject: [PATCH] Abort concurrency encoding in possibly unsound cases --- regression/cbmc-concurrency/thread_chain_posix2/test.desc | 2 +- regression/cbmc-concurrency/thread_chain_posix3/test.desc | 2 +- regression/cbmc/realloc3/test.desc | 8 ++++++-- src/goto-symex/goto_symex_state.cpp | 4 ++++ 4 files changed, 12 insertions(+), 4 deletions(-) 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))