Showing error 1777

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


Source:

3721  return;
3722}
3723}
3724#line 210 "Test.c"
3725void bobSetAddressBook(void) 
3726{ 
3727
3728  {
3729  {
3730#line 211
3731  setClientAddressBookSize(bob, 1);
3732#line 212
3733  setClientAddressBookAlias(bob, 0, rjh);
3734#line 213
3735  setClientAddressBookAddress(bob, 0, rjh);
3736#line 214
3737  setClientAddressBookAddress(bob, 1, chuck);
3738  }
3739#line 1847 "Test.c"
3740  return;
3741}
3742}
3743#line 1 "wsllib_check.o"
3744#pragma merger(0,"wsllib_check.i","")
3745#line 3 "wsllib_check.c"
3746void __automaton_fail(void) 
3747{ 
3748
3749  {
3750  goto ERROR;
3751  ERROR: ;
3752#line 53 "wsllib_check.c"
3753  return;
3754}
3755}
3756#line 1 "Client.o"
3757#pragma merger(0,"Client.i","")
3758#line 12 "Email.h"
3759int createEmail(int from , int to ) ;
3760#line 14 "Client.h"
3761void queue(int client , int msg ) ;
Show full sources