Showing error 1439

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.cil.c
Line in file: 27
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/volatile_alias.c"
 5int main(void) 
 6{ int volatile   a ;
 7  int *p ;
 8  int volatile   __cil_tmp3 ;
 9  int __cil_tmp4 ;
10
11  {
12#line 15
13  a = (int volatile   )4;
14#line 16
15  p = (int *)(& a);
16#line 17
17  p = (int *)(& a);
18#line 18
19  __cil_tmp3 = (int volatile   )4;
20#line 18
21  a = a - __cil_tmp3;
22  {
23#line 19
24  __cil_tmp4 = *p;
25#line 19
26  if (__cil_tmp4 != 0) {
27    ERROR: 
28#line 20
29    goto ERROR;
30  } else {
31
32  }
33  }
34#line 22
35  return (0);
36}
37}
↑