Replace goto_symext::options with const members

goto_symext no longer has a reference to a optionst object. Instead, the
options that goto_symext needs to read from an optionst are read during
construction and cached in const members.

Author: karkhaz

src/goto-symex/goto_symex.cpp

@@ -18,7 +18,7 @@ unsigned goto_symext::dynamic_counter=0;
 
 void goto_symext::do_simplify(exprt &expr)
 {
-  if(options.get_bool_option("simplify"))
+  if(simplify_opt)
     simplify(expr, ns);
 }
 

src/goto-symex/goto_symex.h

@@ -55,7 +55,6 @@ class goto_symext
     const optionst &options,
     path_storaget &path_storage)
     : should_pause_symex(false),
-      options(options),
       max_depth(options.get_unsigned_int_option("depth")),
       doing_path_exploration(options.is_set("paths")),
       allow_pointer_unsoundness(
@@ -64,6 +63,10 @@ class goto_symext
       constant_propagation(options.get_bool_option("propagation")),
       self_loops_to_assumptions(
         options.get_bool_option("self-loops-to-assumptions")),
+      simplify_opt(options.get_bool_option("simplify")),
+      unwinding_assertions(options.get_bool_option("unwinding-assertions")),
+      partial_loops(options.get_bool_option("partial-loops")),
+      debug_level(options.get_option("debug-level")),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
       target(_target),
@@ -201,8 +204,6 @@ class goto_symext
     const get_goto_functiont &,
     statet &);
 
-  const optionst &options;
-
   const unsigned max_depth;
   const bool doing_path_exploration;
   const bool allow_pointer_unsoundness;
@@ -218,6 +219,10 @@ class goto_symext
 protected:
   const bool constant_propagation;
   const bool self_loops_to_assumptions;
+  const bool simplify_opt;
+  const bool unwinding_assertions;
+  const bool partial_loops;
+  const std::string debug_level;
 
   /// The symbol table associated with the goto-program that we're
   /// executing. This symbol table will not additionally contain objects

src/goto-symex/symex_assign.cpp

@@ -247,7 +247,7 @@ void goto_symext::symex_assign_symbol(
     ssa_lhs,
     ssa_rhs,
     ns,
-    options.get_bool_option("simplify"),
+    simplify_opt,
     constant_propagation,
     allow_pointer_unsoundness);
 

src/goto-symex/symex_builtin_functions.cpp

@@ -458,7 +458,7 @@ void goto_symext::symex_trace(
 {
   PRECONDITION(code.arguments().size() >= 2);
 
-  int debug_thresh=unsafe_string2int(options.get_option("debug-level"));
+  int debug_thresh = unsafe_string2int(debug_level);
 
   mp_integer debug_lvl;
   optionalt<mp_integer> maybe_debug =

src/goto-symex/symex_dereference.cpp

@@ -281,7 +281,6 @@ void goto_symext::dereference_rec(
     value_set_dereferencet dereference(
       ns,
       state.symbol_table,
-      options,
       symex_dereference_state,
       language_mode,
       expr_is_not_null);

src/goto-symex/symex_function_call.cpp

@@ -236,13 +236,13 @@ void goto_symext::symex_function_call_code(
   // see if it's too much
   if(stop_recursing)
   {
-    if(options.get_bool_option("partial-loops"))
+    if(partial_loops)
     {
       // it's ok, ignore
     }
     else
     {
-      if(options.get_bool_option("unwinding-assertions"))
+      if(unwinding_assertions)
         vcc(false_exprt(), "recursion unwinding assertion", state);
 
       // add to state guard to prevent further assignments

src/goto-symex/symex_goto.cpp

@@ -515,12 +515,6 @@ void goto_symext::loop_bound_exceeded(
   else
     negated_cond=not_exprt(guard);
 
-  bool unwinding_assertions=
-    options.get_bool_option("unwinding-assertions");
-
-  bool partial_loops=
-    options.get_bool_option("partial-loops");
-
   if(!partial_loops)
   {
     if(unwinding_assertions)

src/pointer-analysis/goto_program_dereference.h

@@ -30,13 +30,13 @@ class goto_program_dereferencet:protected dereference_callbackt
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     const optionst &_options,
-    value_setst &_value_sets):
-    options(_options),
-    ns(_ns),
-    value_sets(_value_sets),
-    dereference(_ns, _new_symbol_table, _options, *this, ID_nil, false)
-    {
-    }
+    value_setst &_value_sets)
+    : options(_options),
+      ns(_ns),
+      value_sets(_value_sets),
+      dereference(_ns, _new_symbol_table, *this, ID_nil, false)
+  {
+  }
 
   void dereference_program(
     goto_programt &goto_program,

src/pointer-analysis/value_set_dereference.h

@@ -32,8 +32,6 @@ class value_set_dereferencet
   /*! \brief Constructor
    * \param _ns Namespace
    * \param _new_symbol_table A symbol_table to store new symbols in
-   * \param _options Options, in particular whether pointer checks are
-            to be performed
    * \param _dereference_callback Callback object for error reporting
    * \param _language_mode Mode for any new symbols created to represent
             a dereference failure
@@ -43,13 +41,11 @@ class value_set_dereferencet
   value_set_dereferencet(
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
-    const optionst &_options,
     dereference_callbackt &_dereference_callback,
     const irep_idt _language_mode,
     bool _exclude_null_derefs):
     ns(_ns),
     new_symbol_table(_new_symbol_table),
-    options(_options),
     dereference_callback(_dereference_callback),
     language_mode(_language_mode),
     exclude_null_derefs(_exclude_null_derefs)
@@ -83,7 +79,6 @@ class value_set_dereferencet
 private:
   const namespacet &ns;
   symbol_tablet &new_symbol_table;
-  const optionst &options;
   dereference_callbackt &dereference_callback;
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.