Showing error 36

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ddv-machzwd/ddv_machzwd_all_unsafe.cil.c
Line in file: 6371
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

6341}
6342#line 1633 "concatenated.c"
6343void __VERIFIER_assume(int phi ) 
6344{ 
6345
6346  {
6347  {
6348#line 1633
6349  while (1) {
6350    while_18_continue: /* CIL Label */ ;
6351#line 1633
6352    if (! phi) {
6353
6354    } else {
6355      goto while_18_break;
6356    }
6357  }
6358  while_18_break: /* CIL Label */ ;
6359  }
6360#line 1633
6361  return;
6362}
6363}
6364#line 1634 "concatenated.c"
6365void __VERIFIER_assert(int phi , char *txt ) 
6366{ 
6367
6368  {
6369#line 1634
6370  if (! phi) {
6371    ERROR: 
6372    goto ERROR;
6373  } else {
6374
6375  }
6376#line 1634
6377  return;
6378}
6379}
6380#line 1636 "concatenated.c"
6381int nonseekable_open(struct inode *inode , struct file *filp )
Show full sources
↑