1extern int __VERIFIER_nondet_int();
2void error(void)
3{
4
5 {
6 goto ERROR;
7 ERROR: ;
8 return;
9}
10}
11
12int q_buf_0 ;
13int q_free ;
14int q_read_ev ;
15int q_write_ev ;
16int p_num_write ;
17int p_last_write ;
18int p_dw_st ;
19int p_dw_pc ;
20int p_dw_i ;
21int c_num_read ;
22int c_last_read ;
23int c_dr_st ;
24int c_dr_pc ;
25int c_dr_i ;
26int is_do_write_p_triggered(void)
27{ int __retres1 ;
28
29 {
30 if ((int )p_dw_pc == 1) {
31 if ((int )q_read_ev == 1) {
32 __retres1 = 1;
33 goto return_label;
34 } else {
35
36 }
37 } else {
38
39 }
40 __retres1 = 0;
41 return_label:
42 return (__retres1);
43}
44}
45int is_do_read_c_triggered(void)
46{ int __retres1 ;
47
48 {
49 if ((int )c_dr_pc == 1) {
50 if ((int )q_write_ev == 1) {
51 __retres1 = 1;
52 goto return_label;
53 } else {
54
55 }
56 } else {
57
58 }
59 __retres1 = 0;
60 return_label:
61 return (__retres1);
62}
63}
64void immediate_notify_threads(void)
65{ int tmp ;
66 int tmp___0 ;
67
68 {
69 {
70 tmp = is_do_write_p_triggered();
71 }
72 if (tmp) {
73 p_dw_st = 0;
74 } else {
75
76 }
77 {
78 tmp___0 = is_do_read_c_triggered();
79 }
80 if (tmp___0) {
81 c_dr_st = 0;
82 } else {
83
84 }
85
86 return;
87}
88}
89void do_write_p(void)
90{
91
92
93
94 {
95 if ((int )p_dw_pc == 0) {
96 goto DW_ENTRY;
97 } else {
98 if ((int )p_dw_pc == 1) {
99 goto DW_WAIT_READ;
100 } else {
101
102 }
103 }
104 DW_ENTRY:
105 {
106 while (1) {
107 while_0_continue: ;
108 if ((int )q_free == 0) {
109 p_dw_st = 2;
110 p_dw_pc = 1;
111
112 goto return_label;
113 DW_WAIT_READ: ;
114 } else {
115
116 }
117 {
118 q_buf_0 = __VERIFIER_nondet_int();
119 p_last_write = q_buf_0;
120 p_num_write += 1;
121 q_free = 0;
122 q_write_ev = 1;
123 immediate_notify_threads();
124 q_write_ev = 2;
125 }
126 }
127 while_0_break: ;
128 }
129 return_label:
130 return;
131}
132}
133static int a_t ;
134void do_read_c(void)
135{ int a ;
136
137 {
138 if ((int )c_dr_pc == 0) {
139 goto DR_ENTRY;
140 } else {
141 if ((int )c_dr_pc == 1) {
142 goto DR_WAIT_WRITE;
143 } else {
144
145 }
146 }
147 DR_ENTRY:
148 {
149 while (1) {
150 while_1_continue: ;
151 if ((int )q_free == 1) {
152 c_dr_st = 2;
153 c_dr_pc = 1;
154 a_t = a;
155
156 goto return_label;
157 DR_WAIT_WRITE:
158 a = a_t;
159 } else {
160
161 }
162 {
163 a = q_buf_0;
164 c_last_read = a;
165 c_num_read += 1;
166 q_free = 1;
167 q_read_ev = 1;
168 immediate_notify_threads();
169 q_read_ev = 2;
170 }
171 if (p_last_write == c_last_read) {
172 if (p_num_write == c_num_read) {
173
174 } else {
175 {
176 error();
177 }
178 }
179 } else {
180 {
181 error();
182 }
183 }
184 }
185 while_1_break: ;
186 }
187 return_label:
188 return;
189}
190}
191void init_threads(void)
192{
193
194 {
195 if ((int )p_dw_i == 1) {
196 p_dw_st = 0;
197 } else {
198 p_dw_st = 2;
199 }
200 if ((int )c_dr_i == 1) {
201 c_dr_st = 0;
202 } else {
203 c_dr_st = 2;
204 }
205
206 return;
207}
208}
209int exists_runnable_thread(void)
210{ int __retres1 ;
211
212 {
213 if ((int )p_dw_st == 0) {
214 __retres1 = 1;
215 goto return_label;
216 } else {
217 if ((int )c_dr_st == 0) {
218 __retres1 = 1;
219 goto return_label;
220 } else {
221
222 }
223 }
224 __retres1 = 0;
225 return_label:
226 return (__retres1);
227}
228}
229void eval(void)
230{ int tmp ;
231 int tmp___0 ;
232 int tmp___1 ;
233
234
235 {
236 {
237 while (1) {
238 while_2_continue: ;
239 {
240 tmp___1 = exists_runnable_thread();
241 }
242 if (tmp___1) {
243
244 } else {
245 goto while_2_break;
246 }
247 if ((int )p_dw_st == 0) {
248 {
249 tmp = __VERIFIER_nondet_int();
250 }
251 if (tmp) {
252 {
253 p_dw_st = 1;
254 do_write_p();
255 }
256 } else {
257
258 }
259 } else {
260
261 }
262 if ((int )c_dr_st == 0) {
263 {
264 tmp___0 = __VERIFIER_nondet_int();
265 }
266 if (tmp___0) {
267 {
268 c_dr_st = 1;
269 do_read_c();
270 }
271 } else {
272
273 }
274 } else {
275
276 }
277 }
278 while_2_break: ;
279 }
280
281 return;
282}
283}
284int stop_simulation(void)
285{ int tmp ;
286 int __retres2 ;
287
288 {
289 {
290 tmp = exists_runnable_thread();
291 }
292 if (tmp) {
293 __retres2 = 0;
294 goto return_label;
295 } else {
296
297 }
298 __retres2 = 1;
299 return_label:
300 return (__retres2);
301}
302}
303void start_simulation(void)
304{ int kernel_st ;
305 int tmp ;
306
307 {
308 {
309 kernel_st = 0;
310 init_threads();
311 }
312 {
313 while (1) {
314 while_3_continue: ;
315 {
316 kernel_st = 1;
317 eval();
318 tmp = stop_simulation();
319 }
320 if (tmp) {
321 goto while_3_break;
322 } else {
323
324 }
325 }
326 while_3_break: ;
327 }
328
329 return;
330}
331}
332void init_model(void)
333{
334
335 {
336 q_free = 1;
337 q_write_ev = 2;
338 q_read_ev = q_write_ev;
339 p_num_write = 0;
340 p_dw_pc = 0;
341 p_dw_i = 1;
342 c_num_read = 0;
343 c_dr_pc = 0;
344 c_dr_i = 1;
345
346 return;
347}
348}
349int main(void)
350{ int __retres1 ;
351
352 {
353 {
354 init_model();
355 start_simulation();
356 }
357 __retres1 = 0;
358 return (__retres1);
359}
360}