Skip to content

Commit 7ee921b

Browse files
committed
Complete MMIO rewrites before removing unused functions
__CPROVER_mm_io_{r,w} functions are unused until rewrites via mm_io are done, which is only done when processing the input program by CBMC. remove_unused_functions would spuriously remove the implementation of these function, even when they may be needed. Therefore, run mm_io instrumentation before removing unused functions.
1 parent 7162259 commit 7ee921b

File tree

2 files changed

+3
-1
lines changed

2 files changed

+3
-1
lines changed

Diff for: regression/cbmc/mm_io1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--no-standard-checks
4-
^Replaced MMIO operations: 3 reads, 1 writes
4+
^Replaced MMIO operations: 3 read\(s\), 1 write\(s\)
55
^EXIT=0$
66
^SIGNAL=0$
77
^VERIFICATION SUCCESSFUL$

Diff for: src/goto-instrument/goto_instrument_parse_options.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
2929
#include <goto-programs/label_function_pointer_call_sites.h>
3030
#include <goto-programs/link_to_library.h>
3131
#include <goto-programs/loop_ids.h>
32+
#include <goto-programs/mm_io.h>
3233
#include <goto-programs/parameter_assignments.h>
3334
#include <goto-programs/read_goto_binary.h>
3435
#include <goto-programs/remove_calls_no_body.h>
@@ -899,6 +900,7 @@ int goto_instrument_parse_optionst::doit()
899900
if(cmdline.isset("drop-unused-functions"))
900901
{
901902
do_indirect_call_and_rtti_removal();
903+
mm_io(goto_model, ui_message_handler);
902904

903905
log.status() << "Removing unused functions" << messaget::eom;
904906
remove_unused_functions(goto_model.goto_functions, ui_message_handler);

0 commit comments

Comments
 (0)