Showing error 2057

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


Source:

 713#line 85
 714  tmp = valid_product();
 715  }
 716#line 85
 717  if (tmp) {
 718    {
 719#line 86
 720    setup();
 721#line 87
 722    runTest();
 723    }
 724  } else {
 725
 726  }
 727#line 1226 "Test.c"
 728  retValue_acc = 0;
 729#line 1228
 730  return (retValue_acc);
 731#line 1235
 732  return (retValue_acc);
 733}
 734}
 735#line 1 "wsllib_check.o"
 736#pragma merger(0,"wsllib_check.i","")
 737#line 3 "wsllib_check.c"
 738void __automaton_fail(void) 
 739{ 
 740
 741  {
 742  goto ERROR;
 743  ERROR: ;
 744#line 53 "wsllib_check.c"
 745  return;
 746}
 747}
 748#line 1 "Specification4_spec.o"
 749#pragma merger(0,"Specification4_spec.i","")
 750#line 11 "Specification4_spec.c"
 751void __utac_acc__Specification4_spec__1(void) 
 752{ int tmp ;
 753  int tmp___0 ;
Show full sources