Make goto_symext::language_mode protected

This should be set via constructors. Remove bmc_util/setup_symex as all
work is done through constructors.

Author: tautschnig

src/goto-checker/bmc_util.cpp

@@ -11,7 +11,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "bmc_util.h"
 
-#include <iostream>
+#include <util/json_stream.h>
+#include <util/ui_message.h>
 
 #include <goto-programs/graphml_witness.h>
 #include <goto-programs/json_goto_trace.h>
@@ -21,17 +22,13 @@ Author: Daniel Kroening, Peter Schrammel
 #include <goto-symex/memory_model_pso.h>
 #include <goto-symex/slice.h>
 #include <goto-symex/symex_target_equation.h>
-
-#include <linking/static_lifetime_init.h>
-
 #include <solvers/decision_procedure.h>
 
-#include <util/json_stream.h>
-#include <util/ui_message.h>
-
 #include "goto_symex_property_decider.h"
 #include "symex_bmc.h"
 
+#include <iostream>
+
 void message_building_error_trace(messaget &log)
 {
   log.status() << "Building error trace" << messaget::eom;
@@ -175,21 +172,6 @@ get_memory_model(const optionst &options, const namespacet &ns)
   }
 }
 
-void setup_symex(
-  symex_bmct &symex,
-  const namespacet &ns,
-  ui_message_handlert &ui_message_handler)
-{
-  messaget msg(ui_message_handler);
-  const symbolt *init_symbol;
-  if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
-    symex.language_mode = init_symbol->mode;
-
-  msg.status() << "Starting Bounded Model Checking" << messaget::eom;
-
-  symex.last_source_location.make_nil();
-}
-
 void slice(
   symex_bmct &symex,
   symex_target_equationt &symex_target_equation,

src/goto-checker/bmc_util.h

@@ -69,8 +69,6 @@ void output_graphml(
 std::unique_ptr<memory_model_baset>
 get_memory_model(const optionst &options, const namespacet &);
 
-void setup_symex(symex_bmct &, const namespacet &, ui_message_handlert &);
-
 void slice(
   symex_bmct &,
   symex_target_equationt &symex_target_equation,

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -39,7 +39,6 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
   unwindset.parse_unwind(options.get_option("unwind"));
   unwindset.parse_unwindset(
     options.get_list_option("unwindset"), goto_model, ui_message_handler);
-  setup_symex(symex, ns, ui_message_handler);
 }
 
 incremental_goto_checkert::resultt multi_path_symex_only_checkert::

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -42,7 +42,6 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
   unwindset.parse_unwind(options.get_option("unwind"));
   unwindset.parse_unwindset(
     options.get_list_option("unwindset"), goto_model, ui_message_handler);
-  setup_symex(symex, ns, ui_message_handler);
 
   // Freeze all symbols if we are using a prop_conv_solvert
   prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(

src/goto-checker/single_path_symex_only_checker.cpp

@@ -152,11 +152,6 @@ void single_path_symex_only_checkert::equation_output(
   }
 }
 
-void single_path_symex_only_checkert::setup_symex(symex_bmct &symex)
-{
-  ::setup_symex(symex, ns, ui_message_handler);
-}
-
 void single_path_symex_only_checkert::update_properties(
   propertiest &properties,
   std::unordered_set<irep_idt> &updated_properties,

src/goto-checker/single_path_symex_only_checker.h

@@ -48,7 +48,10 @@ class single_path_symex_only_checkert : public incremental_goto_checkert
     const symex_bmct &symex,
     const symex_target_equationt &equation);
 
-  virtual void setup_symex(symex_bmct &symex);
+  virtual void setup_symex(symex_bmct &symex)
+  {
+    // deriving classes may do extra work here
+  }
 
   /// Adds the initial goto-symex state as a path to the worklist
   virtual void initialize_worklist();

src/goto-checker/symex_bmc.cpp

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/unwindset.h>
 
+#include <linking/static_lifetime_init.h>
+
 #include <limits>
 
 symex_bmct::symex_bmct(
@@ -33,10 +35,17 @@ symex_bmct::symex_bmct(
       options,
       path_storage,
       guard_manager),
+    last_source_location(source_locationt::nil()),
     record_coverage(!options.get_option("symex-coverage-report").empty()),
     unwindset(unwindset),
     symex_coverage(ns)
 {
+  const symbolt *init_symbol = outer_symbol_table.lookup(INITIALIZE_FUNCTION);
+  if(init_symbol)
+    language_mode = init_symbol->mode;
+
+  messaget msg{mh};
+  msg.status() << "Starting Bounded Model Checking" << messaget::eom;
 }
 
 /// show progress

src/goto-symex/goto_symex.h

@@ -235,13 +235,10 @@ class goto_symext
   messaget::mstreamt &
   print_callstack_entry(const symex_targett::sourcet &target);
 
-public:
-
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.
   irep_idt language_mode;
 
-protected:
   /// The symbol table associated with the goto-program being executed.
   /// This symbol table will not have objects that are dynamically created as
   /// part of symbolic execution added to it; those object are stored in the

unit/path_strategies.cpp

@@ -425,7 +425,6 @@ void _check_with_strategy(
       *worklist,
       guard_manager,
       unwindset);
-    setup_symex(symex, ns, ui_message_handler);
 
     symex.initialize_path_storage_from_entry_point_of(
       goto_symext::get_goto_function(goto_model),
@@ -448,7 +447,6 @@ void _check_with_strategy(
       *worklist,
       guard_manager,
       unwindset);
-    setup_symex(symex, ns, ui_message_handler);
 
     symex_symbol_table = symex.resume_symex_from_saved_state(
       goto_symext::get_goto_function(goto_model),