Showing error 1809

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

Source: 

3204#line 23
3205  if (in_encrypted) {
3206    {
3207#line 23
3208    tmp = isEncrypted(msg);
3209    }
3210#line 23
3211    if (tmp) {
3212
3213    } else {
3214      {
3215#line 24
3216      __automaton_fail();
3217      }
3218    }
3219  } else {
3220
3221  }
3222#line 24
3223  return;
3224}
3225}
3226#line 1 "wsllib_check.o"
3227#pragma merger(0,"wsllib_check.i","")
3228#line 3 "wsllib_check.c"
3229void __automaton_fail(void) 
3230{ 
3231
3232  {
3233  goto ERROR;
3234  ERROR: ;
3235#line 53 "wsllib_check.c"
3236  return;
3237}
3238}
3239#line 1 "Email.o"
3240#pragma merger(0,"Email.i","")
3241#line 6 "Email.h"
3242void printMail(int msg ) ;
3243#line 9
3244int isReadable(int msg ) ;
Show full sources
↑