Showing error 124

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/callfpointer.c-unsafe.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 5 "files/callfpointer.c"
 5void f(void (*g)(int  ) ) 
 6{ 
 7
 8  {
 9  {
10#line 6
11  (*g)(1);
12  }
13#line 7
14  return;
15}
16}
17#line 9 "files/callfpointer.c"
18void h(int i ) 
19{ 
20
21  {
22#line 10
23  if (i == 1) {
24    ERROR:assert(0); 
25#line 11
26    goto ERROR;
27  } else {
28
29  }
30#line 15
31  return;
32}
33}
34#line 16 "files/callfpointer.c"
35int main(void) 
36{ 
37
38  {
39  {
40#line 17
41  f(& h);
42  }
43#line 19
44  return (0);
45}
46}
↑