Showing error 1646

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


Source:

4946
4947      } else {
4948        goto while_9_break;
4949      }
4950    } else {
4951      goto while_9_break;
4952    }
4953    {
4954#line 58
4955    timeShift();
4956#line 59
4957    printState();
4958#line 57
4959    i = i + 1;
4960    }
4961  }
4962  while_9_break: /* CIL Label */ ;
4963  }
4964#line 1125 "UnitTests.c"
4965  return;
4966}
4967}
4968#line 1 "wsllib_check.o"
4969#pragma merger(0,"wsllib_check.i","")
4970#line 3 "wsllib_check.c"
4971void __automaton_fail(void) 
4972{ 
4973
4974  {
4975  goto ERROR;
4976  ERROR: ;
4977#line 53 "wsllib_check.c"
4978  return;
4979}
4980}
4981#line 1 "featureselect.o"
4982#pragma merger(0,"featureselect.i","")
4983#line 9 "featureselect.h"
4984int select_one(void) ;
4985#line 8 "featureselect.c"
4986int select_one(void) 
Show full sources