Showing error 1364

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.i
Line in file: 16
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

 1# 1 "files/callfpointer.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/callfpointer.c"
 5
 6
 7
 8
 9
10void f(void g(int)) {
11 g(1);
12}
13
14void h(int i) {
15 if(i==1) {
16  ERROR: goto ERROR;
17 } else {
18
19 }
20}
21int main(void) {
22 f(h);
23
24 return 0;
25}
Show full sources