Showing error 1991

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

Source: 

 811
 812  {
 813  {
 814#line 329 "MinePump.c"
 815  tmp = isLowWaterSensorDry();
 816  }
 817#line 329
 818  if (tmp) {
 819#line 329
 820    tmp___0 = 0;
 821  } else {
 822#line 329
 823    tmp___0 = 1;
 824  }
 825#line 329
 826  retValue_acc = tmp___0;
 827#line 331
 828  return (retValue_acc);
 829#line 338
 830  return (retValue_acc);
 831}
 832}
 833#line 1 "wsllib_check.o"
 834#pragma merger(0,"wsllib_check.i","")
 835#line 3 "wsllib_check.c"
 836void __automaton_fail(void) 
 837{ 
 838
 839  {
 840  goto ERROR;
 841  ERROR: ;
 842#line 53 "wsllib_check.c"
 843  return;
 844}
 845}
 846#line 1 "scenario.o"
 847#pragma merger(0,"scenario.i","")
 848#line 5 "scenario.c"
 849void waterRise(void) ;
 850#line 7
 851#line 8
Show full sources
↑