Showing error 1695

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

Source: 

4393  if (handle == 1) {
4394#line 674
4395    __ste_client_idCounter0 = value;
4396  } else {
4397#line 675
4398    if (handle == 2) {
4399#line 676
4400      __ste_client_idCounter1 = value;
4401    } else {
4402#line 677
4403      if (handle == 3) {
4404#line 678
4405        __ste_client_idCounter2 = value;
4406      } else {
4407
4408      }
4409    }
4410  }
4411#line 2682 "ClientLib.c"
4412  return;
4413}
4414}
4415#line 1 "wsllib_check.o"
4416#pragma merger(0,"wsllib_check.i","")
4417#line 3 "wsllib_check.c"
4418void __automaton_fail(void) 
4419{ 
4420
4421  {
4422  goto ERROR;
4423  ERROR: ;
4424#line 53 "wsllib_check.c"
4425  return;
4426}
4427}
Show full sources
↑