Showing error 2294

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.02_safe.cil.c
Line in file: 8
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 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 t2_pc  =    0;
 16int m_st  ;
 17int t1_st  ;
 18int t2_st  ;
 19int m_i  ;
 20int t1_i  ;
 21int t2_i  ;
 22int M_E  =    2;
 23int T1_E  =    2;
 24int T2_E  =    2;
 25int E_M  =    2;
 26int E_1  =    2;
 27int E_2  =    2;
 28int is_master_triggered(void) ;
 29int is_transmit1_triggered(void) ;
 30int is_transmit2_triggered(void) ;
 31void immediate_notify(void) ;
 32int token  ;
 33int __VERIFIER_nondet_int()  ;
 34int local  ;
 35void master(void) 
 36{ 
 37
 38  {
 39  if (m_pc == 0) {
 40    goto M_ENTRY;
 41  } else {
 42    if (m_pc == 1) {
 43      goto M_WAIT;
 44    } else {
 45
 46    }
 47  }
 48  M_ENTRY: ;
 49  {
 50  while (1) {
 51    while_0_continue: /* CIL Label */ ;
 52    {
 53    token = __VERIFIER_nondet_int();
 54    local = token;
 55    E_1 = 1;
 56    immediate_notify();
 57    E_1 = 2;
 58    m_pc = 1;
 59    m_st = 2;
 60    }
 61
 62    goto return_label;
 63    M_WAIT: ;
 64    if (token != local + 2) {
 65      {
 66      error();
 67      }
 68    } else {
 69
 70    }
 71  }
 72  while_0_break: /* CIL Label */ ;
 73  }
 74
 75  return_label: /* CIL Label */ 
 76  return;
 77}
 78}
 79void transmit1(void) 
 80{ 
 81
 82  {
 83  if (t1_pc == 0) {
 84    goto T1_ENTRY;
 85  } else {
 86    if (t1_pc == 1) {
 87      goto T1_WAIT;
 88    } else {
 89
 90    }
 91  }
 92  T1_ENTRY: ;
 93  {
 94  while (1) {
 95    while_1_continue: /* CIL Label */ ;
 96    t1_pc = 1;
 97    t1_st = 2;
 98
 99    goto return_label;
100    T1_WAIT: 
101    {
102    token += 1;
103    E_2 = 1;
104    immediate_notify();
105    E_2 = 2;
106    }
107  }
108  while_1_break: /* CIL Label */ ;
109  }
110
111  return_label: /* CIL Label */ 
112  return;
113}
114}
115void transmit2(void) 
116{ 
117
118  {
119  if (t2_pc == 0) {
120    goto T2_ENTRY;
121  } else {
122    if (t2_pc == 1) {
123      goto T2_WAIT;
124    } else {
125
126    }
127  }
128  T2_ENTRY: ;
129  {
130  while (1) {
131    while_2_continue: /* CIL Label */ ;
132    t2_pc = 1;
133    t2_st = 2;
134
135    goto return_label;
136    T2_WAIT: 
137    {
138    token += 1;
139    E_M = 1;
140    immediate_notify();
141    E_M = 2;
142    }
143  }
144  while_2_break: /* CIL Label */ ;
145  }
146
147  return_label: /* CIL Label */ 
148  return;
149}
150}
151int is_master_triggered(void) 
152{ int __retres1 ;
153
154  {
155  if (m_pc == 1) {
156    if (E_M == 1) {
157      __retres1 = 1;
158      goto return_label;
159    } else {
160
161    }
162  } else {
163
164  }
165  __retres1 = 0;
166  return_label: /* CIL Label */ 
167  return (__retres1);
168}
169}
170int is_transmit1_triggered(void) 
171{ int __retres1 ;
172
173  {
174  if (t1_pc == 1) {
175    if (E_1 == 1) {
176      __retres1 = 1;
177      goto return_label;
178    } else {
179
180    }
181  } else {
182
183  }
184  __retres1 = 0;
185  return_label: /* CIL Label */ 
186  return (__retres1);
187}
188}
189int is_transmit2_triggered(void) 
190{ int __retres1 ;
191
192  {
193  if (t2_pc == 1) {
194    if (E_2 == 1) {
195      __retres1 = 1;
196      goto return_label;
197    } else {
198
199    }
200  } else {
201
202  }
203  __retres1 = 0;
204  return_label: /* CIL Label */ 
205  return (__retres1);
206}
207}
208void update_channels(void) 
209{ 
210
211  {
212
213  return;
214}
215}
216void init_threads(void) 
217{ 
218
219  {
220  if (m_i == 1) {
221    m_st = 0;
222  } else {
223    m_st = 2;
224  }
225  if (t1_i == 1) {
226    t1_st = 0;
227  } else {
228    t1_st = 2;
229  }
230  if (t2_i == 1) {
231    t2_st = 0;
232  } else {
233    t2_st = 2;
234  }
235
236  return;
237}
238}
239int exists_runnable_thread(void) 
240{ int __retres1 ;
241
242  {
243  if (m_st == 0) {
244    __retres1 = 1;
245    goto return_label;
246  } else {
247    if (t1_st == 0) {
248      __retres1 = 1;
249      goto return_label;
250    } else {
251      if (t2_st == 0) {
252        __retres1 = 1;
253        goto return_label;
254      } else {
255
256      }
257    }
258  }
259  __retres1 = 0;
260  return_label: /* CIL Label */ 
261  return (__retres1);
262}
263}
264void eval(void) 
265{
266  int tmp ;
267
268  {
269  {
270  while (1) {
271    while_3_continue: /* CIL Label */ ;
272    {
273    tmp = exists_runnable_thread();
274    }
275    if (tmp) {
276
277    } else {
278      goto while_3_break;
279    }
280    if (m_st == 0) {
281      int tmp_ndt_1;
282      tmp_ndt_1 = __VERIFIER_nondet_int();
283      if (tmp_ndt_1) {
284        {
285        m_st = 1;
286        master();
287        }
288      } else {
289
290      }
291    } else {
292
293    }
294    if (t1_st == 0) {
295      int tmp_ndt_2;
296      tmp_ndt_2 = __VERIFIER_nondet_int();
297      if (tmp_ndt_2) {
298        {
299        t1_st = 1;
300        transmit1();
301        }
302      } else {
303
304      }
305    } else {
306
307    }
308    if (t2_st == 0) {
309      int tmp_ndt_3;
310      tmp_ndt_3 = __VERIFIER_nondet_int();
311      if (tmp_ndt_3) {
312        {
313        t2_st = 1;
314        transmit2();
315        }
316      } else {
317
318      }
319    } else {
320
321    }
322  }
323  while_3_break: /* CIL Label */ ;
324  }
325
326  return;
327}
328}
329void fire_delta_events(void) 
330{ 
331
332  {
333  if (M_E == 0) {
334    M_E = 1;
335  } else {
336
337  }
338  if (T1_E == 0) {
339    T1_E = 1;
340  } else {
341
342  }
343  if (T2_E == 0) {
344    T2_E = 1;
345  } else {
346
347  }
348  if (E_M == 0) {
349    E_M = 1;
350  } else {
351
352  }
353  if (E_1 == 0) {
354    E_1 = 1;
355  } else {
356
357  }
358  if (E_2 == 0) {
359    E_2 = 1;
360  } else {
361
362  }
363
364  return;
365}
366}
367void reset_delta_events(void) 
368{ 
369
370  {
371  if (M_E == 1) {
372    M_E = 2;
373  } else {
374
375  }
376  if (T1_E == 1) {
377    T1_E = 2;
378  } else {
379
380  }
381  if (T2_E == 1) {
382    T2_E = 2;
383  } else {
384
385  }
386  if (E_M == 1) {
387    E_M = 2;
388  } else {
389
390  }
391  if (E_1 == 1) {
392    E_1 = 2;
393  } else {
394
395  }
396  if (E_2 == 1) {
397    E_2 = 2;
398  } else {
399
400  }
401
402  return;
403}
404}
405void activate_threads(void) 
406{ int tmp ;
407  int tmp___0 ;
408  int tmp___1 ;
409
410  {
411  {
412  tmp = is_master_triggered();
413  }
414  if (tmp) {
415    m_st = 0;
416  } else {
417
418  }
419  {
420  tmp___0 = is_transmit1_triggered();
421  }
422  if (tmp___0) {
423    t1_st = 0;
424  } else {
425
426  }
427  {
428  tmp___1 = is_transmit2_triggered();
429  }
430  if (tmp___1) {
431    t2_st = 0;
432  } else {
433
434  }
435
436  return;
437}
438}
439void immediate_notify(void) 
440{ 
441
442  {
443  {
444  activate_threads();
445  }
446
447  return;
448}
449}
450void fire_time_events(void) 
451{ 
452
453  {
454  M_E = 1;
455
456  return;
457}
458}
459void reset_time_events(void) 
460{ 
461
462  {
463  if (M_E == 1) {
464    M_E = 2;
465  } else {
466
467  }
468  if (T1_E == 1) {
469    T1_E = 2;
470  } else {
471
472  }
473  if (T2_E == 1) {
474    T2_E = 2;
475  } else {
476
477  }
478  if (E_M == 1) {
479    E_M = 2;
480  } else {
481
482  }
483  if (E_1 == 1) {
484    E_1 = 2;
485  } else {
486
487  }
488  if (E_2 == 1) {
489    E_2 = 2;
490  } else {
491
492  }
493
494  return;
495}
496}
497void init_model(void) 
498{ 
499
500  {
501  m_i = 1;
502  t1_i = 1;
503  t2_i = 1;
504
505  return;
506}
507}
508int stop_simulation(void) 
509{ int tmp ;
510  int __retres2 ;
511
512  {
513  {
514  tmp = exists_runnable_thread();
515  }
516  if (tmp) {
517    __retres2 = 0;
518    goto return_label;
519  } else {
520
521  }
522  __retres2 = 1;
523  return_label: /* CIL Label */ 
524  return (__retres2);
525}
526}
527void start_simulation(void) 
528{ int kernel_st ;
529  int tmp ;
530  int tmp___0 ;
531
532  {
533  {
534  kernel_st = 0;
535  update_channels();
536  init_threads();
537  fire_delta_events();
538  activate_threads();
539  reset_delta_events();
540  }
541  {
542  while (1) {
543    while_4_continue: /* CIL Label */ ;
544    {
545    kernel_st = 1;
546    eval();
547    }
548    {
549    kernel_st = 2;
550    update_channels();
551    }
552    {
553    kernel_st = 3;
554    fire_delta_events();
555    activate_threads();
556    reset_delta_events();
557    }
558    {
559    tmp = exists_runnable_thread();
560    }
561    if (tmp == 0) {
562      {
563      kernel_st = 4;
564      fire_time_events();
565      activate_threads();
566      reset_time_events();
567      }
568    } else {
569
570    }
571    {
572    tmp___0 = stop_simulation();
573    }
574    if (tmp___0) {
575      goto while_4_break;
576    } else {
577
578    }
579  }
580  while_4_break: /* CIL Label */ ;
581  }
582
583  return;
584}
585}
586int main(void) 
587{ int __retres1 ;
588
589  {
590  {
591  init_model();
592  start_simulation();
593  }
594  __retres1 = 0;
595  return (__retres1);
596}
597}
↑