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: 

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}
Show full sources
↑