Showing error 1712

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


Source:

2267    {
2268#line 220
2269    tmp___3 = getEmailSignKey(msg);
2270#line 220
2271    tmp___4 = isKeyPairValid(tmp___3, pubkey);
2272    }
2273#line 220
2274    if (tmp___4) {
2275      {
2276#line 221
2277      setEmailIsSignatureVerified(msg, 1);
2278      }
2279    } else {
2280
2281    }
2282  } else {
2283
2284  }
2285#line 1443 "Client.c"
2286  return;
2287}
2288}
2289#line 1 "wsllib_check.o"
2290#pragma merger(0,"wsllib_check.i","")
2291#line 3 "wsllib_check.c"
2292void __automaton_fail(void) 
2293{ 
2294
2295  {
2296  goto ERROR;
2297  ERROR: ;
2298#line 53 "wsllib_check.c"
2299  return;
2300}
2301}
2302#line 1 "featureselect.o"
2303#pragma merger(0,"featureselect.i","")
2304#line 41 "featureselect.h"
2305int select_one(void) ;
2306#line 43
2307void select_features(void) ;
Show full sources