Showing error 1526

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