Showing error 1854

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


Source:

1219#line 17
1220  if (tmp) {
1221    {
1222#line 17
1223    tmp___0 = isPumpRunning();
1224    }
1225#line 17
1226    if (tmp___0) {
1227      {
1228#line 14
1229      __automaton_fail();
1230      }
1231    } else {
1232
1233    }
1234  } else {
1235
1236  }
1237#line 14
1238  return;
1239}
1240}
1241#line 1 "wsllib_check.o"
1242#pragma merger(0,"wsllib_check.i","")
1243#line 3 "wsllib_check.c"
1244void __automaton_fail(void) 
1245{ 
1246
1247  {
1248  goto ERROR;
1249  ERROR: ;
1250#line 53 "wsllib_check.c"
1251  return;
1252}
1253}
Show full sources