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.
NathanJPhillips · Jun 1, 2018 · e77cabc · e77cabc
1 parent 34a3d85
commit e77cabc
Show file tree

Hide file tree

Showing 6 changed files with 25 additions and 9 deletions.
diff --git a/src/cbmc/bmc.cpp b/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;

diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
@@ -76,7 +76,12 @@ 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)
@@ -148,7 +153,12 @@ 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)

diff --git a/src/cbmc/symex_bmc.cpp b/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)
 {

diff --git a/src/cbmc/symex_bmc.h b/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

diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h
@@ -43,12 +43,16 @@ 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)
   {
+    // Unconditionally set for performance reasons. This option setting applies
+    // only to this program.
+    options.set_option("simplify", true);
   }
 
   void append(goto_programt::instructionst &instructions);
@@ -80,6 +84,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;

diff --git a/src/goto-symex/goto_symex.h b/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;