Showing error 1780

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

Source: 

3445    tmp = getClientPrivateKey(client);
3446#line 28
3447    tmp___0 = getEmailEncryptionKey(msg);
3448#line 28
3449    tmp___1 = isKeyPairValid(tmp___0, tmp);
3450    }
3451#line 28
3452    if (tmp___1) {
3453
3454    } else {
3455      {
3456#line 26
3457      __automaton_fail();
3458      }
3459    }
3460  } else {
3461
3462  }
3463#line 26
3464  return;
3465}
3466}
3467#line 1 "wsllib_check.o"
3468#pragma merger(0,"wsllib_check.i","")
3469#line 3 "wsllib_check.c"
3470void __automaton_fail(void) 
3471{ 
3472
3473  {
3474  goto ERROR;
3475  ERROR: ;
3476#line 53 "wsllib_check.c"
3477  return;
3478}
3479}
3480#line 1 "scenario.o"
3481#pragma merger(0,"scenario.i","")
3482#line 1 "scenario.c"
3483void test(void) 
3484{ int op1 ;
3485  int op2 ;
Show full sources
↑