Showing error 1429

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_cast-2_safe.cil.c
Line in file: 59
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 19 "test_union_cast-2-safe.c"
 5struct l_struct_2E_X {
 6   double field0 ;
 7};
 8#line 71 "/usr/include/assert.h"
 9extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
10                                                                      char const   *__file ,
11                                                                      unsigned int __line ,
12                                                                      char const   *__function ) ;
13#line 7 "test_union_cast-2-safe.c"
14
15#line 8 "test_union_cast-2-safe.c"
16int CURRENTLY_UNKNOWN  ;
17#line 24 "test_union_cast-2-safe.c"
18int main(void) 
19{ struct l_struct_2E_X llvm_cbe_var ;
20  struct l_struct_2E_X *__cil_tmp2 ;
21  struct l_struct_2E_X *__cil_tmp3 ;
22  double *__cil_tmp4 ;
23  unsigned int *__cil_tmp5 ;
24  struct l_struct_2E_X *__cil_tmp6 ;
25  double *__cil_tmp7 ;
26  unsigned int *__cil_tmp8 ;
27  unsigned int __cil_tmp9 ;
28
29  {
30#line 32
31  __cil_tmp2 = & llvm_cbe_var;
32#line 32
33  *((double *)__cil_tmp2) = 0x1.4p+4;
34#line 33
35  __cil_tmp3 = & llvm_cbe_var;
36#line 33
37  __cil_tmp4 = (double *)__cil_tmp3;
38#line 33
39  __cil_tmp5 = (unsigned int *)__cil_tmp4;
40#line 33
41  *__cil_tmp5 = 10U;
42  {
43#line 34
44  __cil_tmp6 = & llvm_cbe_var;
45#line 34
46  __cil_tmp7 = (double *)__cil_tmp6;
47#line 34
48  __cil_tmp8 = (unsigned int *)__cil_tmp7;
49#line 34
50  __cil_tmp9 = *__cil_tmp8;
51#line 34
52  if (__cil_tmp9 == 10U) {
53
54  } else {
55    {
56#line 34
57    //__assert_fail("*(((unsigned int *)((&llvm_cbe_var.field0)))) == 10u", "test_union_cast-2-safe.c",
58    //              34U, "main");
59    ERROR: goto ERROR;
60    }
61  }
62  }
63#line 36
64  return (0);
65}
66}
↑