Showing error 120

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 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

 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:assert(0); 
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}
↑