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 3877e0f commit 3fef02a
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 6 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
12 changes: 8 additions & 4 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -628,12 +628,16 @@ int jbmc_parse_optionst::get_goto_program(

// Move the model out of the local lazy_goto_model
// and into the caller's goto_model
goto_model_ptr = lazy_goto_modelt::process_whole_model_and_freeze(
std::move(lazy_goto_model));
if(goto_model_ptr == nullptr)
auto final_goto_model_ptr =
lazy_goto_modelt::process_whole_model_and_freeze(

Check warning on line 632 in jbmc/src/jbmc/jbmc_parse_options.cpp

View check run for this annotation

Codecov / codecov/patch

jbmc/src/jbmc/jbmc_parse_options.cpp#L632

Added line #L632 was not covered by tests
std::move(lazy_goto_model));
if(final_goto_model_ptr == nullptr)
return CPROVER_EXIT_INTERNAL_ERROR;

goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
goto_modelt &goto_model = *final_goto_model_ptr;
goto_model_ptr =
std::unique_ptr<abstract_goto_modelt>(final_goto_model_ptr.get());
final_goto_model_ptr.release();

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

0 comments on commit 3fef02a

Please sign in to comment.