Showing error 1424

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.i
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

 1# 1 "files/test_union_cast.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/test_union_cast.c"
 5# 1 "./assert.h" 1
 6
 7void __blast_assert()
 8{
 9 ERROR: goto ERROR;
10}
11# 2 "files/test_union_cast.c" 2
12
13
14
15
16
17
18# 19 "files/test_union_cast.c"
19struct l_struct_2E_X {
20  double field0;
21};
22
23
24int main(void) {
25
26
27
28
29
30
31 struct l_struct_2E_X llvm_cbe_var;
32 *((&llvm_cbe_var.field0)) = 0x1.4p+4;
33 *(((unsigned int *)((&llvm_cbe_var.field0)))) = 10u;
34 ((*(((unsigned int *)((&llvm_cbe_var.field0)))) == 10u) ? (0) : __blast_assert ());
35
36 return 0;
37}