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