Calls to do_initialization may change the initializer in a declaration, introducing additional symbols

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3153 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc/Initialization3/main.c

@@ -0,0 +1,31 @@
+typedef struct _this {
+  int ndim;
+  void *voidregion;
+} This;
+
+#define NDIM t->ndim
+
+void Split(This *t)
+{
+typedef struct region {
+  int bounds[NDIM];
+} Region;
+
+  // The following has to be equivalent to
+  // Region *region;
+  // region = (Region*)t->voidregion;
+  Region *region = (Region*)t->voidregion;
+  unsigned size=sizeof(region->bounds);
+  assert(size==NDIM*sizeof(int));
+}
+
+int main()
+{
+  struct {
+    int bounds[42];
+  } s;
+  This t={ .ndim=42, .voidregion=&s };
+  Split(&t);
+  return 0;
+}
+

regression/cbmc/Initialization3/test.desc

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

regression/cbmc/Initialization5/main.c

@@ -0,0 +1,34 @@
+extern int __VERIFIER_nondet_int(void);
+
+typedef enum {
+  LIST_BEG,
+  LIST_END
+} end_point_t;
+
+typedef enum {
+  ITEM_PREV,
+  ITEM_NEXT
+} direction_t;
+
+void remove_one(end_point_t from)
+{
+  const direction_t next_field = (LIST_BEG == from) ? ITEM_NEXT : ITEM_PREV;
+}
+
+end_point_t rand_end_point(void)
+{
+  _Bool choice;
+  if (choice)
+    return LIST_BEG;
+  else
+    return LIST_END;
+}
+
+int main()
+{
+  remove_one(rand_end_point());
+
+  __CPROVER_assert(0, "");
+
+  return 0;
+}

regression/cbmc/Initialization5/test.desc

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

src/ansi-c/c_typecheck_code.cpp

@@ -396,6 +396,33 @@ void c_typecheck_baset::typecheck_decl(codet &code)
 
 /*******************************************************************\
 
+Function: move_declarations
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void move_declarations(
+  exprt &code,
+  std::list<codet> &clean_code)
+{
+  Forall_operands(it, code)
+    move_declarations(*it, clean_code);
+
+  if(code.id()==ID_code &&
+     to_code(code).get_statement()==ID_decl)
+  {
+    clean_code.push_back(code_skipt());
+    code.swap(clean_code.back());
+  }
+}
+
+/*******************************************************************\
+
 Function: c_typecheck_baset::typecheck_decl
 
   Inputs:
@@ -467,15 +494,19 @@ void c_typecheck_baset::typecheck_decl(
 
   code.location()=symbol.location;
   
-  // check the initializer, if any
+  // handle the initializer, if any
   if(code.operands().size()==2)
   {
-    typecheck_expr(code.op1());
-    do_initializer(code.op1(), symbol.type, false);
-
-    if(follow(symbol.type).id()==ID_array &&
-       to_array_type(follow(symbol.type)).size().is_nil())
-      symbol.type=code.op1().type();
+    // the symbol must have a non-nil value, and its initializer has
+    // been type checked via typecheck_redefinition_non_type already
+    assert(symbol.value.is_not_nil());
+    // move any declarations towards clean_code to make sure these
+    // symbols (e.g., $array_size) have the same lifetime as symbol
+    // and aren't marked dead immediately
+    move_declarations(symbol.value, clean_code);
+    // add typecast, if necessary
+    implicit_typecast(symbol.value, symbol.type);
+    code.op1()=symbol.value;
   }
   
   // set type now (might be changed by initializer)