1# 1 "files/1_3.c"
2# 1 "<built-in>"
3# 1 "<command-line>"
4# 1 "files/1_3.c"
5# 1 "./assert.h" 1
6
7void __blast_assert()
8{
9 ERROR: goto ERROR;
10}
11# 2 "files/1_3.c" 2
12# 1 "files/1_3.h" 1
13
14
15struct RR
16{
17 int state;
18};
19
20typedef struct RR rr;
21
22extern void *__VERIFIER_nondet_pointer();
23extern int __VERIFIER_nondet_int();
24
25typedef unsigned int size_t;
26extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
27
28# 3 "files/1_3.c" 2
29
30
31
32
33
34
35# 23 "files/1_3.c"
36rr * getrr()
37{
38 rr * r = (rr *)malloc(sizeof *r);
39 r -> state = 0;
40 return r;
41}
42
43rr * getPtr()
44{
45 rr * r = getrr();
46 r -> state = 1;
47 return r;
48}
49
50void freePtr(rr * ptr)
51{
52 ((ptr -> state == 1) ? (0) : __blast_assert ());
53 ptr -> state = 2;
54}
55
56int main()
57{
58 rr * ptr1 = 0;
59 ptr1 = getPtr();
60 freePtr(ptr1);
61
62 freePtr(ptr1);
63
64 return 0;
65}