From 3fef02a35d79b12a64561abbbb4b7c44b1fdca7f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 09:16:32 +0000 Subject: [PATCH] jbmc, janalyzer: Remove unnecessary dynamic_cast `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. --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 4 ++-- jbmc/src/jbmc/jbmc_parse_options.cpp | 12 ++++++++---- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 4c63681b1eb..79b712d55d1 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -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 goto_model_ptr = + std::unique_ptr 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_model_ptr); + goto_modelt &goto_model = *goto_model_ptr; // show it? if(cmdline.isset("show-symbol-table")) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 1ae828e5341..7ed4105af63 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -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( + std::move(lazy_goto_model)); + if(final_goto_model_ptr == nullptr) return CPROVER_EXIT_INTERNAL_ERROR; - goto_modelt &goto_model = dynamic_cast(*goto_model_ptr); + goto_modelt &goto_model = *final_goto_model_ptr; + goto_model_ptr = + std::unique_ptr(final_goto_model_ptr.get()); + final_goto_model_ptr.release(); if(cmdline.isset("validate-goto-model")) {