Showing error 1676

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


Source:

1986#line 20 "featureselect.c"
1987void select_helpers(void) 
1988{ 
1989
1990  {
1991#line 133 "featureselect.c"
1992  return;
1993}
1994}
1995#line 25 "featureselect.c"
1996int valid_product(void) 
1997{ int retValue_acc ;
1998
1999  {
2000#line 151 "featureselect.c"
2001  retValue_acc = 1;
2002#line 153
2003  return (retValue_acc);
2004#line 160
2005  return (retValue_acc);
2006}
2007}
2008#line 1 "wsllib_check.o"
2009#pragma merger(0,"wsllib_check.i","")
2010#line 3 "wsllib_check.c"
2011void __automaton_fail(void) 
2012{ 
2013
2014  {
2015  goto ERROR;
2016  ERROR: ;
2017#line 53 "wsllib_check.c"
2018  return;
2019}
2020}
2021#line 1 "DecryptForward_spec.o"
2022#pragma merger(0,"DecryptForward_spec.i","")
2023#line 688 "/usr/include/stdio.h"
2024extern int puts(char const   *__s ) ;
2025#line 11 "DecryptForward_spec.c"
2026__inline void __utac_acc__DecryptForward_spec__1(int msg ) 
Show full sources