Merge pull request #8418 from tautschnig/lazy_goto_model-no-dynamic_cast

jbmc, janalyzer: Remove unnecessary dynamic_cast
diffblue · Sep 12, 2024 · f0543bd · f0543bd
2 parents a29e933 + 3fef02a
commit f0543bd
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 6 deletions.
diff --git 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<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"))

diff --git 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_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"))
     {