Showing error 1358

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.i
Line in file: 11
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 1# 1 "files/alias_of_return_2.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/alias_of_return_2.c"
 5# 10 "files/alias_of_return_2.c"
 6
 7
 8
 9
10void err()
11{ ERROR: goto ERROR; }
12
13int __VERIFIER_nondet_int();
14
15int * return_self (int * p)
16{
17 if (__VERIFIER_nondet_int()){
18  return p;
19 }else{
20  return p;
21 }
22}
23
24int main()
25{
26 int a,*q;
27
28 a = 1;
29
30
31
32 q = return_self(&a);
33
34
35 *q = 2;
36
37 if (a != 2) err();
38}
↑