Showing error 1752

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

Source: 

4513#line 28
4514      tmp___1 = getEmailSignKey(msg);
4515#line 28
4516      tmp___2 = isKeyPairValid(tmp___1, pubkey);
4517      }
4518#line 28
4519      if (tmp___2) {
4520
4521      } else {
4522        {
4523#line 29
4524        __automaton_fail();
4525        }
4526      }
4527    }
4528  } else {
4529
4530  }
4531#line 29
4532  return;
4533}
4534}
4535#line 1 "wsllib_check.o"
4536#pragma merger(0,"wsllib_check.i","")
4537#line 3 "wsllib_check.c"
4538void __automaton_fail(void) 
4539{ 
4540
4541  {
4542  goto ERROR;
4543  ERROR: ;
4544#line 53 "wsllib_check.c"
4545  return;
4546}
4547}
Show full sources
↑