File tree Expand file tree Collapse file tree 2 files changed +0
-4
lines changed Expand file tree Collapse file tree 2 files changed +0
-4
lines changed Original file line number Diff line number Diff line change 3535#include < goto-programs/mm_io.h>
3636#include < goto-programs/read_goto_binary.h>
3737#include < goto-programs/remove_function_pointers.h>
38- #include < goto-programs/remove_virtual_functions.h>
3938#include < goto-programs/remove_instanceof.h>
4039#include < goto-programs/remove_returns.h>
4140#include < goto-programs/remove_exceptions.h>
@@ -745,8 +744,6 @@ bool cbmc_parse_optionst::process_goto_program(
745744 get_message_handler (),
746745 goto_model,
747746 cmdline.isset (" pointer-check" ));
748- // virtual functions -> explicit dispatch tables:
749- remove_virtual_functions (goto_model);
750747 // remove catch and throw (introduces instanceof)
751748 remove_exceptions (goto_model);
752749
Original file line number Diff line number Diff line change @@ -32,7 +32,6 @@ class optionst;
3232 " (document-subgoals)(outfile):(test-preprocessor)" \
3333 " D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \
3434 " (object-bits):" \
35- " (classpath):(cp):(main-class):" \
3635 " (depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
3736 OPT_GOTO_CHECK \
3837 " (no-assertions)(no-assumptions)" \
You can’t perform that action at this time.
0 commit comments