Showing error 272

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