Showing error 1356

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