Showing error 2324

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_unsafe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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