Showing error 242

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