Merge pull request #6119 from tautschnig/concurrency-spawn

Concurrency: do not lose L2 entries of procedure-local variables

Author: tautschnig

regression/cbmc-concurrency/stack2/main.c

@@ -0,0 +1,17 @@
+void foo(unsigned x)
+{
+  __CPROVER_assert(x <= 1, "");
+}
+
+int main()
+{
+  unsigned local_to_main;
+  local_to_main %= 2;
+  _Bool nondet1;
+  if(nondet1)
+  {
+  __CPROVER_ASYNC_1:
+    foo(local_to_main);
+    return 0;
+  }
+}

regression/cbmc-concurrency/stack2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Procedure-local variables must be copied into a newly created thread, and must
+not be lost when merging goto states.

src/goto-symex/symex_goto.cpp

@@ -784,8 +784,12 @@ static void merge_names(
   // only later be removed from level2.current_names by pop_frame
   // once the thread is executed)
   const irep_idt level_0 = ssa.get_level_0();
-  if(!level_0.empty() && level_0 != std::to_string(dest_state.source.thread_nr))
+  if(
+    !level_0.empty() &&
+    level_0 != std::to_string(dest_state.source.thread_nr) && dest_count != 0)
+  {
     return;
+  }
 
   exprt goto_state_rhs = ssa, dest_state_rhs = ssa;