Showing error 1353

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.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

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: 
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  {
30#line 25
31  a = 1;
32#line 29
33  q = return_self(& a);
34#line 32
35  *q = 2;
36  }
37#line 34
38  if (a != 2) {
39    {
40#line 34
41    err();
42    }
43  } else {
44
45  }
46#line 35
47  return (0);
48}
49}
↑