Showing error 1425

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_1.cil.c
Line in file: 14
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_cast.c"
 5union X {
 6   int y ;
 7   double z ;
 8};
 9#line 2 "./assert.h"
10void __blast_assert(void) 
11{ 
12
13  {
14  ERROR: 
15#line 4
16  goto ERROR;
17}
18}
19#line 22 "files/test_union_cast.c"
20int main(void) 
21{ union X var ;
22  unsigned int __cil_tmp2 ;
23
24  {
25#line 25
26  var.z = 0x1.4p+4;
27#line 26
28  var.y = 10;
29  {
30#line 27
31  __cil_tmp2 = (unsigned int )var.y;
32#line 27
33  if (__cil_tmp2 == 10U) {
34
35  } else {
36    {
37#line 27
38    __blast_assert();
39    }
40  }
41  }
42#line 34
43  return (0);
44}
45}
↑