1extern int __VERIFIER_nondet_int();
2
3void error(void)
4{
5
6 {
7 goto ERROR;
8 ERROR: ;
9 return;
10}
11}
12
13int q_buf_0 ;
14int q_free ;
15int q_read_ev ;
16int q_write_ev ;
17int p_num_write ;
18int p_last_write ;
19int p_dw_st ;
20int p_dw_pc ;
21int p_dw_i ;
22int c_num_read ;
23int c_last_read ;
24int c_dr_st ;
25int c_dr_pc ;
26int c_dr_i ;
27int is_do_write_p_triggered(void)
28{ int __retres1 ;
29
30 {
31 if ((int )p_dw_pc == 1) {
32 if ((int )q_read_ev == 1) {
33 __retres1 = 1;
34 goto return_label;
35 } else {
36
37 }
38 } else {
39
40 }
41 __retres1 = 0;
42 return_label:
43 return (__retres1);
44}
45}
46int is_do_read_c_triggered(void)
47{ int __retres1 ;
48
49 {
50 if ((int )c_dr_pc == 1) {
51 if ((int )q_write_ev == 1) {
52 __retres1 = 1;
53 goto return_label;
54 } else {
55
56 }
57 } else {
58
59 }
60 __retres1 = 0;
61 return_label:
62 return (__retres1);
63}
64}
65void immediate_notify_threads(void)
66{ int tmp ;
67 int tmp___0 ;
68
69 {
70 {
71 tmp = is_do_write_p_triggered();
72 }
73 if (tmp) {
74 p_dw_st = 0;
75 } else {
76
77 }
78 {
79 tmp___0 = is_do_read_c_triggered();
80 }
81 if (tmp___0) {
82 c_dr_st = 0;
83 } else {
84
85 }
86
87 return;
88}
89}
90void do_write_p(void)
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 while (1) {
237 while_2_continue: ;
238 {
239 tmp___1 = exists_runnable_thread();
240 }
241 if (tmp___1) {
242
243 } else {
244 goto while_2_break;
245 }
246 if ((int )p_dw_st == 0) {
247 {
248 tmp = __VERIFIER_nondet_int();
249 }
250 if (tmp) {
251 {
252 p_dw_st = 1;
253 do_write_p();
254 }
255 } else {
256
257 }
258 } else {
259
260 }
261 if ((int )c_dr_st == 0) {
262 {
263 tmp___0 = __VERIFIER_nondet_int();
264 }
265 if (tmp___0) {
266 {
267 c_dr_st = 1;
268 do_read_c();
269 }
270 } else {
271
272 }
273 } else {
274
275 }
276 }
277 while_2_break: ;
278 }
279
280 return;
281}
282}
283int stop_simulation(void)
284{ int tmp ;
285 int __retres2 ;
286
287 {
288 {
289 tmp = exists_runnable_thread();
290 }
291 if (tmp) {
292 __retres2 = 0;
293 goto return_label;
294 } else {
295
296 }
297 __retres2 = 1;
298 return_label:
299 return (__retres2);
300}
301}
302void start_simulation(void)
303{ int kernel_st ;
304 int tmp ;
305
306 {
307 {
308 kernel_st = 0;
309 init_threads();
310 }
311 {
312 while (1) {
313 while_3_continue: ;
314 {
315 kernel_st = 1;
316 eval();
317 tmp = stop_simulation();
318 }
319 if (tmp) {
320 goto while_3_break;
321 } else {
322
323 }
324 }
325 while_3_break: ;
326 }
327
328 return;
329}
330}
331void init_model(void)
332{
333
334 {
335 q_free = 1;
336 q_write_ev = 2;
337 q_read_ev = q_write_ev;
338 p_num_write = 0;
339 p_dw_pc = 0;
340 p_dw_i = 1;
341 c_num_read = 0;
342 c_dr_pc = 0;
343 c_dr_i = 1;
344
345 return;
346}
347}
348int main(void)
349{ int __retres1 ;
350
351 {
352 {
353 init_model();
354 start_simulation();
355 }
356 __retres1 = 0;
357 return (__retres1);
358}
359}