Showing error 1704

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


Source:

3473{ int tmp ;
3474
3475  {
3476  {
3477#line 13
3478  puts("before autoRespond\n");
3479#line 14
3480  tmp = isReadable(msg);
3481  }
3482#line 14
3483  if (tmp) {
3484
3485  } else {
3486    {
3487#line 15
3488    __automaton_fail();
3489    }
3490  }
3491#line 15
3492  return;
3493}
3494}
3495#line 1 "wsllib_check.o"
3496#pragma merger(0,"wsllib_check.i","")
3497#line 3 "wsllib_check.c"
3498void __automaton_fail(void) 
3499{ 
3500
3501  {
3502  goto ERROR;
3503  ERROR: ;
3504#line 53 "wsllib_check.c"
3505  return;
3506}
3507}
3508#line 1 "Test.o"
3509#pragma merger(0,"Test.i","")
3510#line 43 "featureselect.h"
3511void select_features(void) ;
3512#line 45
3513void select_helpers(void) ;
Show full sources