Showing error 1582

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


Source:

3861#line 176
3862  tmp = valid_product();
3863  }
3864#line 176
3865  if (tmp) {
3866    {
3867#line 177
3868    setup();
3869#line 178
3870    runTest();
3871    }
3872  } else {
3873
3874  }
3875#line 1620 "Test.c"
3876  retValue_acc = 0;
3877#line 1622
3878  return (retValue_acc);
3879#line 1629
3880  return (retValue_acc);
3881}
3882}
3883#line 1 "wsllib_check.o"
3884#pragma merger(0,"wsllib_check.i","")
3885#line 3 "wsllib_check.c"
3886void __automaton_fail(void) 
3887{ 
3888
3889  {
3890  goto ERROR;
3891  ERROR: ;
3892#line 53 "wsllib_check.c"
3893  return;
3894}
3895}
3896#line 1 "Floor.o"
3897#pragma merger(0,"Floor.i","")
3898#line 16 "Floor.h"
3899void callOnFloor(int floorID ) ;
3900#line 9 "Floor.c"
3901int calls_0  ;
Show full sources