Showing error 1791

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


Source:

3112#line 20 "featureselect.c"
3113void select_helpers(void) 
3114{ 
3115
3116  {
3117#line 133 "featureselect.c"
3118  return;
3119}
3120}
3121#line 25 "featureselect.c"
3122int valid_product(void) 
3123{ int retValue_acc ;
3124
3125  {
3126#line 151 "featureselect.c"
3127  retValue_acc = 1;
3128#line 153
3129  return (retValue_acc);
3130#line 160
3131  return (retValue_acc);
3132}
3133}
3134#line 1 "wsllib_check.o"
3135#pragma merger(0,"wsllib_check.i","")
3136#line 3 "wsllib_check.c"
3137void __automaton_fail(void) 
3138{ 
3139
3140  {
3141  goto ERROR;
3142  ERROR: ;
3143#line 53 "wsllib_check.c"
3144  return;
3145}
3146}
3147#line 1 "scenario.o"
3148#pragma merger(0,"scenario.i","")
3149#line 17 "scenario.c"
3150void bobKeyAdd(void) ;
3151#line 24
3152void rjhDeletePrivateKey(void) ;
Show full sources