diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel index 2ba432c93b3..28894cf26b0 100644 Binary files a/regression/ansi-c/arch_flags_mcpu_bad/object.intel and b/regression/ansi-c/arch_flags_mcpu_bad/object.intel differ diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm index 6593905c6b4..d86aa22b7bb 100644 Binary files a/regression/ansi-c/arch_flags_mcpu_good/object.arm and b/regression/ansi-c/arch_flags_mcpu_good/object.arm differ diff --git a/regression/ansi-c/arch_flags_mthumb_bad/object.intel b/regression/ansi-c/arch_flags_mthumb_bad/object.intel index d1b887e5bef..2696d85f1cb 100644 Binary files a/regression/ansi-c/arch_flags_mthumb_bad/object.intel and b/regression/ansi-c/arch_flags_mthumb_bad/object.intel differ diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm index 6a398a5058b..2f8bf4f810c 100644 Binary files a/regression/ansi-c/arch_flags_mthumb_good/object.arm and b/regression/ansi-c/arch_flags_mthumb_good/object.arm differ diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/regression/goto-harness/havoc-global-int-02/test.desc index 5617b1ecfcd..cb192a4c1e5 100644 --- a/regression/goto-harness/havoc-global-int-02/test.desc +++ b/regression/goto-harness/havoc-global-int-02/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:5 --havoc-variables y ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$ ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$ ^EXIT=10$ diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index a5c42d0bf42..ae824f2d256 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -951,7 +951,7 @@ exprt c_typecheck_baset::do_initializer_list( // make complete by setting array size size_t size=result.operands().size(); result.type().id(ID_array); - result.type().set(ID_size, from_integer(size, index_type())); + result.type().set(ID_size, from_integer(size, size_type())); } return result; diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index eb33205655a..b6ab7a512d6 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -559,7 +559,6 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) if(size.is_not_nil()) { typecheck_expr(size); - make_index_type(size); // The size need not be a constant! // We simplify it, for the benefit of array initialisation. @@ -587,10 +586,13 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) throw 0; } + implicit_typecast(tmp_size, size_type()); + simplify(tmp_size, *this); size=tmp_size; } else if(tmp_size.id()==ID_infinity) { + tmp_size.type() = size_type(); size=tmp_size; } else if(tmp_size.id()==ID_symbol && @@ -602,6 +604,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) // Of course we can modify a 'const' symbol, e.g., // using a pointer type cast. Interestingly, // at least gcc 4.2.1 makes the very same mistake! + implicit_typecast(tmp_size, size_type()); size=tmp_size; } else @@ -985,7 +988,7 @@ void c_typecheck_baset::typecheck_compound_body( // make it zero-length c_type.id(ID_array); - c_type.set(ID_size, from_integer(0, index_type())); + c_type.set(ID_size, from_integer(0, size_type())); } } } diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp index f04f955466f..9d479a79c50 100644 --- a/src/ansi-c/literals/convert_string_literal.cpp +++ b/src/ansi-c/literals/convert_string_literal.cpp @@ -132,7 +132,7 @@ exprt convert_string_literal(const std::string &src) result.set(ID_C_string_constant, true); result.type()=typet(ID_array); result.type().subtype()=subtype; - result.type().set(ID_size, from_integer(value.size(), index_type())); + result.type().set(ID_size, from_integer(value.size(), size_type())); result.operands().resize(value.size()); for(std::size_t i=0; i #include #include +#include #include @@ -758,10 +759,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) exprt &size=to_array_type(expr.type()).size(); typecheck_expr(size); - bool size_is_unsigned=(size.type().id()==ID_unsignedbv); - bitvector_typet integer_type( - size_is_unsigned ? ID_unsignedbv : ID_signedbv, config.ansi_c.int_width); - implicit_typecast(size, integer_type); + implicit_typecast(size, size_type()); + simplify(size, *this); expr.set(ID_statement, ID_cpp_new_array); diff --git a/src/util/string_constant.cpp b/src/util/string_constant.cpp index 15f61a0eeef..9e9bbcee9f9 100644 --- a/src/util/string_constant.cpp +++ b/src/util/string_constant.cpp @@ -20,7 +20,7 @@ string_constantt::string_constantt(const irep_idt &_value) void string_constantt::set_value(const irep_idt &value) { - exprt size_expr=from_integer(value.size()+1, index_type()); + exprt size_expr = from_integer(value.size() + 1, size_type()); type()=array_typet(char_type(), size_expr); set(ID_value, value); } @@ -33,7 +33,7 @@ array_exprt string_constantt::to_array_expr() const const typet &char_type = to_array_type(type()).subtype(); bool char_is_unsigned=char_type.id()==ID_unsignedbv; - exprt size=from_integer(string_size, index_type()); + exprt size = from_integer(string_size, size_type()); array_exprt dest({}, array_typet(char_type, size));