Showing error 1606

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

Source: 

3120#line 176
3121  tmp = valid_product();
3122  }
3123#line 176
3124  if (tmp) {
3125    {
3126#line 177
3127    setup();
3128#line 178
3129    runTest();
3130    }
3131  } else {
3132
3133  }
3134#line 1604 "Test.c"
3135  retValue_acc = 0;
3136#line 1606
3137  return (retValue_acc);
3138#line 1613
3139  return (retValue_acc);
3140}
3141}
3142#line 1 "wsllib_check.o"
3143#pragma merger(0,"wsllib_check.i","")
3144#line 3 "wsllib_check.c"
3145void __automaton_fail(void) 
3146{ 
3147
3148  {
3149  goto ERROR;
3150  ERROR: ;
3151#line 53 "wsllib_check.c"
3152  return;
3153}
3154}
3155#line 1 "UnitTests.o"
3156#pragma merger(0,"UnitTests.i","")
3157#line 24 "UnitTests.c"
3158void spec1(void) 
3159{ int tmp ;
3160  int tmp___0 ;
Show full sources
↑