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/alias_of_return.c_safe_1.cil.c |
Line in file: | 9 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
1/* Generated by CIL v. 1.3.7 */ 2/* print_CIL_Input is true */ 3 4#line 12 "files/alias_of_return.c" 5void err(void) 6{ 7 8 { 9 ERROR: 10#line 13 11 goto ERROR; 12} 13} 14#line 16 "files/alias_of_return.c" 15int *return_self(int *p ) 16{ 17 18 { 19#line 18 20 return (p); 21} 22} 23#line 21 "files/alias_of_return.c" 24int main(void) 25{ int a ; 26 int *q ; 27 28 { 29#line 25 30 a = 1; 31#line 27 32 q = & a; 33#line 32 34 *q = 2; 35#line 34 36 if (a != 2) { 37 { 38#line 34 39 err(); 40 } 41 } else { 42 43 } 44#line 35 45 return (0); 46} 47}