Merge pull request #2114 from tautschnig/type-renaming

Ensure consistent type renaming of heap objects of dynamic size

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/ansi-c/c_typecheck_type.cpp

@@ -581,10 +581,9 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
       new_symbol.base_name=id2string(current_symbol.base_name)+suffix;
       new_symbol.type=size.type();
       new_symbol.type.set(ID_C_constant, true);
-      new_symbol.is_type=false;
-      new_symbol.is_static_lifetime=false;
       new_symbol.value=size;
       new_symbol.location=source_location;
+      new_symbol.mode = mode;
 
       symbol_table.add(new_symbol);
 

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