Showing error 1729

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


Source:

3819#line 20 "featureselect.c"
3820void select_helpers(void) 
3821{ 
3822
3823  {
3824#line 133 "featureselect.c"
3825  return;
3826}
3827}
3828#line 25 "featureselect.c"
3829int valid_product(void) 
3830{ int retValue_acc ;
3831
3832  {
3833#line 151 "featureselect.c"
3834  retValue_acc = 1;
3835#line 153
3836  return (retValue_acc);
3837#line 160
3838  return (retValue_acc);
3839}
3840}
3841#line 1 "wsllib_check.o"
3842#pragma merger(0,"wsllib_check.i","")
3843#line 3 "wsllib_check.c"
3844void __automaton_fail(void) 
3845{ 
3846
3847  {
3848  goto ERROR;
3849  ERROR: ;
3850#line 53 "wsllib_check.c"
3851  return;
3852}
3853}
3854#line 1 "VerifyForward_spec.o"
3855#pragma merger(0,"VerifyForward_spec.i","")
3856#line 12 "VerifyForward_spec.c"
3857__inline void __utac_acc__VerifyForward_spec__1(int client , int msg ) 
3858{ int pubkey ;
3859  int tmp ;
Show full sources