diff --git a/regression/cbmc/vla1/main.c b/regression/cbmc/vla1/main.c deleted file mode 100644 index 0e97523b6fc..00000000000 --- a/regression/cbmc/vla1/main.c +++ /dev/null @@ -1,30 +0,0 @@ -#include - -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; -} diff --git a/regression/cbmc/vla1/program-only.desc b/regression/cbmc/vla1/program-only.desc deleted file mode 100644 index 35f671bf4a5..00000000000 --- a/regression/cbmc/vla1/program-only.desc +++ /dev/null @@ -1,12 +0,0 @@ -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. diff --git a/regression/cbmc/vla1/test.desc b/regression/cbmc/vla1/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/cbmc/vla1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 036981b126d..f0b4e24b11c 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -609,25 +608,43 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) throw 0; } - 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); + // 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(); new_symbol.type.set(ID_C_constant, true); - new_symbol.value = typecast_exprt::conditional_cast(size, size_type()); + new_symbol.value = size; + new_symbol.location = size_source_location; + new_symbol.mode = mode; + + symbol_table.add(new_symbol); // produce the code that declares and initializes the symbol - symbol_exprt symbol_expr = new_symbol.symbol_expr(); + symbol_exprt symbol_expr; + symbol_expr.set_identifier(temp_identifier); + symbol_expr.type() = new_symbol.type; code_declt declaration(symbol_expr); declaration.add_source_location() = size_source_location; code_assignt assignment; assignment.lhs()=symbol_expr; - assignment.rhs() = new_symbol.value; + assignment.rhs() = size; assignment.add_source_location() = size_source_location; // store the code diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 0b0fc90e74f..44b3b58e4ca 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -618,70 +618,12 @@ 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) - { - const auto &array_type = to_array_type(type); - return requires_renaming(array_type.subtype(), ns) || - !array_type.size().is_constant(); - } - else if( - type.id() == ID_struct || type.id() == ID_union || type.id() == ID_class) - { - const struct_union_typet &s_u_type = to_struct_union_type(type); - const struct_union_typet::componentst &components = s_u_type.components(); - - for(auto &component : components) - { - // be careful, or it might get cyclic - if( - component.type().id() != ID_pointer && - requires_renaming(component.type(), ns)) - { - return true; - } - } - - return false; - } - else if(type.id() == ID_pointer) - { - return requires_renaming(to_pointer_type(type).subtype(), ns); - } - else if(type.id() == ID_symbol_type) - { - const symbolt &symbol = ns.lookup(to_symbol_type(type)); - return requires_renaming(symbol.type, ns); - } - else if(type.id() == ID_union_tag) - { - const symbolt &symbol = ns.lookup(to_union_tag_type(type)); - return requires_renaming(symbol.type, ns); - } - else if(type.id() == ID_struct_tag) - { - const symbolt &symbol = ns.lookup(to_struct_tag_type(type)); - return requires_renaming(symbol.type, ns); - } - - return false; -} - void goto_symex_statet::rename( typet &type, const irep_idt &l1_identifier, const namespacet &ns, levelt level) { - // check whether there are symbol expressions in the type; if not, there - // is no need to expand the struct/union tags in the type - if(!requires_renaming(type, ns)) - return; // no action - // rename all the symbols with their last known value // to the given level