Merge pull request #1994 from tautschnig/concurrency-soundness

[SV-COMP'18 5/19] Abort concurrency encoding in possibly unsound cases

Author: tautschnig

regression/cbmc-concurrency/thread_chain_posix2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 -D_ENABLE_CHAIN_ --unwind 2
 ^EXIT=0$

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$

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.

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))