Showing error 1826

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

Source: 

3245  if (handle == 1) {
3246#line 674
3247    __ste_client_idCounter0 = value;
3248  } else {
3249#line 675
3250    if (handle == 2) {
3251#line 676
3252      __ste_client_idCounter1 = value;
3253    } else {
3254#line 677
3255      if (handle == 3) {
3256#line 678
3257        __ste_client_idCounter2 = value;
3258      } else {
3259
3260      }
3261    }
3262  }
3263#line 2682 "ClientLib.c"
3264  return;
3265}
3266}
3267#line 1 "wsllib_check.o"
3268#pragma merger(0,"wsllib_check.i","")
3269#line 3 "wsllib_check.c"
3270void __automaton_fail(void) 
3271{ 
3272
3273  {
3274  goto ERROR;
3275  ERROR: ;
3276#line 53 "wsllib_check.c"
3277  return;
3278}
3279}
3280#line 1 "Client.o"
3281#pragma merger(0,"Client.i","")
3282#line 688 "/usr/include/stdio.h"
3283extern int puts(char const   *__s ) ;
3284#line 12 "Email.h"
3285int createEmail(int from , int to ) ;
Show full sources
↑