Showing error 154

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.c-safe.cil.c
Line in file: 13
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

 1/* Generated by CIL v. 1.3.7 */
 2/* print_CIL_Input is true */
 3
 4#line 19 "files/test_union_cast.c"
 5struct l_struct_2E_X {
 6   double field0 ;
 7};
 8#line 2 "./assert.h"
 9void __blast_assert(void) 
10{ 
11
12  {
13  ERROR:assert(0); 
14#line 4
15  goto ERROR;
16}
17}
18#line 24 "files/test_union_cast.c"
19int main(void) 
20{ struct l_struct_2E_X llvm_cbe_var ;
21  double *__cil_tmp2 ;
22  unsigned int *__cil_tmp3 ;
23  double *__cil_tmp4 ;
24  unsigned int *__cil_tmp5 ;
25  unsigned int __cil_tmp6 ;
26
27  {
28#line 32
29  llvm_cbe_var.field0 = 0x1.4p+4;
30#line 33
31  __cil_tmp2 = & llvm_cbe_var.field0;
32#line 33
33  __cil_tmp3 = (unsigned int *)__cil_tmp2;
34#line 33
35  *__cil_tmp3 = 10U;
36  {
37#line 34
38  __cil_tmp4 = & llvm_cbe_var.field0;
39#line 34
40  __cil_tmp5 = (unsigned int *)__cil_tmp4;
41#line 34
42  __cil_tmp6 = *__cil_tmp5;
43#line 34
44  if (__cil_tmp6 == 10U) {
45
46  } else {
47    {
48#line 34
49    __blast_assert();
50    }
51  }
52  }
53#line 36
54  return (0);
55}
56}
↑