Remove optionst member from goto_symext

goto_symext now has a const reference rather than owning a member. There
is no need to copy an optionst by value from bmct.

Author: karkhaz

src/cbmc/bmc.cpp

@@ -305,7 +305,6 @@ void bmct::get_memory_model()
 void bmct::setup()
 {
   get_memory_model();
-  symex.options=options;
 
   {
     const symbolt *init_symbol;
@@ -561,7 +560,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
 ///   See class member `bmct::driver_callback_after_symex` for details.
 int bmct::do_language_agnostic_bmc(
   const path_strategy_choosert &path_strategy_chooser,
-  const optionst &opts,
+  optionst &opts,
   abstract_goto_modelt &model,
   const ui_message_handlert::uit &ui,
   messaget &message,

src/cbmc/bmc.h

@@ -64,7 +64,7 @@ class bmct:public safety_checkert
   ///   `path_storage` and using it to construct a path_explorert
   ///   object.
   bmct(
-    const optionst &_options,
+    optionst &_options,
     const symbol_tablet &outer_symbol_table,
     message_handlert &_message_handler,
     prop_convt &_prop_conv,
@@ -76,14 +76,21 @@ class bmct:public safety_checkert
       ns(outer_symbol_table, symex_symbol_table),
       equation(),
       path_storage(_path_storage),
-      symex(_message_handler, outer_symbol_table, equation, path_storage),
+      symex(
+        _message_handler,
+        outer_symbol_table,
+        equation,
+        options,
+        path_storage),
       prop_conv(_prop_conv),
       ui(ui_message_handlert::uit::PLAIN),
       driver_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation=options.get_bool_option("propagation");
     symex.record_coverage=
       !options.get_option("symex-coverage-report").empty();
+    options.set_option("simplify", true);
+    options.set_option("assertions", true);
   }
 
   virtual resultt run(const goto_functionst &goto_functions)
@@ -118,7 +125,7 @@ class bmct:public safety_checkert
 
   static int do_language_agnostic_bmc(
     const path_strategy_choosert &path_strategy_chooser,
-    const optionst &opts,
+    optionst &opts,
     abstract_goto_modelt &goto_model,
     const ui_message_handlert::uit &ui,
     messaget &message,
@@ -135,7 +142,7 @@ class bmct:public safety_checkert
   /// symex_target_equationt. See the documentation for path_explorert for
   /// details.
   bmct(
-    const optionst &_options,
+    optionst &_options,
     const symbol_tablet &outer_symbol_table,
     message_handlert &_message_handler,
     prop_convt &_prop_conv,
@@ -148,21 +155,28 @@ class bmct:public safety_checkert
       ns(outer_symbol_table),
       equation(_equation),
       path_storage(_path_storage),
-      symex(_message_handler, outer_symbol_table, equation, path_storage),
+      symex(
+        _message_handler,
+        outer_symbol_table,
+        equation,
+        options,
+        path_storage),
       prop_conv(_prop_conv),
       ui(ui_message_handlert::uit::PLAIN),
       driver_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation = options.get_bool_option("propagation");
     symex.record_coverage =
       !options.get_option("symex-coverage-report").empty();
+    options.set_option("simplify", true);
+    options.set_option("assertions", true);
     INVARIANT(
       options.get_bool_option("paths"),
       "Should only use saved equation & goto_state constructor "
       "when doing path exploration");
   }
 
-  const optionst &options;
+  optionst &options;
   /// \brief symbol table for the goto-program that we will execute
   const symbol_tablet &outer_symbol_table;
   /// \brief symbol table generated during symbolic execution
@@ -252,7 +266,7 @@ class path_explorert : public bmct
 {
 public:
   path_explorert(
-    const optionst &_options,
+    optionst &_options,
     const symbol_tablet &outer_symbol_table,
     message_handlert &_message_handler,
     prop_convt &_prop_conv,

src/cbmc/symex_bmc.cpp

@@ -22,8 +22,9 @@ symex_bmct::symex_bmct(
   message_handlert &mh,
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &_target,
+  const optionst &options,
   path_storaget &path_storage)
-  : goto_symext(mh, outer_symbol_table, _target, path_storage),
+  : goto_symext(mh, outer_symbol_table, _target, options, path_storage),
     record_coverage(false),
     symex_coverage(ns)
 {

src/cbmc/symex_bmc.h

@@ -29,6 +29,7 @@ class symex_bmct: public goto_symext
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
+    const optionst &options,
     path_storaget &path_storage);
 
   // To show progress

src/goto-instrument/accelerate/scratch_program.h

@@ -43,12 +43,15 @@ class scratch_programt:public goto_programt
       ns(symbol_table, symex_symbol_table),
       equation(),
       path_storage(),
-      symex(mh, symbol_table, equation, path_storage),
+      options(),
+      symex(mh, symbol_table, equation, options, path_storage),
       satcheck(util_make_unique<satcheckt>()),
       satchecker(ns, *satcheck),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
       checker(&z3) // checker(&satchecker)
   {
+    options.set_option("simplify", true);
+    options.set_option("assertions", true);
   }
 
   void append(goto_programt::instructionst &instructions);
@@ -80,6 +83,7 @@ class scratch_programt:public goto_programt
   namespacet ns;
   symex_target_equationt equation;
   path_fifot path_storage;
+  optionst options;
   goto_symext symex;
 
   std::unique_ptr<propt> satcheck;

src/goto-symex/goto_symex.h

@@ -52,8 +52,10 @@ class goto_symext
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
+    const optionst &options,
     path_storaget &path_storage)
     : should_pause_symex(false),
+      options(options),
       total_vccs(0),
       remaining_vccs(0),
       constant_propagation(true),
@@ -66,8 +68,6 @@ class goto_symext
       guard_identifier("goto_symex::\\guard"),
       path_storage(path_storage)
   {
-    options.set_option("simplify", true);
-    options.set_option("assertions", true);
   }
 
   virtual ~goto_symext()
@@ -194,6 +194,8 @@ class goto_symext
     const get_goto_functiont &,
     statet &);
 
+  const optionst &options;
+
 public:
   // these bypass the target maps
   virtual void symex_step_goto(statet &, bool taken);
@@ -203,8 +205,6 @@ class goto_symext
 
   bool constant_propagation;
 
-  optionst options;
-
   /// 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;