Skip to content

Commit 6882da6

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#2367 from diffblue/fix-tests
Fix two cbmc tests
2 parents 52a8afc + bcc3bef commit 6882da6

File tree

4 files changed

+14
-15
lines changed

4 files changed

+14
-15
lines changed

Diff for: regression/cbmc/Typecast2/main.c

-8
This file was deleted.

Diff for: regression/cbmc/Typecast2/main.i

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
int main()
2+
{
3+
unsigned int i=2;
4+
__CPROVER_assert(0l==(signed long int)(i - (unsigned int)2),
5+
"difference of cast");
6+
return 0;
7+
}

Diff for: regression/cbmc/Typecast2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
2-
main.c
2+
main.i
33
--no-propagation --64
44
^EXIT=0$
55
^SIGNAL=0$

Diff for: regression/cbmc/bounds_check1/test.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ main.c
33
--bounds-check --pointer-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[\(signed long( long)? int\)i2\]: FAILURE
7-
dest\[\(signed long( long)? int\)j2\]: FAILURE
8-
payload\[\(signed long( long)? int\)[kl]2\]: FAILURE
6+
\[\(.*\)i2\]: FAILURE
7+
dest\[\(.*\)j2\]: FAILURE
8+
payload\[\(.*\)[kl]2\]: FAILURE
99
\*\* 10 of 72 failed
1010
--
1111
^warning: ignoring
12-
\[\(signed long( long)? int\)i\]: FAILURE
13-
dest\[\(signed long( long)? int\)j\]: FAILURE
14-
payload\[\(signed long( long)? int\)[kl]\]: FAILURE
12+
\[\(.*\)i\]: FAILURE
13+
dest\[\(.*\)j\]: FAILURE
14+
payload\[\(.*\)[kl]\]: FAILURE

0 commit comments

Comments
 (0)