Skip to content

Commit 49c4b04

Browse files
author
thk123
committed
Adding tests for missing features
The function pointer optimsation can be further improved by dealing with things like structs and pointers to function pointers. More detail is outlined in diffblue#476
1 parent 991611b commit 49c4b04

File tree

6 files changed

+151
-0
lines changed

6 files changed

+151
-0
lines changed
Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
4+
void f1 (void) { printf("%i", 1); }
5+
void f2 (void) { printf("%i", 2); }
6+
void f3 (void) { printf("%i", 3); }
7+
void f4 (void) { printf("%i", 4); }
8+
void f5 (void) { printf("%i", 5); }
9+
void f6 (void) { printf("%i", 6); }
10+
void f7 (void) { printf("%i", 7); }
11+
void f8 (void) { printf("%i", 8); }
12+
void f9 (void) { printf("%i", 9); }
13+
14+
typedef void(*void_fp)(void);
15+
16+
// There is a basic check that excludes all functions that aren't used anywhere
17+
// This ensures that check can't work in this example
18+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
19+
20+
typedef struct fp_container
21+
{
22+
const void_fp fp_tbl[3];
23+
} fp_container;
24+
25+
26+
27+
void func(){
28+
fp_container container = { .fp_tbl = {f2 ,f3, f4} };
29+
fp_container container2 = { .fp_tbl = {f5 ,f6, f7} };
30+
// Illegal:
31+
// container = container2;
32+
void_fp fp = container.fp_tbl[1];
33+
fp();
34+
}
35+
36+
void main(){
37+
func();
38+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
KNOWNBUG
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*f3();$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
This test is marked as a KNOWNBUG as it is possible for the function
12+
pointer to be optimized away. Currently goto-analyzer falls back to
13+
assuming it could be any type compatible function.
14+
15+
Issue: https://github.com/diffblue/cbmc/issues/476
Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
4+
void f1 (void) { printf("%i", 1); }
5+
void f2 (void) { printf("%i", 2); }
6+
void f3 (void) { printf("%i", 3); }
7+
void f4 (void) { printf("%i", 4); }
8+
void f5 (void) { printf("%i", 5); }
9+
void f6 (void) { printf("%i", 6); }
10+
void f7 (void) { printf("%i", 7); }
11+
void f8 (void) { printf("%i", 8); }
12+
void f9 (void) { printf("%i", 9); }
13+
14+
typedef void(*void_fp)(void);
15+
16+
// There is a basic check that excludes all functions that aren't used anywhere
17+
// This ensures that check can't work in this example
18+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
19+
20+
typedef struct fp_container
21+
{
22+
void_fp fp_tbl[3];
23+
} fp_container;
24+
25+
26+
27+
void func(){
28+
const fp_container container = { .fp_tbl = {f2 ,f3, f4} };
29+
fp_container container2 = { .fp_tbl = {f5 ,f6, f7} };
30+
const void_fp alternatate_fp_tbl[] = {f5 ,f6, f7};
31+
// Illegal:
32+
// container = container2;
33+
// container.fp_tbl = alternatate_fp_tbl;
34+
void_fp fp = container.fp_tbl[1];
35+
fp();
36+
}
37+
38+
void main(){
39+
func();
40+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
KNOWNBUG
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*f3();$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
This test is marked as a KNOWNBUG as it is possible for the function
12+
pointer to be optimized away. Currently goto-analyzer falls back to
13+
assuming it could be any type compatible function.
14+
15+
Issue: https://github.com/diffblue/cbmc/issues/476
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
4+
void f1 (void) { printf("%i", 1); }
5+
void f2 (void) { printf("%i", 2); }
6+
void f3 (void) { printf("%i", 3); }
7+
void f4 (void) { printf("%i", 4); }
8+
void f5 (void) { printf("%i", 5); }
9+
void f6 (void) { printf("%i", 6); }
10+
void f7 (void) { printf("%i", 7); }
11+
void f8 (void) { printf("%i", 8); }
12+
void f9 (void) { printf("%i", 9); }
13+
14+
typedef void(*void_fp)(void);
15+
16+
// There is a basic check that excludes all functions that aren't used anywhere
17+
// This ensures that check can't work in this example
18+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
19+
20+
void func(){
21+
const void_fp fp = f3;
22+
const void_fp* p2fp = &fp;
23+
(*p2fp)();
24+
}
25+
26+
void main(){
27+
func();
28+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
KNOWNBUG
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*f3();$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
This test is marked as a KNOWNBUG as it is possible for the function
12+
pointer to be optimized away. Currently goto-analyzer falls back to
13+
assuming it could be any type compatible function.
14+
15+
Issue: https://github.com/diffblue/cbmc/issues/476

0 commit comments

Comments
 (0)