Showing error 1776

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_spec6_product16_unsafe.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#line 227 "EmailLib.c"
2766void setEmailIsSignatureVerified(int handle , int value ) 
2767{ 
2768
2769  {
2770#line 233
2771  if (handle == 1) {
2772#line 229
2773    __ste_email_isSignatureVerified0 = value;
2774  } else {
2775#line 230
2776    if (handle == 2) {
2777#line 231
2778      __ste_email_isSignatureVerified1 = value;
2779    } else {
2780
2781    }
2782  }
2783#line 1511 "EmailLib.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 "libacc.o"
2801#pragma merger(0,"libacc.i","")
2802#line 73 "/usr/include/assert.h"
2803extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
2804                                                                      char const   *__file ,
2805                                                                      unsigned int __line ,
Show full sources
↑