File tree Expand file tree Collapse file tree 2 files changed +5
-12
lines changed Expand file tree Collapse file tree 2 files changed +5
-12
lines changed Original file line number Diff line number Diff line change 1
- #include <assert.h>
2
- #include <stdlib.h>
3
-
4
- #ifdef _MSC_VER
5
- # define _Static_assert (x , m ) static_assert(x, m)
6
- #endif
7
-
8
1
struct list ;
9
2
10
3
typedef struct list list_nodet;
@@ -22,11 +15,11 @@ int max_depth = 2;
22
15
list_nodet *build_node (int depth)
23
16
{
24
17
if (max_depth < depth)
25
- return ((list_nodet * )NULL );
18
+ return ((list_nodet *)0 );
26
19
else
27
20
{
28
- _Static_assert (sizeof (list_nodet ) == 16 , "" );
29
- list_nodet * result = malloc (16 );
21
+ __CPROVER_assert (sizeof (list_nodet) == 16 , " struct size is 16 bytes " );
22
+ list_nodet *result = __CPROVER_allocate (16 , 0 );
30
23
31
24
if (result)
32
25
{
@@ -53,6 +46,6 @@ int main()
53
46
{
54
47
i = i + 1 ;
55
48
}
56
- assert (i == 3 );
49
+ __CPROVER_assert (i == 3 , " i should be 3 " );
57
50
return 0 ;
58
51
}
Original file line number Diff line number Diff line change 1
1
CORE
2
- main.c
2
+ main.i
3
3
--no-malloc-may-fail --64 --unwind 4 --unwinding-assertions
4
4
^EXIT=0$
5
5
^SIGNAL=0$
You can’t perform that action at this time.
0 commit comments