1
2
3
4#line 211 "/usr/lib/gcc/x86_64-pc-linux-gnu/4.5.3/include/stddef.h"
5typedef unsigned int size_t;
6#line 3 "files/1_3.h"
7struct RR {
8 int state ;
9};
10#line 8 "files/1_3.h"
11typedef struct RR rr;
12#line 471 "/usr/include/stdlib.h"
13extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
14#line 2 "./assert.h"
15void __blast_assert(void)
16{
17
18 {
19 ERROR:assert(0);
20#line 4
21 goto ERROR;
22}
23}
24#line 10 "files/1_3.h"
25extern void *__VERIFIER_nondet_pointer() ;
26#line 23 "files/1_3.c"
27rr *getrr(void)
28{ rr *r ;
29 void *tmp ;
30 unsigned int __cil_tmp3 ;
31
32 {
33 {
34#line 25
35 __cil_tmp3 = (unsigned int )4UL;
36#line 25
37 tmp = malloc(__cil_tmp3);
38#line 25
39 r = (rr *)tmp;
40#line 26
41 r->state = 0;
42 }
43#line 27
44 return (r);
45}
46}
47#line 30 "files/1_3.c"
48rr *getPtr(void)
49{ rr *r ;
50 rr *tmp ;
51
52 {
53 {
54#line 32
55 tmp = getrr();
56#line 32
57 r = tmp;
58#line 33
59 r->state = 1;
60 }
61#line 34
62 return (r);
63}
64}
65#line 37 "files/1_3.c"
66void freePtr(rr *ptr )
67{ int __cil_tmp2 ;
68
69 {
70 {
71#line 39
72 __cil_tmp2 = ptr->state;
73#line 39
74 if (__cil_tmp2 == 1) {
75
76 } else {
77 {
78#line 39
79 __blast_assert();
80 }
81 }
82 }
83#line 40
84 ptr->state = 2;
85#line 41
86 return;
87}
88}
89#line 43 "files/1_3.c"
90int main(void)
91{ rr *ptr1 ;
92
93 {
94 {
95#line 45
96 ptr1 = (rr *)0;
97#line 46
98 ptr1 = getPtr();
99#line 47
100 freePtr(ptr1);
101#line 49
102 freePtr(ptr1);
103 }
104#line 51
105 return (0);
106}
107}