Showing error 1427

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-1_safe.cil.c
Line in file: 38
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 12 "test_union_cast-1-safe.c"
 5union X {
 6   int y ;
 7   double z ;
 8};
 9#line 71 "/usr/include/assert.h"
10extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
11                                                                      char const   *__file ,
12                                                                      unsigned int __line ,
13                                                                      char const   *__function ) ;
14#line 4 "test_union_cast-1-safe.c"
15
16#line 5 "test_union_cast-1-safe.c"
17int CURRENTLY_SAFE  ;
18#line 24 "test_union_cast-1-safe.c"
19int main(void) 
20{ union X var ;
21  unsigned int __cil_tmp2 ;
22
23  {
24#line 27
25  var.z = 0x1.4p+4;
26#line 28
27  var.y = 10;
28  {
29#line 29
30  __cil_tmp2 = (unsigned int )var.y;
31#line 29
32  if (__cil_tmp2 == 10U) {
33
34  } else {
35    {
36#line 29
37    //__assert_fail("var.y==10u", "test_union_cast-1-safe.c", 29U, "main");
38    ERROR: goto ERROR;
39    }
40  }
41  }
42#line 36
43  return (0);
44}
45}
↑