Showing error 1956

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


Source:

 831#line 85
 832  tmp = valid_product();
 833  }
 834#line 85
 835  if (tmp) {
 836    {
 837#line 86
 838    setup();
 839#line 87
 840    runTest();
 841    }
 842  } else {
 843
 844  }
 845#line 1234 "Test.c"
 846  retValue_acc = 0;
 847#line 1236
 848  return (retValue_acc);
 849#line 1243
 850  return (retValue_acc);
 851}
 852}
 853#line 1 "wsllib_check.o"
 854#pragma merger(0,"wsllib_check.i","")
 855#line 3 "wsllib_check.c"
 856void __automaton_fail(void) 
 857{ 
 858
 859  {
 860  goto ERROR;
 861  ERROR: ;
 862#line 53 "wsllib_check.c"
 863  return;
 864}
 865}
 866#line 1 "libacc.o"
 867#pragma merger(0,"libacc.i","")
 868#line 73 "/usr/include/assert.h"
 869extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 870                                                                      char const   *__file ,
 871                                                                      unsigned int __line ,
Show full sources