Showing error 150

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/test_cut_trace.c-safe.cil.c
Line in file: 9
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 2 "./assert.h"
 5void __blast_assert(void) 
 6{ 
 7
 8  {
 9  ERROR:assert(0); 
10#line 4
11  goto ERROR;
12}
13}
14#line 6 "files/test_cut_trace.c"
15int main(void) 
16{ int z ;
17  int a ;
18
19  {
20#line 8
21  z = 0;
22#line 9
23  if (z == 0) {
24
25  } else {
26    {
27#line 9
28    __blast_assert();
29    }
30  }
31#line 10
32  a = z;
33#line 11
34  if (a == 0) {
35
36  } else {
37    {
38#line 11
39    __blast_assert();
40    }
41  }
42#line 12
43  return (0);
44}
45}
↑