Showing error 2016

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

Source: 

1312#line 12
1313      if (tmp___1) {
1314
1315      } else {
1316
1317      }
1318    }
1319    {
1320#line 14
1321    timeShift();
1322    }
1323  }
1324  while_4_break: /* CIL Label */ ;
1325  }
1326  {
1327#line 16
1328  cleanup();
1329  }
1330#line 76 "scenario.c"
1331  return;
1332}
1333}
1334#line 1 "wsllib_check.o"
1335#pragma merger(0,"wsllib_check.i","")
1336#line 3 "wsllib_check.c"
1337void __automaton_fail(void) 
1338{ 
1339
1340  {
1341  goto ERROR;
1342  ERROR: ;
1343#line 53 "wsllib_check.c"
1344  return;
1345}
1346}
Show full sources
↑