Showing error 1601

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

Source: 

3195          } else {
3196#line 1188
3197            if (person == 5) {
3198#line 1193
3199              retValue_acc = 3;
3200#line 1195
3201              return (retValue_acc);
3202            } else {
3203#line 1201 "Person.c"
3204              retValue_acc = 0;
3205#line 1203
3206              return (retValue_acc);
3207            }
3208          }
3209        }
3210      }
3211    }
3212  }
3213#line 1210 "Person.c"
3214  return (retValue_acc);
3215}
3216}
3217#line 1 "wsllib_check.o"
3218#pragma merger(0,"wsllib_check.i","")
3219#line 3 "wsllib_check.c"
3220void __automaton_fail(void) 
3221{ 
3222
3223  {
3224  goto ERROR;
3225  ERROR: ;
3226#line 53 "wsllib_check.c"
3227  return;
3228}
3229}
3230#line 1 "Test.o"
3231#pragma merger(0,"Test.i","")
3232#line 544 "/usr/include/stdlib.h"
3233extern  __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ;
3234#line 17 "Test.c"
3235#line 23 "Test.c"
Show full sources
↑