Showing error 163

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.cil.c
Line in file: 24
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 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 a ;
 7  int *p ;
 8  int __cil_tmp3 ;
 9
10  {
11#line 15
12  a = 4;
13#line 16
14  p = & a;
15#line 17
16  p = & a;
17#line 18
18  a = a - 4;
19  {
20#line 19
21  __cil_tmp3 = *p;
22#line 19
23  if (__cil_tmp3 != 0) {
24    ERROR:assert(0); 
25#line 20
26    goto ERROR;
27  } else {
28
29  }
30  }
31#line 22
32  return (0);
33}
34}
↑