Check all struct members for possible need for renaming

regression/cbmc/vla1/main.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  unsigned char x = argc;
+  // make sure int multiplication below won't overflow - type casting to
+  // unsigned long long would be possible, but puts yields a challenging problem
+  // for the SAT solver
+  __CPROVER_assume(x < 1ULL << (sizeof(int) * 8 / 2 - 1));
+
+  struct S
+  {
+    int a;
+    int b[x];
+    int c;
+  };
+
+  if(x % 2 == 0)
+    x = 3;
+
+  struct S s[x];
+
+  __CPROVER_assume(x < 255);
+  ++x;
+
+  assert(sizeof(struct S) == ((unsigned char)argc + 2) * sizeof(int));
+  assert(sizeof(s) == (x - 1) * ((unsigned char)argc + 2) * sizeof(int));
+
+  return 0;
+}

regression/cbmc/vla1/program-only.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+\(__CPROVER_size_t\)x\$array_size
+--
+There should not be any type cast of x$array_size to __CPROVER_size_t, because
+it already is of that type.

regression/cbmc/vla1/test.desc

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

regression/cbmc/vla2/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  unsigned char x = argc;
+  // make sure int multiplication below won't overflow - type casting to
+  // unsigned long long would be possible, but puts yields a challenging problem
+  // for the SAT solver
+  __CPROVER_assume(x < 1ULL << (sizeof(int) * 8 / 2 - 1));
+
+  struct S
+  {
+    int a;
+    int b[x];
+    int c;
+  };
+
+  if(x % 2 == 0)
+    x = 3;
+
+  struct S s[x];
+
+  if((unsigned char)argc > 0)
+  {
+    s[0].b[0] = 42;
+    assert(s[0].b[0] == 42);
+  }
+
+  __CPROVER_assume(x < 255);
+  ++x;
+
+  assert(sizeof(struct S) == ((unsigned char)argc + 2) * sizeof(int));
+  assert(sizeof(s) == (x - 1) * ((unsigned char)argc + 2) * sizeof(int));
+
+  return 0;
+}

regression/cbmc/vla2/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The array decision procedure does not yet handle member expressions.

regression/cbmc/vla3/main.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  unsigned char x = argc;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    struct S
+    {
+      int a;
+      int b[x + i + 1];
+      int *c;
+    } __attribute((packed));
+
+    struct S s;
+
+    for(int j = 0; j < i; ++j)
+      s.b[x + j] = j;
+
+    for(int j = 0; j < i; ++j)
+      assert(s.b[x + j] == j);
+
+    assert(
+      sizeof(struct S) ==
+      sizeof(int *) + ((unsigned char)argc + i + 2) * sizeof(int));
+  }
+
+  return 0;
+}

regression/cbmc/vla3/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Renaming is inconsistent across loop iterations as we map L1 names to types, but
+do not actually introduce new L1 ids each time we declare an object.

src/ansi-c/c_typecheck_type.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/fresh_symbol.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
@@ -608,44 +609,25 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
         throw 0;
       }
 
-      // Need to pull out! We insert new symbol.
-      unsigned count=0;
-      irep_idt temp_identifier;
-      std::string suffix;
-
-      do
-      {
-        suffix="$array_size"+std::to_string(count);
-        temp_identifier=id2string(current_symbol.name)+suffix;
-        count++;
-      }
-      while(symbol_table.symbols.find(temp_identifier)!=
-            symbol_table.symbols.end());
-
-      // add the symbol to symbol table
-      auxiliary_symbolt new_symbol;
-      new_symbol.name=temp_identifier;
-      new_symbol.pretty_name=id2string(current_symbol.pretty_name)+suffix;
-      new_symbol.base_name=id2string(current_symbol.base_name)+suffix;
-      new_symbol.type=size.type();
+      symbolt &new_symbol = get_fresh_aux_symbol(
+        size_type(),
+        id2string(current_symbol.name) + "$array_size",
+        id2string(current_symbol.base_name) + "$array_size",
+        size_source_location,
+        mode,
+        symbol_table);
       new_symbol.type.set(ID_C_constant, true);
-      new_symbol.value=size;
-      new_symbol.location = size_source_location;
-      new_symbol.mode = mode;
-
-      symbol_table.add(new_symbol);
+      new_symbol.value = typecast_exprt::conditional_cast(size, size_type());
 
       // produce the code that declares and initializes the symbol
-      symbol_exprt symbol_expr;
-      symbol_expr.set_identifier(temp_identifier);
-      symbol_expr.type()=new_symbol.type;
+      symbol_exprt symbol_expr = new_symbol.symbol_expr();
 
       code_declt declaration(symbol_expr);
       declaration.add_source_location() = size_source_location;
 
       code_assignt assignment;
       assignment.lhs()=symbol_expr;
-      assignment.rhs()=size;
+      assignment.rhs() = new_symbol.value;
       assignment.add_source_location() = size_source_location;
 
       // store the code

src/goto-symex/goto_symex_state.cpp

@@ -618,6 +618,9 @@ void goto_symex_statet::rename_address(
   }
 }
 
+/// Return true if, and only if, the \p type or one of its subtypes requires SSA
+/// renaming. Renaming is necessary when symbol expressions occur within the
+/// type, which is the case for arrays of non-constant size.
 static bool requires_renaming(const typet &type, const namespacet &ns)
 {
   if(type.id() == ID_array)
@@ -635,8 +638,12 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
     for(auto &component : components)
     {
       // be careful, or it might get cyclic
-      if(component.type().id() != ID_pointer)
-        return requires_renaming(component.type(), ns);
+      if(
+        component.type().id() != ID_pointer &&
+        requires_renaming(component.type(), ns))
+      {
+        return true;
+      }
     }
 
     return false;