Showing error 125

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-regression/ex3_forlist.c-safe.cil.c
Line in file: 9
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 2 "./assert.h"
  5void __blast_assert(void) 
  6{ 
  7
  8  {
  9  ERROR:assert(0); 
 10#line 4
 11  goto ERROR;
 12}
 13}
 14#line 13 "files/ex3_forlist.c"
 15void *pp[2]  ;
 16#line 14 "files/ex3_forlist.c"
 17int pstate[2]  ;
 18#line 16 "files/ex3_forlist.c"
 19void init(void) 
Show full sources