Showing error 273

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