Showing error 1504

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: loops/pc_sfifo_1_safe.i
Line in file: 7
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();
  2void error(void)
  3{
  4
  5  {
  6  goto ERROR;
  7  ERROR: ;
  8  return;
  9}
 10}
 11
 12int q_buf_0 ;
 13int q_free ;
 14int q_read_ev ;
 15int q_write_ev ;
 16int p_num_write ;
 17int p_last_write ;
Show full sources