Showing error 1756

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

Source: 

2765  {
2766  {
2767#line 191
2768  generateKeyPair(bob, 777);
2769  }
2770#line 1777 "Test.c"
2771  return;
2772}
2773}
2774#line 197 "Test.c"
2775void rjhKeyChange(void) 
2776{ 
2777
2778  {
2779  {
2780#line 198
2781  generateKeyPair(rjh, 666);
2782  }
2783#line 1797 "Test.c"
2784  return;
2785}
2786}
2787#line 1 "wsllib_check.o"
2788#pragma merger(0,"wsllib_check.i","")
2789#line 3 "wsllib_check.c"
2790void __automaton_fail(void) 
2791{ 
2792
2793  {
2794  goto ERROR;
2795  ERROR: ;
2796#line 53 "wsllib_check.c"
2797  return;
2798}
2799}
2800#line 1 "scenario.o"
2801#pragma merger(0,"scenario.i","")
2802#line 1 "scenario.c"
2803void test(void) 
2804{ int op1 ;
2805  int op2 ;
Show full sources
↑