Skip to content

Commit c47678d

Browse files
committed
Add an integer value round trip (int -> void* -> int) test
1 parent 1aa34c6 commit c47678d

File tree

2 files changed

+24
-0
lines changed

2 files changed

+24
-0
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
int f(int x)
2+
{
3+
void *p = (void *)x;
4+
int r = (int)p;
5+
return r;
6+
}
7+
8+
int main()
9+
{
10+
int a = f(5);
11+
__CPROVER_assert(a == 5, "a == 5: expected success");
12+
__CPROVER_assert(a != 5, "a != 5: expected failure");
13+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
pointer_round_trip.c
3+
--trace
4+
\[main\.assertion\.1\] line \d+ a == 5: expected success: SUCCESS
5+
\[main\.assertion\.2\] line \d+ a != 5: expected failure: FAILURE
6+
^VERIFICATION FAILED$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
--
11+
This test is testing an integer value round trip (int -> pointer -> int) test.

0 commit comments

Comments
 (0)