Showing error 1773

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

Source: 

3481#line 227 "EmailLib.c"
3482void setEmailIsSignatureVerified(int handle , int value ) 
3483{ 
3484
3485  {
3486#line 233
3487  if (handle == 1) {
3488#line 229
3489    __ste_email_isSignatureVerified0 = value;
3490  } else {
3491#line 230
3492    if (handle == 2) {
3493#line 231
3494      __ste_email_isSignatureVerified1 = value;
3495    } else {
3496
3497    }
3498  }
3499#line 1511 "EmailLib.c"
3500  return;
3501}
3502}
3503#line 1 "wsllib_check.o"
3504#pragma merger(0,"wsllib_check.i","")
3505#line 3 "wsllib_check.c"
3506void __automaton_fail(void) 
3507{ 
3508
3509  {
3510  goto ERROR;
3511  ERROR: ;
3512#line 53 "wsllib_check.c"
3513  return;
3514}
3515}
3516#line 1 "Client.o"
3517#pragma merger(0,"Client.i","")
3518#line 14 "Client.h"
3519void queue(int client , int msg ) ;
3520#line 24
3521void mail(int client , int msg ) ;
Show full sources
↑