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.
diffblue · Aug 20, 2024 · f4e049c · f4e049c
1 parent 3877e0f
commit f4e049c
Show file tree

Hide file tree

Showing 3 changed files with 6 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
@@ -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;
@@ -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"))
@@ -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"))
     {

diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -127,7 +127,7 @@ class jbmc_parse_optionst : public parse_options_baset
 
   void get_command_line_options(optionst &);
   int get_goto_program(
-    std::unique_ptr<abstract_goto_modelt> &goto_model,
+    std::unique_ptr<goto_modelt> &goto_model,
     const optionst &);
   bool show_loaded_functions(const abstract_goto_modelt &goto_model);
   bool show_loaded_symbols(const abstract_goto_modelt &goto_model);