Showing error 2323

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