Showing error 1730

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

Source: 

2330    {
2331#line 180
2332    tmp___3 = getEmailSignKey(msg);
2333#line 180
2334    tmp___4 = isKeyPairValid(tmp___3, pubkey);
2335    }
2336#line 180
2337    if (tmp___4) {
2338      {
2339#line 181
2340      setEmailIsSignatureVerified(msg, 1);
2341      }
2342    } else {
2343
2344    }
2345  } else {
2346
2347  }
2348#line 1216 "Client.c"
2349  return;
2350}
2351}
2352#line 1 "wsllib_check.o"
2353#pragma merger(0,"wsllib_check.i","")
2354#line 3 "wsllib_check.c"
2355void __automaton_fail(void) 
2356{ 
2357
2358  {
2359  goto ERROR;
2360  ERROR: ;
2361#line 53 "wsllib_check.c"
2362  return;
2363}
2364}
2365#line 1 "Util.o"
2366#pragma merger(0,"Util.i","")
2367#line 1 "Util.h"
2368int prompt(char *msg ) ;
2369#line 9 "Util.c"
2370int prompt(char *msg )
Show full sources
↑