Showing error 1709

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

Source: 

2507  if (handle == 1) {
2508#line 674
2509    __ste_client_idCounter0 = value;
2510  } else {
2511#line 675
2512    if (handle == 2) {
2513#line 676
2514      __ste_client_idCounter1 = value;
2515    } else {
2516#line 677
2517      if (handle == 3) {
2518#line 678
2519        __ste_client_idCounter2 = value;
2520      } else {
2521
2522      }
2523    }
2524  }
2525#line 2682 "ClientLib.c"
2526  return;
2527}
2528}
2529#line 1 "wsllib_check.o"
2530#pragma merger(0,"wsllib_check.i","")
2531#line 3 "wsllib_check.c"
2532void __automaton_fail(void) 
2533{ 
2534
2535  {
2536  goto ERROR;
2537  ERROR: ;
2538#line 53 "wsllib_check.c"
2539  return;
2540}
2541}
2542#line 1 "Test.o"
2543#pragma merger(0,"Test.i","")
2544#line 17 "Client.h"
2545int is_queue_empty(void) ;
2546#line 19
2547int get_queued_client(void) ;
Show full sources
↑