Showing error 1433

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-regression/test_union.c_safe_1.cil.c
Line in file: 15
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 1/* Generated by CIL v. 1.3.7 */
 2/* print_CIL_Input is true */
 3
 4#line 10 "files/test_union.c"
 5union A {
 6   int list ;
 7   int l2 ;
 8   char *str ;
 9};
10#line 2 "./assert.h"
11void __blast_assert(void) 
12{ 
13
14  {
15  ERROR: 
16#line 4
17  goto ERROR;
18}
19}
20#line 16 "files/test_union.c"
21int main(void) 
22{ union A x ;
23
24  {
25#line 18
26  x.list = 0;
27#line 20
28  if (x.l2 == 0) {
29
30  } else {
31    {
32#line 20
33    __blast_assert();
34    }
35  }
36#line 24
37  return (0);
38}
39}
↑