diff --git a/regression/ansi-c/int128_and_bool1/main.c b/regression/ansi-c/int128_and_bool1/main.c new file mode 100644 index 00000000000..f050c46c24f --- /dev/null +++ b/regression/ansi-c/int128_and_bool1/main.c @@ -0,0 +1,6 @@ +int main(int argc, char *argv[]) +{ + unsigned __int128 z; + z = (unsigned __int128)argc; + z += (argc < 1); +} diff --git a/regression/ansi-c/int128_and_bool1/test.desc b/regression/ansi-c/int128_and_bool1/test.desc new file mode 100644 index 00000000000..d9d5bdfa642 --- /dev/null +++ b/regression/ansi-c/int128_and_bool1/test.desc @@ -0,0 +1,7 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^CONVERSION ERROR$ diff --git a/regression/cbmc/enum9/main.c b/regression/cbmc/enum9/main.c new file mode 100644 index 00000000000..2b9a61c3698 --- /dev/null +++ b/regression/cbmc/enum9/main.c @@ -0,0 +1,25 @@ +#include + +enum E +{ + V1 = 1, + V2 = 2 +}; + +struct B +{ + unsigned b : 2; +}; + +int main() +{ + unsigned __int128 int x; + __CPROVER_assume(x < (~(unsigned __int128)0) - 4); + + enum E e; + __CPROVER_assume(__CPROVER_enum_is_in_range(e)); + __CPROVER_assert(x + e > x, "long long plus enum"); + + struct B b; + __CPROVER_assert(x + b.b >= x, "long long plus bitfield"); +} diff --git a/regression/cbmc/enum9/test.desc b/regression/cbmc/enum9/test.desc new file mode 100644 index 00000000000..245d2eacb1b --- /dev/null +++ b/regression/cbmc/enum9/test.desc @@ -0,0 +1,9 @@ +CORE gcc-only +main.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^CONVERSION ERROR$ +^warning: ignoring diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 8092ac457c5..d6899f9261a 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -650,24 +650,8 @@ void c_typecastt::implicit_typecast_arithmetic( if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT) { - // get the biggest width of both - std::size_t width1 = to_bitvector_type(type1).get_width(); - std::size_t width2 = to_bitvector_type(type2).get_width(); - // produce type - typet result_type; - - if(width1==width2) - { - if(max_type==LARGE_SIGNED_INT) - result_type=signedbv_typet(width1); - else - result_type=unsignedbv_typet(width1); - } - else if(width1>width2) - result_type=type1; - else // width1