Showing error 1410

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.i
Line in file: 2
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

  1void __blast_assert(void) {
  2ERROR: goto ERROR;
  3}
  4
  5
  6
  7int ldv_mutex = 1;
  8
  9int open_called = 0;
 10int __VERIFIER_nondet_int(void) { int x; return x; }
 11
 12void mutex_lock(void)
Show full sources
↑