Skip to content

Commit 185206c

Browse files
author
Daniel Kroening
committed
cbmc cleanup
1 parent d542f7e commit 185206c

File tree

2 files changed

+0
-4
lines changed

2 files changed

+0
-4
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,6 @@ Author: Daniel Kroening, [email protected]
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

src/cbmc/cbmc_parse_options.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff 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)" \

0 commit comments

Comments
 (0)