1
2
3
4#line 1 "stateful_check.c"
5void __blast_assert(void)
6{
7
8 {
9 ERROR:
10 goto ERROR;
11}
12}
13#line 7 "stateful_check.c"
14int ldv_mutex = 1;
15#line 9 "stateful_check.c"
16int open_called = 0;
17#line 10
18int __VERIFIER_nondet_int(void) { int x; return x; }
19#line 12 "stateful_check.c"
20void mutex_lock(void)
21{
22
23 {
24#line 14
25 if (ldv_mutex == 1) {
26
27 } else {
28 {
29#line 14
30 __blast_assert();
31 }
32 }
33#line 15
34 ldv_mutex = 2;
35#line 16
36 return;
37}
38}
39#line 18 "stateful_check.c"
40void mutex_unlock(void)
41{
42
43 {
44#line 20
45 if (ldv_mutex == 2) {
46
47 } else {
48 {
49#line 20
50 __blast_assert();
51 }
52 }
53#line 21
54 ldv_mutex = 1;
55#line 22
56 return;
57}
58}
59#line 24 "stateful_check.c"
60void check_final_state(void)
61{
62
63 {
64#line 26
65 if (ldv_mutex == 1) {
66
67 } else {
68 {
69#line 26
70 __blast_assert();
71 }
72 }
73#line 27
74 return;
75}
76}
77#line 29 "stateful_check.c"
78static int misc_release(void)
79{
80
81 {
82#line 32
83 if (open_called) {
84 {
85#line 34
86 mutex_lock();
87#line 35
88 mutex_unlock();
89#line 36
90 open_called = 0;
91 }
92 } else {
93 {
94#line 39
95 mutex_lock();
96#line 40
97 mutex_lock();
98 }
99 }
100#line 42
101 return (0);
102}
103}
104#line 45 "stateful_check.c"
105static int misc_llseek(void)
106{
107
108 {
109#line 46
110 return (0);
111}
112}
113#line 49 "stateful_check.c"
114static int misc_read(void)
115{
116
117 {
118#line 50
119 return (0);
120}
121}
122#line 53 "stateful_check.c"
123static int misc_open(void)
124{ int tmp ;
125
126 {
127 {
128#line 55
129 tmp = __VERIFIER_nondet_int();
130 }
131#line 55
132 if (tmp) {
133#line 57
134 return (1);
135 } else {
136#line 59
137 open_called = 1;
138#line 60
139 return (0);
140 }
141}
142}
143#line 64 "stateful_check.c"
144static int my_init(void)
145{
146
147 {
148#line 67
149 open_called = 0;
150#line 68
151 return (0);
152}
153}
154#line 76
155extern int ( __VERIFIER_nondet_int)() ;
156#line 71 "stateful_check.c"
157void main(void)
158{ int ldv_s_misc_fops_file_operations ;
159 int tmp ;
160 int tmp___0 ;
161
162 {
163 {
164#line 72
165 ldv_s_misc_fops_file_operations = 0;
166#line 73
167 my_init();
168 }
169 {
170#line 74
171 while (1) {
172 while_0_continue: ;
173 {
174#line 74
175 tmp___0 = __VERIFIER_nondet_int();
176 }
177#line 74
178 if (tmp___0) {
179
180 } else {
181 goto while_0_break;
182 }
183 {
184#line 76
185 tmp = __VERIFIER_nondet_int();
186 }
187#line 78
188 if (tmp == 0) {
189 goto switch_1_0;
190 } else {
191#line 86
192 if (tmp == 1) {
193 goto switch_1_1;
194 } else {
195#line 94
196 if (tmp == 2) {
197 goto switch_1_2;
198 } else {
199#line 102
200 if (tmp == 3) {
201 goto switch_1_3;
202 } else {
203 {
204 goto switch_1_default;
205#line 76
206 if (0) {
207 switch_1_0:
208#line 79
209 if (ldv_s_misc_fops_file_operations == 0) {
210 {
211#line 80
212 misc_open();
213#line 81
214 ldv_s_misc_fops_file_operations = ldv_s_misc_fops_file_operations + 1;
215 }
216 } else {
217
218 }
219 goto switch_1_break;
220 switch_1_1:
221#line 87
222 if (ldv_s_misc_fops_file_operations == 1) {
223 {
224#line 88
225 misc_read();
226#line 89
227 ldv_s_misc_fops_file_operations = ldv_s_misc_fops_file_operations + 1;
228 }
229 } else {
230
231 }
232 goto switch_1_break;
233 switch_1_2:
234#line 95
235 if (ldv_s_misc_fops_file_operations == 2) {
236 {
237#line 96
238 misc_llseek();
239#line 97
240 ldv_s_misc_fops_file_operations = ldv_s_misc_fops_file_operations + 1;
241 }
242 } else {
243
244 }
245 goto switch_1_break;
246 switch_1_3:
247#line 103
248 if (ldv_s_misc_fops_file_operations == 3) {
249 {
250#line 104
251 misc_release();
252#line 105
253 ldv_s_misc_fops_file_operations = 0;
254 }
255 } else {
256
257 }
258 goto switch_1_break;
259 switch_1_default: ;
260 goto switch_1_break;
261 } else {
262 switch_1_break: ;
263 }
264 }
265 }
266 }
267 }
268 }
269 }
270 while_0_break: ;
271 }
272 {
273#line 113
274 check_final_state();
275 }
276#line 114
277 return;
278}
279}