Skip to content

Commit 4de4538

Browse files
author
Daniel Kroening
committed
switch regression/cbmc/Typecast2 to preprocessed code
This avoids the need for a cross-compiler to 64 bit when run on a 32-bit system.
1 parent 52a8afc commit 4de4538

File tree

3 files changed

+8
-9
lines changed

3 files changed

+8
-9
lines changed

regression/cbmc/Typecast2/main.c

Lines changed: 0 additions & 8 deletions
This file was deleted.

regression/cbmc/Typecast2/main.i

Lines changed: 7 additions & 0 deletions
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+
}

regression/cbmc/Typecast2/test.desc

Lines changed: 1 addition & 1 deletion
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$

0 commit comments

Comments
 (0)