Showing error 1357

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_2.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 13 "files/alias_of_return_2.c"
 5void err(void) 
 6{ 
 7
 8  {
 9  ERROR: 
10#line 14
11  goto ERROR;
12}
13}
14#line 16
15extern int __VERIFIER_nondet_int() ;
16#line 18 "files/alias_of_return_2.c"
17int *return_self(int *p ) 
18{ int tmp ;
19
20  {
21  {
22#line 20
23  tmp = __VERIFIER_nondet_int();
24  }
25#line 20
26  if (tmp) {
27#line 21
28    return (p);
29  } else {
30#line 23
31    return (p);
32  }
33}
34}
35#line 27 "files/alias_of_return_2.c"
36int main(void) 
37{ int a ;
38  int *q ;
39
40  {
41  {
42#line 31
43  a = 1;
44#line 35
45  q = return_self(& a);
46#line 38
47  *q = 2;
48  }
49#line 40
50  if (a != 2) {
51    {
52#line 40
53    err();
54    }
55  } else {
56
57  }
58#line 41
59  return (0);
60}
61}
↑