diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel index 2ba432c93b3..12933c39767 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..5a6ae1e2c48 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..7cb7e011e3f 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..d7dd5b25c97 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/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 804adf9db67..7ede86031cc 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -113,7 +113,8 @@ static std::string architecture_string(const std::string &value, const char *s) template static std::string architecture_string(T value, const char *s) { - return std::string("const int " CPROVER_PREFIX "architecture_") + + return std::string("const " CPROVER_PREFIX "integer " CPROVER_PREFIX + "architecture_") + std::string(s) + "=" + std::to_string(value) + ";\n"; } diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index 8817ed686aa..b69caf0a58b 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -1451,12 +1451,36 @@ bool cpp_typecheckt::implicit_conversion_sequence( { rank=backup_rank; if(!user_defined_conversion_sequence(e, type, new_expr, rank)) + { + if( + type.id() == ID_integer && + (expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)) + { + // This is a nonstandard implicit conversion, from + // bit-vectors to unbounded integers. + rank = 0; + new_expr = typecast_exprt(expr, type); + return true; + } + else if( + (type.id() == ID_signedbv || type.id() == ID_unsignedbv) && + expr.type().id() == ID_integer) + { + // This is a nonstandard implicit conversion, from + // unbounded integers to bit-vectors. + rank = 0; + new_expr = typecast_exprt(expr, type); + return true; + } + + // no conversion return false; + } - #if 0 +#if 0 simplify_exprt simplify(*this); simplify.simplify(new_expr); - #endif +#endif } return true; diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index 0ec59432b39..d55c39f7b10 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu /// C++ Language Type Checking #include +#include +#include #include #include @@ -69,6 +71,19 @@ void cpp_typecheckt::typecheck_type(typet &type) if(type.get_bool(ID_C_constant)) qualifiers.is_constant = true; + // CPROVER extensions + irep_idt typedef_identifier = type.get(ID_C_typedef); + if(typedef_identifier == CPROVER_PREFIX "rational") + { + type = rational_typet(); + type.add_source_location() = symbol_expr.source_location(); + } + else if(typedef_identifier == CPROVER_PREFIX "integer") + { + type = integer_typet(); + type.add_source_location() = symbol_expr.source_location(); + } + qualifiers.write(type); } else if(type.id()==ID_struct || diff --git a/src/util/interval.cpp b/src/util/interval.cpp index dace8934b85..2d87be0bcb7 100644 --- a/src/util/interval.cpp +++ b/src/util/interval.cpp @@ -1094,7 +1094,7 @@ bool constant_interval_exprt::is_numeric( bool constant_interval_exprt::is_int(const typet &type) { - return (is_signed(type) || is_unsigned(type)); + return is_signed(type) || is_unsigned(type) || type.id() == ID_integer; } bool constant_interval_exprt::is_float(const typet &src)