Showing error 1409

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/stateful_check_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: 

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 1 "stateful_check.c"
  5void __blast_assert(void) 
  6{ 
  7
  8  {
  9  ERROR: 
 10  goto ERROR;
 11}
 12}
 13#line 7 "stateful_check.c"
 14int ldv_mutex  =    1;
 15#line 9 "stateful_check.c"
 16int open_called  =    0;
 17#line 10
 18int __VERIFIER_nondet_int(void) { int x; return x; }
 19#line 12 "stateful_check.c"
Show full sources
↑