diff --git a/regression/cbmc/Typecast2/main.c b/regression/cbmc/Typecast2/main.c deleted file mode 100644 index 59ea8cb72d0..00000000000 --- a/regression/cbmc/Typecast2/main.c +++ /dev/null @@ -1,8 +0,0 @@ -#include - -int main() -{ - unsigned int i=2; - assert(0l==(signed long int)(i - (unsigned int)2)); - return 0; -} diff --git a/regression/cbmc/Typecast2/main.i b/regression/cbmc/Typecast2/main.i new file mode 100644 index 00000000000..8dc3ecf5e6a --- /dev/null +++ b/regression/cbmc/Typecast2/main.i @@ -0,0 +1,7 @@ +int main() +{ + unsigned int i=2; + __CPROVER_assert(0l==(signed long int)(i - (unsigned int)2), + "difference of cast"); + return 0; +} diff --git a/regression/cbmc/Typecast2/test.desc b/regression/cbmc/Typecast2/test.desc index 1af9f7644e7..cdbe617e1f6 100644 --- a/regression/cbmc/Typecast2/test.desc +++ b/regression/cbmc/Typecast2/test.desc @@ -1,5 +1,5 @@ CORE -main.c +main.i --no-propagation --64 ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc index efec610daee..eed958c1397 100644 --- a/regression/cbmc/bounds_check1/test.desc +++ b/regression/cbmc/bounds_check1/test.desc @@ -3,12 +3,12 @@ main.c --bounds-check --pointer-check ^EXIT=10$ ^SIGNAL=0$ -\[\(signed long( long)? int\)i2\]: FAILURE -dest\[\(signed long( long)? int\)j2\]: FAILURE -payload\[\(signed long( long)? int\)[kl]2\]: FAILURE +\[\(.*\)i2\]: FAILURE +dest\[\(.*\)j2\]: FAILURE +payload\[\(.*\)[kl]2\]: FAILURE \*\* 10 of 72 failed -- ^warning: ignoring -\[\(signed long( long)? int\)i\]: FAILURE -dest\[\(signed long( long)? int\)j\]: FAILURE -payload\[\(signed long( long)? int\)[kl]\]: FAILURE +\[\(.*\)i\]: FAILURE +dest\[\(.*\)j\]: FAILURE +payload\[\(.*\)[kl]\]: FAILURE