Showing error 1760

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

Source: 

4286  return;
4287}
4288}
4289#line 210 "Test.c"
4290void bobSetAddressBook(void) 
4291{ 
4292
4293  {
4294  {
4295#line 211
4296  setClientAddressBookSize(bob, 1);
4297#line 212
4298  setClientAddressBookAlias(bob, 0, rjh);
4299#line 213
4300  setClientAddressBookAddress(bob, 0, rjh);
4301#line 214
4302  setClientAddressBookAddress(bob, 1, chuck);
4303  }
4304#line 1851 "Test.c"
4305  return;
4306}
4307}
4308#line 1 "wsllib_check.o"
4309#pragma merger(0,"wsllib_check.i","")
4310#line 3 "wsllib_check.c"
4311void __automaton_fail(void) 
4312{ 
4313
4314  {
4315  goto ERROR;
4316  ERROR: ;
4317#line 53 "wsllib_check.c"
4318  return;
4319}
4320}
4321#line 1 "featureselect.o"
4322#pragma merger(0,"featureselect.i","")
4323#line 41 "featureselect.h"
4324int select_one(void) ;
4325#line 8 "featureselect.c"
4326int select_one(void)
Show full sources
↑