symex_dynamic::dynamic_object_size* are constants

We do not have a notion of guaranteed constants, thus mark them thread-local via
the auxiliary_symbolt constructor. This avoids repeated renaming of the size of
an array, which resulted in spurious errors in concurrent programs (e.g., in
SV-COMP running "cbmc --unwind 2 --stop-on-fail --32
c/pthread-C-DAC/pthread-numerical-integration_true-unreach-call.i").

Author: tautschnig

regression/cbmc-concurrency/malloc2/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+#include <pthread.h>
+
+_Bool set_done;
+int *ptr;
+
+void *set_x(void *arg)
+{
+  *(int *)arg = 10;
+  set_done = 1;
+}
+
+int main(int argc, char *argv[])
+{
+  __CPROVER_assume(argc >= sizeof(int));
+  ptr = malloc(argc);
+  __CPROVER_ASYNC_1: set_x(ptr);
+  __CPROVER_assume(set_done);
+  assert(*ptr == 10);
+  return 0;
+}

regression/cbmc-concurrency/malloc2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/symex_builtin_functions.cpp

@@ -138,14 +138,15 @@ void goto_symext::symex_allocate(
     {
       exprt &size=to_array_type(object_type).size();
 
-      symbolt size_symbol;
+      auxiliary_symbolt size_symbol;
 
       size_symbol.base_name=
         "dynamic_object_size"+std::to_string(dynamic_counter);
       size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
-      size_symbol.is_lvalue=true;
       size_symbol.type=tmp_size.type();
       size_symbol.mode = mode;
+      size_symbol.type.set(ID_C_constant, true);
+      size_symbol.value = size;
 
       state.symbol_table.add(size_symbol);