Skip to content

Commit

Permalink
jbmc, janalyzer: Remove unnecessary dynamic_cast
Browse files Browse the repository at this point in the history
`lazy_goto_modelt::process_whole_model_and_freeze` returns a unique
pointer to `goto_modelt`, which these call sites unnecessarily
generalised to `abstract_goto_modelt` (just to then `dynamic_cast` it to
`goto_modelt`). Fix the local pointer types and remove the now no longer
necessary cast.
  • Loading branch information
tautschnig committed Aug 20, 2024
1 parent b87d38a commit 08f611e
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 5 deletions.
4 changes: 2 additions & 2 deletions jbmc/src/janalyzer/janalyzer_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -401,13 +401,13 @@ int janalyzer_parse_optionst::doit()
log.status() << "Generating GOTO Program" << messaget::eom;
lazy_goto_model.load_all_functions();

std::unique_ptr<abstract_goto_modelt> goto_model_ptr =
std::unique_ptr<goto_modelt> goto_model_ptr =
lazy_goto_modelt::process_whole_model_and_freeze(
std::move(lazy_goto_model));
if(goto_model_ptr == nullptr)
return CPROVER_EXIT_INTERNAL_ERROR;

goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
goto_modelt &goto_model = *goto_model_ptr;

// show it?
if(cmdline.isset("show-symbol-table"))
Expand Down
6 changes: 3 additions & 3 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -474,7 +474,7 @@ int jbmc_parse_optionst::doit()
stub_objects_are_not_null =
options.get_bool_option("java-assume-inputs-non-null");

std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
std::unique_ptr<goto_modelt> goto_model_ptr;
int get_goto_program_ret = get_goto_program(goto_model_ptr, options);
if(get_goto_program_ret != -1)
return get_goto_program_ret;
Expand Down Expand Up @@ -594,7 +594,7 @@ int jbmc_parse_optionst::doit()
}

int jbmc_parse_optionst::get_goto_program(
std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
std::unique_ptr<goto_modelt> &goto_model_ptr,
const optionst &options)
{
if(options.is_set("context-include") || options.is_set("context-exclude"))
Expand Down Expand Up @@ -633,7 +633,7 @@ int jbmc_parse_optionst::get_goto_program(
if(goto_model_ptr == nullptr)
return CPROVER_EXIT_INTERNAL_ERROR;

goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
goto_modelt &goto_model = *goto_model_ptr;

if(cmdline.isset("validate-goto-model"))
{
Expand Down

0 comments on commit 08f611e

Please sign in to comment.