Showing error 1442

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

Source: 

 1# 1 "files/volatile_alias.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/volatile_alias.c"
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18int main()
19{
20        int a = 4;
21        int * p = &a;
22        p = &a;
23        a = a - 4;
24        if (*p != 0){
25                ERROR: goto ERROR;
26        }
27        return 0;
28}
↑