Showing error 1938

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


Source:

 373#line 85
 374  tmp = valid_product();
 375  }
 376#line 85
 377  if (tmp) {
 378    {
 379#line 86
 380    setup();
 381#line 87
 382    runTest();
 383    }
 384  } else {
 385
 386  }
 387#line 1234 "Test.c"
 388  retValue_acc = 0;
 389#line 1236
 390  return (retValue_acc);
 391#line 1243
 392  return (retValue_acc);
 393}
 394}
 395#line 1 "wsllib_check.o"
 396#pragma merger(0,"wsllib_check.i","")
 397#line 3 "wsllib_check.c"
 398void __automaton_fail(void) 
 399{ 
 400
 401  {
 402  goto ERROR;
 403  ERROR: ;
 404#line 53 "wsllib_check.c"
 405  return;
 406}
 407}
 408#line 1 "MinePump.o"
 409#pragma merger(0,"MinePump.i","")
 410#line 6 "MinePump.h"
 411void activatePump(void) ;
 412#line 8
 413void deactivatePump(void) ;
Show full sources