Showing error 241

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/token_ring.01.BUG.cil.c
Line in file: 8
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

  1/* Generated by CIL v. 1.3.6 */
  2/* print_CIL_Input is true */
  3
  4void error(void) 
  5{ 
  6
  7  {
  8  ERROR: ;
  9  goto ERROR;
 10  return;
 11}
 12}
 13int m_pc  =    0;
 14int t1_pc  =    0;
 15int m_st  ;
 16int t1_st  ;
 17int m_i  ;
 18int t1_i  ;
 19int M_E  =    2;
 20int T1_E  =    2;
 21int E_M  =    2;
 22int E_1  =    2;
 23int is_master_triggered(void) ;
 24int is_transmit1_triggered(void) ;
 25void immediate_notify(void) ;
 26int token  ;
 27int __VERIFIER_nondet_int()  ;
 28int local  ;
 29void master(void) 
 30{ 
 31int tmp_var ;
 32  {
 33  if (m_pc == 0) {
 34    goto M_ENTRY;
 35  } else {
 36    if (m_pc == 1) {
 37      goto M_WAIT;
 38    } else {
 39
 40    }
 41  }
 42  M_ENTRY: ;
 43  {
 44  while (1) {
 45    while_0_continue: /* CIL Label */ ;
 46    {
 47    token = __VERIFIER_nondet_int();
 48    local = token;
 49    E_1 = 1;
 50    immediate_notify();
 51    E_1 = 2;
 52    m_pc = 1;
 53    m_st = 2;
 54    }
 55
 56    goto return_label;
 57    M_WAIT: ;
 58    if (token != local + 1) {
 59      {
 60      error();
 61      }
 62    } else {
 63       if(tmp_var <= 5){
 64           if(tmp_var >= 5){
 65             
 66           }
 67        }
 68
 69        if(tmp_var <= 5){
 70           if(tmp_var >= 5){
 71             if(tmp_var == 5){
 72             error();
 73             }
 74          }
 75        }
 76    }
 77  }
 78  while_0_break: /* CIL Label */ ;
 79  }
 80
 81  return_label: /* CIL Label */ 
 82  return;
 83}
 84}
 85void transmit1(void) 
 86{ 
 87
 88  {
 89  if (t1_pc == 0) {
 90    goto T1_ENTRY;
 91  } else {
 92    if (t1_pc == 1) {
 93      goto T1_WAIT;
 94    } else {
 95
 96    }
 97  }
 98  T1_ENTRY: ;
 99  {
100  while (1) {
101    while_1_continue: /* CIL Label */ ;
102    t1_pc = 1;
103    t1_st = 2;
104
105    goto return_label;
106    T1_WAIT: 
107    {
108    token += 1;
109    E_M = 1;
110    immediate_notify();
111    E_M = 2;
112    }
113  }
114  while_1_break: /* CIL Label */ ;
115  }
116
117  return_label: /* CIL Label */ 
118  return;
119}
120}
121int is_master_triggered(void) 
122{ int __retres1 ;
123
124  {
125  if (m_pc == 1) {
126    if (E_M == 1) {
127      __retres1 = 1;
128      goto return_label;
129    } else {
130
131    }
132  } else {
133
134  }
135  __retres1 = 0;
136  return_label: /* CIL Label */ 
137  return (__retres1);
138}
139}
140int is_transmit1_triggered(void) 
141{ int __retres1 ;
142
143  {
144  if (t1_pc == 1) {
145    if (E_1 == 1) {
146      __retres1 = 1;
147      goto return_label;
148    } else {
149
150    }
151  } else {
152
153  }
154  __retres1 = 0;
155  return_label: /* CIL Label */ 
156  return (__retres1);
157}
158}
159void update_channels(void) 
160{ 
161
162  {
163
164  return;
165}
166}
167void init_threads(void) 
168{ 
169
170  {
171  if (m_i == 1) {
172    m_st = 0;
173  } else {
174    m_st = 2;
175  }
176  if (t1_i == 1) {
177    t1_st = 0;
178  } else {
179    t1_st = 2;
180  }
181
182  return;
183}
184}
185int exists_runnable_thread(void) 
186{ int __retres1 ;
187
188  {
189  if (m_st == 0) {
190    __retres1 = 1;
191    goto return_label;
192  } else {
193    if (t1_st == 0) {
194      __retres1 = 1;
195      goto return_label;
196    } else {
197
198    }
199  }
200  __retres1 = 0;
201  return_label: /* CIL Label */ 
202  return (__retres1);
203}
204}
205void eval(void) 
206{// int __VERIFIER_nondet_int() ;
207  int tmp ;
208
209  {
210  {
211  while (1) {
212    while_2_continue: /* CIL Label */ ;
213    {
214    tmp = exists_runnable_thread();
215    }
216    if (tmp) {
217
218    } else {
219      goto while_2_break;
220    }
221    if (m_st == 0) {
222      int tmp_ndt_1;
223      tmp_ndt_1 = __VERIFIER_nondet_int();
224      if (tmp_ndt_1) {
225        {
226        m_st = 1;
227        master();
228        }
229      } else {
230
231      }
232    } else {
233
234    }
235    if (t1_st == 0) {
236      int tmp_ndt_2;
237      tmp_ndt_2 = __VERIFIER_nondet_int();
238      if (tmp_ndt_2) {
239        {
240        t1_st = 1;
241        transmit1();
242        }
243      } else {
244
245      }
246    } else {
247
248    }
249  }
250  while_2_break: /* CIL Label */ ;
251  }
252
253  return;
254}
255}
256void fire_delta_events(void) 
257{ 
258
259  {
260  if (M_E == 0) {
261    M_E = 1;
262  } else {
263
264  }
265  if (T1_E == 0) {
266    T1_E = 1;
267  } else {
268
269  }
270  if (E_M == 0) {
271    E_M = 1;
272  } else {
273
274  }
275  if (E_1 == 0) {
276    E_1 = 1;
277  } else {
278
279  }
280
281  return;
282}
283}
284void reset_delta_events(void) 
285{ 
286
287  {
288  if (M_E == 1) {
289    M_E = 2;
290  } else {
291
292  }
293  if (T1_E == 1) {
294    T1_E = 2;
295  } else {
296
297  }
298  if (E_M == 1) {
299    E_M = 2;
300  } else {
301
302  }
303  if (E_1 == 1) {
304    E_1 = 2;
305  } else {
306
307  }
308
309  return;
310}
311}
312void activate_threads(void) 
313{ int tmp ;
314  int tmp___0 ;
315
316  {
317  {
318  tmp = is_master_triggered();
319  }
320  if (tmp) {
321    m_st = 0;
322  } else {
323
324  }
325  {
326  tmp___0 = is_transmit1_triggered();
327  }
328  if (tmp___0) {
329    t1_st = 0;
330  } else {
331
332  }
333
334  return;
335}
336}
337void immediate_notify(void) 
338{ 
339
340  {
341  {
342  activate_threads();
343  }
344
345  return;
346}
347}
348void fire_time_events(void) 
349{ 
350
351  {
352  M_E = 1;
353
354  return;
355}
356}
357void reset_time_events(void) 
358{ 
359
360  {
361  if (M_E == 1) {
362    M_E = 2;
363  } else {
364
365  }
366  if (T1_E == 1) {
367    T1_E = 2;
368  } else {
369
370  }
371  if (E_M == 1) {
372    E_M = 2;
373  } else {
374
375  }
376  if (E_1 == 1) {
377    E_1 = 2;
378  } else {
379
380  }
381
382  return;
383}
384}
385void init_model(void) 
386{ 
387
388  {
389  m_i = 1;
390  t1_i = 1;
391
392  return;
393}
394}
395int stop_simulation(void) 
396{ int tmp ;
397  int __retres2 ;
398
399  {
400  {
401  tmp = exists_runnable_thread();
402  }
403  if (tmp) {
404    __retres2 = 0;
405    goto return_label;
406  } else {
407
408  }
409  __retres2 = 1;
410  return_label: /* CIL Label */ 
411  return (__retres2);
412}
413}
414void start_simulation(void) 
415{ int kernel_st ;
416  int tmp ;
417  int tmp___0 ;
418
419  {
420  {
421  kernel_st = 0;
422  update_channels();
423  init_threads();
424  fire_delta_events();
425  activate_threads();
426  reset_delta_events();
427  }
428  {
429  while (1) {
430    while_3_continue: /* CIL Label */ ;
431    {
432    kernel_st = 1;
433    eval();
434    }
435    {
436    kernel_st = 2;
437    update_channels();
438    }
439    {
440    kernel_st = 3;
441    fire_delta_events();
442    activate_threads();
443    reset_delta_events();
444    }
445    {
446    tmp = exists_runnable_thread();
447    }
448    if (tmp == 0) {
449      {
450      kernel_st = 4;
451      fire_time_events();
452      activate_threads();
453      reset_time_events();
454      }
455    } else {
456
457    }
458    {
459    tmp___0 = stop_simulation();
460    }
461    if (tmp___0) {
462      goto while_3_break;
463    } else {
464
465    }
466  }
467  while_3_break: /* CIL Label */ ;
468  }
469
470  return;
471}
472}
473int main(void) 
474{ int __retres1 ;
475
476  {
477  {
478  init_model();
479  start_simulation();
480  }
481  __retres1 = 0;
482  return (__retres1);
483}
484}
↑