Showing error 161

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_while_int.c-unsafe_1.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 17 "files/test_while_int.c"
15int main(void) 
16{ int i ;
17
18  {
19#line 18
20  i = 0;
21  {
22#line 19
23  while (1) {
24    while_continue: /* CIL Label */ ;
25#line 19
26    if (i < 5) {
27
28    } else {
29#line 19
30      goto while_break;
31    }
32#line 20
33    i = i + 1;
34#line 22
35    if (i != 3) {
36
37    } else {
38      {
39#line 22
40      __blast_assert();
41      }
42    }
43  }
44  while_break: /* CIL Label */ ;
45  }
46#line 27
47  return (0);
48}
49}
↑