Skip to content

Commit fae3cd8

Browse files
author
Daniel Kroening
authored
Merge pull request #519 from thk123/feature/clean-fp-removal
Clean Const Function Pointer Removal
2 parents bf08eee + d7c15ae commit fae3cd8

File tree

151 files changed

+4993
-44
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

151 files changed

+4993
-44
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
const void_fp fp_tbl[] = {f2, f3 ,f4};
16+
17+
// There is a basic check that excludes all functions that aren't used anywhere
18+
// This ensures that check can't work in this example
19+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
20+
21+
void func(int i)
22+
{
23+
fp_tbl[i]();
24+
}
25+
26+
int main()
27+
{
28+
for(int i=0;i<3;i++)
29+
{
30+
func(i);
31+
}
32+
33+
return 0;
34+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions --verbosity 10 --pointer-check
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp_tbl\[\(signed long int\)i\] == f2 THEN GOTO [0-9]$
7+
^\s*IF fp_tbl\[\(signed long int\)i\] == f3 THEN GOTO [0-9]$
8+
^\s*IF fp_tbl\[\(signed long int\)i\] == f4 THEN GOTO [0-9]$
9+
^SIGNAL=0$
10+
--
11+
^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
12+
^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
16+
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
17+
^warning: ignoring
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
// There is a basic check that excludes all functions that aren't used anywhere
16+
// This ensures that check can't work in this example
17+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
18+
19+
void(* const fp_tbl[3])(void) =
20+
{
21+
(void(*)())f2,
22+
(void(*)())f3,
23+
(void(*)())f4,
24+
};
25+
26+
27+
void func(int i)
28+
{
29+
const void_fp fp = fp_tbl[i];
30+
fp();
31+
}
32+
33+
int main()
34+
{
35+
for(int i=0;i<3;i++)
36+
{
37+
func(i);
38+
}
39+
40+
return 0;
41+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions --verbosity 10 --pointer-check
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp == f2 THEN GOTO [0-9]$
7+
^\s*IF fp == f3 THEN GOTO [0-9]$
8+
^\s*IF fp == f4 THEN GOTO [0-9]$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
16+
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
17+
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
const void_fp fp_tbl[] = {f2, f3 ,f4, 0};
16+
17+
// There is a basic check that excludes all functions that aren't used anywhere
18+
// This ensures that check can't work in this example
19+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
20+
21+
void func(int i)
22+
{
23+
const void_fp fp = fp_tbl[i];
24+
fp();
25+
}
26+
27+
int main()
28+
{
29+
for(int i=0;i<3;i++)
30+
{
31+
func(i);
32+
}
33+
34+
return 0;
35+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions --verbosity 10 --pointer-check
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp == f2 THEN GOTO [0-9]$
7+
^\s*IF fp == f3 THEN GOTO [0-9]$
8+
^\s*IF fp == f4 THEN GOTO [0-9]$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
16+
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
17+
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
const void_fp fp_tbl[] = {f2, f3 ,f4};
16+
17+
// There is a basic check that excludes all functions that aren't used anywhere
18+
// This ensures that check can't work in this example
19+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
20+
21+
void func(int i)
22+
{
23+
const void_fp fp = fp_tbl[i];
24+
fp();
25+
}
26+
27+
int main()
28+
{
29+
for(int i=0;i<3;i++)
30+
{
31+
func(i);
32+
}
33+
34+
return 0;
35+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions --verbosity 10 --pointer-check
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp == f2 THEN GOTO [0-9]$
7+
^\s*IF fp == f3 THEN GOTO [0-9]$
8+
^\s*IF fp == f4 THEN GOTO [0-9]$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
16+
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
17+
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
struct action
16+
{
17+
void_fp fun;
18+
};
19+
20+
const struct action rec = { .fun = f2 };
21+
const struct action rec2 = { .fun = f3 };
22+
const struct action rec3 = { .fun = f4 };
23+
24+
const struct action * const action_list[4] =
25+
{
26+
&rec,
27+
&rec2,
28+
&rec3,
29+
&rec
30+
};
31+
32+
// There is a basic check that excludes all functions that aren't used anywhere
33+
// This ensures that check can't work in this example
34+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
35+
36+
void func(int i)
37+
{
38+
const void_fp fp = action_list[i]->fun;
39+
fp();
40+
}
41+
42+
int main()
43+
{
44+
for(int i=0;i<3;i++)
45+
{
46+
func(i);
47+
}
48+
49+
return 0;
50+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions --verbosity 10 --pointer-check
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp == f2 THEN GOTO [0-9]$
7+
^\s*IF fp == f3 THEN GOTO [0-9]$
8+
^\s*IF fp == f4 THEN GOTO [0-9]$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
16+
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
17+
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
// There is a basic check that excludes all functions that aren't used anywhere
16+
// This ensures that check can't work in this example
17+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
18+
19+
struct stable
20+
{
21+
int x;
22+
void (*fp)(void);
23+
};
24+
25+
const struct stable stable_table [3] =
26+
{
27+
{ 1, f2 },
28+
{ 2, f3 },
29+
{ 3, f4 }
30+
};
31+
32+
const struct stable another_table = { 4, f5 };
33+
34+
35+
void func(int i)
36+
{
37+
const void_fp fp = stable_table[i].fp;
38+
39+
// Illegal
40+
// stable_table[1] = another_table;
41+
fp();
42+
}
43+
44+
int main()
45+
{
46+
for(int i=0;i<3;i++)
47+
{
48+
func(i);
49+
}
50+
return 0;
51+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions --verbosity 10 --pointer-check
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp == f2 THEN GOTO [0-9]$
7+
^\s*IF fp == f3 THEN GOTO [0-9]$
8+
^\s*IF fp == f4 THEN GOTO [0-9]$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
16+
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
17+
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$

0 commit comments

Comments
 (0)