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 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
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:assert(0); 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 {