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.c-safe.cil.c |
Line in file: | 15 |
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.c" 5union A { 6 int list ; 7 int l2 ; 8 char *str ; 9}; 10#line 2 "./assert.h" 11void __blast_assert(void) 12{ 13 14 { 15 ERROR:assert(0); 16#line 4 17 goto ERROR; 18} 19} 20#line 16 "files/test_union.c" 21int main(void) 22{ union A x ; 23 24 { 25#line 18 26 x.list = 0; 27#line 22 28 if (x.list == 0) { 29 30 } else { 31 { 32#line 22 33 __blast_assert(); 34 } 35 } 36#line 24 37 return (0); 38} 39}