Showing error 1856

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


Source:

 384#line 85
 385  tmp = valid_product();
 386  }
 387#line 85
 388  if (tmp) {
 389    {
 390#line 86
 391    setup();
 392#line 87
 393    runTest();
 394    }
 395  } else {
 396
 397  }
 398#line 1226 "Test.c"
 399  retValue_acc = 0;
 400#line 1228
 401  return (retValue_acc);
 402#line 1235
 403  return (retValue_acc);
 404}
 405}
 406#line 1 "wsllib_check.o"
 407#pragma merger(0,"wsllib_check.i","")
 408#line 3 "wsllib_check.c"
 409void __automaton_fail(void) 
 410{ 
 411
 412  {
 413  goto ERROR;
 414  ERROR: ;
 415#line 53 "wsllib_check.c"
 416  return;
 417}
 418}
 419#line 1 "libacc.o"
 420#pragma merger(0,"libacc.i","")
 421#line 73 "/usr/include/assert.h"
 422extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 423                                                                      char const   *__file ,
 424                                                                      unsigned int __line ,
Show full sources