Showing error 1725

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

Source: 

1117  {
1118  {
1119#line 198
1120  generateKeyPair(rjh, 666);
1121  }
1122#line 1801 "Test.c"
1123  return;
1124}
1125}
1126#line 204 "Test.c"
1127void rjhEnableForwarding(void) 
1128{ 
1129
1130  {
1131  {
1132#line 205
1133  setClientForwardReceiver(rjh, chuck);
1134  }
1135#line 1821 "Test.c"
1136  return;
1137}
1138}
1139#line 1 "wsllib_check.o"
1140#pragma merger(0,"wsllib_check.i","")
1141#line 3 "wsllib_check.c"
1142void __automaton_fail(void) 
1143{ 
1144
1145  {
1146  goto ERROR;
1147  ERROR: ;
1148#line 53 "wsllib_check.c"
1149  return;
1150}
1151}
1152#line 1 "scenario.o"
1153#pragma merger(0,"scenario.i","")
1154#line 1 "scenario.c"
1155void test(void) 
1156{ int op1 ;
1157  int op2 ;
Show full sources
↑