Showing error 1435

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.cil.c
Line in file: 9
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 2 "./assert.h"
 5void __blast_assert(void) 
 6{ 
 7
 8  {
 9  ERROR: 
10#line 4
11  goto ERROR;
12}
13}
14#line 10 "files/test_while_int.c"
15void check_error(int b ) 
16{ 
17
18  {
19#line 11
20  if (b) {
21
22  } else {
23    {
24#line 11
25    __blast_assert();
26    }
27  }
28#line 12
29  return;
30}
31}
32#line 15 "files/test_while_int.c"
33int main(void) 
34{ int i ;
35  int __cil_tmp2 ;
36
37  {
38#line 16
39  i = 0;
40  {
41#line 17
42  while (1) {
43    while_continue: /* CIL Label */ ;
44#line 17
45    if (i < 5) {
46
47    } else {
48#line 17
49      goto while_break;
50    }
51    {
52#line 18
53    i = i + 1;
54#line 22
55    __cil_tmp2 = i != 3;
56#line 22
57    check_error(__cil_tmp2);
58    }
59  }
60  while_break: /* CIL Label */ ;
61  }
62#line 25
63  return (0);
64}
65}
↑