Skip to content

Commit 7e5922a

Browse files
committed
remove functions without a body
1 parent bc2c0cd commit 7e5922a

File tree

17 files changed

+315
-68
lines changed

17 files changed

+315
-68
lines changed
Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--inline
3+
--inline --remove-calls-no-body
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
@@ -9,4 +9,5 @@ main.c
99
^\s*a;$
1010
no body.*[`]f
1111
--
12+
f\(\)
1213
^warning: ignoring
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
void func1();
2+
3+
int main()
4+
{
5+
int ret;
6+
7+
func1();
8+
ret = func2();
9+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--inline
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
func1\(\)
8+
ret.*=.*func2\(\)
9+
no body for function.*func1
10+
no body for function.*func2
11+
--
12+
^warning: ignoring
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
void func1()
2+
{
3+
func2();
4+
}
5+
6+
int main()
7+
{
8+
func1();
9+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--function-inline func1
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
func1\(\)
8+
func2\(\)
9+
--
10+
^warning: ignoring
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
void func1();
2+
3+
void func3()
4+
{
5+
}
6+
7+
void func4()
8+
{
9+
func1();
10+
func2();
11+
}
12+
13+
void main()
14+
{
15+
func1();
16+
func2();
17+
func3();
18+
func4();
19+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--remove-calls-no-body
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
func3\(\)
8+
func4\(\)
9+
--
10+
func1\(\)
11+
func2\(\)
12+
^warning: ignoring
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
int func1(int arg1, int arg2);
2+
3+
void func3()
4+
{
5+
}
6+
7+
void func4()
8+
{
9+
func1(567, 285);
10+
func2();
11+
}
12+
13+
void main()
14+
{
15+
int ret1;
16+
17+
ret1 = func1(567, 285);
18+
func2();
19+
func3();
20+
func4();
21+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--remove-calls-no-body
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
func3\(\)
8+
func4\(\)
9+
567;
10+
285;
11+
ret1.*=.*NONDET
12+
--
13+
func1\(.*\)
14+
func2\(.*\)
15+
^warning: ignoring

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 21 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
2323

2424
#include <goto-programs/class_hierarchy.h>
2525
#include <goto-programs/goto_convert_functions.h>
26+
#include <goto-programs/remove_calls_no_body.h>
2627
#include <goto-programs/remove_function_pointers.h>
2728
#include <goto-programs/remove_virtual_functions.h>
2829
#include <goto-programs/remove_exceptions.h>
@@ -729,6 +730,10 @@ int goto_instrument_parse_optionst::doit()
729730
status() << "Performing full inlining" << eom;
730731
goto_inline(goto_model, get_message_handler());
731732

733+
status() << "Removing calls to functions without a body" << eom;
734+
remove_calls_no_bodyt remove_calls_no_body;
735+
remove_calls_no_body(goto_model.goto_functions);
736+
732737
status() << "Accelerating" << eom;
733738
accelerate_functions(
734739
goto_model, get_message_handler(), cmdline.isset("z3"));
@@ -992,7 +997,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
992997
// now do full inlining, if requested
993998
if(cmdline.isset("inline"))
994999
{
995-
do_indirect_call_and_rtti_removal(/*force=*/true);
1000+
do_indirect_call_and_rtti_removal(true);
9961001

9971002
if(cmdline.isset("show-custom-bitvector-analysis") ||
9981003
cmdline.isset("custom-bitvector-analysis"))
@@ -1113,10 +1118,21 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11131118
do_indirect_call_and_rtti_removal();
11141119

11151120
status() << "Partial inlining" << eom;
1116-
goto_partial_inline(goto_functions, ns, ui_message_handler, 0, true);
1121+
goto_partial_inline(goto_model, ui_message_handler, 0, true);
1122+
1123+
goto_model.goto_functions.update();
1124+
goto_model.goto_functions.compute_loop_numbers();
1125+
}
11171126

1118-
goto_functions.update();
1119-
goto_functions.compute_loop_numbers();
1127+
if(cmdline.isset("remove-calls-no-body"))
1128+
{
1129+
status() << "Removing calls to functions without a body" << eom;
1130+
1131+
remove_calls_no_bodyt remove_calls_no_body;
1132+
remove_calls_no_body(goto_model.goto_functions);
1133+
1134+
goto_model.goto_functions.update();
1135+
goto_model.goto_functions.compute_loop_numbers();
11201136
}
11211137

11221138
if(cmdline.isset("constant-propagator"))
@@ -1545,6 +1561,7 @@ void goto_instrument_parse_optionst::help()
15451561
" --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
15461562
" --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
15471563
" --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1564+
HELP_REMOVE_CALLS_NO_BODY
15481565
HELP_REMOVE_CONST_FUNCTION_POINTERS
15491566
" --add-library add models of C library functions\n"
15501567
" --model-argc-argv <n> model up to <n> command line arguments\n"

0 commit comments

Comments
 (0)