Merge pull request #2367 from diffblue/fix-tests

Fix two cbmc tests

Author: kroening

regression/cbmc/Typecast2/main.c

@@ -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;
+}

regression/cbmc/Typecast2/main.i

@@ -1,5 +1,5 @@
 CORE
-main.c
+main.i
 --no-propagation --64
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Typecast2/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