Skip to content

Commit ac41f93

Browse files
smowtoncristina-david
authored andcommitted
Use remove_instanceof in driver programs
This adds a remove_instanceof call wherever there was an existing remove_virtual_functions call.
1 parent c8c9085 commit ac41f93

File tree

3 files changed

+2
-3
lines changed

3 files changed

+2
-3
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -894,7 +894,7 @@ bool cbmc_parse_optionst::process_goto_program(
894894
cmdline.isset("pointer-check"));
895895
// Java virtual functions -> explicit dispatch tables:
896896
remove_virtual_functions(symbol_table, goto_functions);
897-
// Java instanceof -> clsid comparison:
897+
// Similar removal of RTTI inspection:
898898
remove_instanceof(symbol_table, goto_functions);
899899

900900
// full slice?

src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -387,7 +387,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
387387
remove_function_pointers(goto_model, cmdline.isset("pointer-check"));
388388
// Java virtual functions -> explicit dispatch tables:
389389
remove_virtual_functions(goto_model);
390-
// Java instanceof -> clsid comparison:
390+
// remove rtti
391391
remove_instanceof(goto_model);
392392

393393
// do partial inlining

src/symex/symex_parse_options.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -369,7 +369,6 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
369369
remove_vector(goto_model);
370370
// Java virtual functions -> explicit dispatch tables:
371371
remove_virtual_functions(goto_model);
372-
// Java instanceof -> clsid comparison:
373372
remove_instanceof(goto_model);
374373
rewrite_union(goto_model);
375374
adjust_float_expressions(goto_model);

0 commit comments

Comments
 (0)