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/volatile_alias.c-safe.cil.c |
Line in file: | 27 |
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 13 "files/volatile_alias.c" 5int main(void) 6{ int volatile a ; 7 int *p ; 8 int volatile __cil_tmp3 ; 9 int __cil_tmp4 ; 10 11 { 12#line 15 13 a = (int volatile )4; 14#line 16 15 p = (int *)(& a); 16#line 17 17 p = (int *)(& a); 18#line 18 19 __cil_tmp3 = (int volatile )4; 20#line 18 21 a = a - __cil_tmp3; 22 { 23#line 19 24 __cil_tmp4 = *p; 25#line 19 26 if (__cil_tmp4 != 0) { 27 ERROR:assert(0); 28#line 20 29 goto ERROR; 30 } else { 31 32 } 33 } 34#line 22 35 return (0); 36} 37}