Showing error 1967

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


Source:

 706#line 85
 707  tmp = valid_product();
 708  }
 709#line 85
 710  if (tmp) {
 711    {
 712#line 86
 713    setup();
 714#line 87
 715    runTest();
 716    }
 717  } else {
 718
 719  }
 720#line 1234 "Test.c"
 721  retValue_acc = 0;
 722#line 1236
 723  return (retValue_acc);
 724#line 1243
 725  return (retValue_acc);
 726}
 727}
 728#line 1 "wsllib_check.o"
 729#pragma merger(0,"wsllib_check.i","")
 730#line 3 "wsllib_check.c"
 731void __automaton_fail(void) 
 732{ 
 733
 734  {
 735  goto ERROR;
 736  ERROR: ;
 737#line 53 "wsllib_check.c"
 738  return;
 739}
 740}
 741#line 1 "Specification2_spec.o"
 742#pragma merger(0,"Specification2_spec.i","")
 743#line 10 "MinePump.h"
 744int isPumpRunning(void) ;
 745#line 10 "Environment.h"
 746int isMethaneLevelCritical(void) ;
Show full sources