move setup_unwind to parse_unwindset_options to prevent duplication

Author: Daniel Kroening

src/cbmc/bmc.cpp

@@ -15,8 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 
 #include <util/exit_codes.h>
-#include <util/string2int.h>
-#include <util/string_utils.h>
 
 #include <langapi/language_util.h>
 
@@ -319,7 +317,7 @@ void bmct::setup()
 
   symex.last_source_location.make_nil();
 
-    setup_unwind();
+  parse_unwinding_options(options, symex);
 }
 
 safety_checkert::resultt bmct::execute(
@@ -546,43 +544,6 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
   }
 }
 
-void bmct::setup_unwind()
-{
-  const std::string &set=options.get_option("unwindset");
-  std::vector<std::string> unwindset_loops;
-  split_string(set, ',', unwindset_loops, true, true);
-
-  for(auto &val : unwindset_loops)
-  {
-    unsigned thread_nr=0;
-    bool thread_nr_set=false;
-
-    if(!val.empty() &&
-       isdigit(val[0]) &&
-       val.find(":")!=std::string::npos)
-    {
-      std::string nr=val.substr(0, val.find(":"));
-      thread_nr=unsafe_string2unsigned(nr);
-      thread_nr_set=true;
-      val.erase(0, nr.size()+1);
-    }
-
-    if(val.rfind(":")!=std::string::npos)
-    {
-      std::string id=val.substr(0, val.rfind(":"));
-      long uw=unsafe_string2int(val.substr(val.rfind(":")+1));
-
-      if(thread_nr_set)
-        symex.set_unwind_thread_loop_limit(thread_nr, id, uw);
-      else
-        symex.set_unwind_loop_limit(id, uw);
-    }
-  }
-
-  if(options.get_option("unwind")!="")
-    symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
-}
-
 /// Perform core BMC, using an abstract model to supply GOTO function bodies
 /// (perhaps created on demand).
 /// \param opts: command-line options affecting BMC

src/cbmc/bmc.h

@@ -180,8 +180,6 @@ class bmct:public safety_checkert
     const goto_functionst &,
     prop_convt &);
 
-  // unwinding
-  virtual void setup_unwind();
   void do_conversion();
 
   virtual void freeze_program_variables();

src/cbmc/symex_bmc.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/source_location.h>
 #include <util/simplify_expr.h>
+#include <util/string_utils.h>
+#include <util/string2int.h>
 
 symex_bmct::symex_bmct(
   message_handlert &mh,
@@ -236,3 +238,42 @@ void symex_bmct::no_body(const irep_idt &identifier)
                   << log.eom;
   }
 }
+
+void parse_unwinding_options(
+  const optionst &options,
+  symex_bmct &symex)
+{
+  const std::string &set=options.get_option("unwindset");
+  std::vector<std::string> unwindset_loops;
+  split_string(set, ',', unwindset_loops, true, true);
+
+  for(auto &val : unwindset_loops)
+  {
+    unsigned thread_nr=0;
+    bool thread_nr_set=false;
+
+    if(!val.empty() &&
+       isdigit(val[0]) &&
+       val.find(":")!=std::string::npos)
+    {
+      std::string nr=val.substr(0, val.find(":"));
+      thread_nr=unsafe_string2unsigned(nr);
+      thread_nr_set=true;
+      val.erase(0, nr.size()+1);
+    }
+
+    if(val.rfind(":")!=std::string::npos)
+    {
+      std::string id=val.substr(0, val.rfind(":"));
+      long uw=unsafe_string2int(val.substr(val.rfind(":")+1));
+
+      if(thread_nr_set)
+        symex.set_unwind_thread_loop_limit(thread_nr, id, uw);
+      else
+        symex.set_unwind_loop_limit(id, uw);
+    }
+  }
+
+  if(options.get_option("unwind")!="")
+    symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
+}

src/cbmc/symex_bmc.h

@@ -152,4 +152,10 @@ class symex_bmct: public goto_symext
   symex_coveraget symex_coverage;
 };
 
+class optionst;
+
+void parse_unwinding_options(
+  const optionst &,
+  symex_bmct &);
+
 #endif // CPROVER_CBMC_SYMEX_BMC_H