Merge pull request diffblue#145 from diffblue/nathan/feature/use-new-sss

Update for merge of master

Author: NathanJPhillips

cbmc

@@ -199,13 +199,9 @@ int sec_driver_parse_optionst::doit()
   register_languages();
   register_evs_pretty_printer();
 
-  goto_model.set_message_handler(get_message_handler());
-
   // Prevent generation of _start, which isn't necessary for our analysis
   // and can be costly:
-  goto_model.generate_start_function = false;
-
-  if(goto_model(cmdline))
+  if(initialize_goto_model(goto_model, cmdline, false, get_message_handler()))
     return 6;
 
   if(process_goto_program(options))

src/driver/sec_driver_parse_options.cpp

@@ -14,7 +14,7 @@ Author: Chris Smowton, [email protected]
 
 #include <langapi/language_ui.h>
 
-#include <goto-programs/get_goto_model.h>
+#include <goto-programs/initialize_goto_model.h>
 
 class bmct;
 class goto_functionst;
@@ -57,7 +57,7 @@ class sec_driver_parse_optionst final:
 
 private:
   ui_message_handlert ui_message_handler;
-  get_goto_modelt goto_model;
+  goto_modelt goto_model;
 
   void register_languages();
 

src/driver/sec_driver_parse_options.h

@@ -1510,8 +1510,7 @@ void taint_algorithm_computing_summary_of_functiont::
     it!=itend;
     ++it)
   {
-    goto_programt::const_targetst succs;
-    fn_to_summarise.body.get_successors(it,succs);
+    goto_programt::const_targetst succs=fn_to_summarise.body.get_successors(it);
     for(auto succit : succs)
       inst_predecessors[succit].push_back(it);
   }
@@ -1558,8 +1557,8 @@ void taint_algorithm_computing_summary_of_functiont::
         lvsa,
         summary->transition_props);
 
-    goto_programt::const_targetst successors;
-    fn_to_summarise.body.get_successors(src_instr_it, successors);
+    goto_programt::const_targetst successors=
+      fn_to_summarise.body.get_successors(src_instr_it);
     for(auto  succ_it = successors.begin();
       succ_it != successors.end();
       ++succ_it)

src/taint-analysis/taint_summary.cpp

@@ -277,10 +277,10 @@ static void  taint_collect_successors_inside_function(
       goto_model.goto_functions.function_map.at(
           elem.get_name_of_function()
           );
-  goto_programt::const_targetst  succ_targets;
-  fn.body.get_successors(elem.get_instruction_iterator(),succ_targets);
-  std::unordered_set<std::size_t>  processed_locations;
-  for (goto_programt::const_targett  succ_target : succ_targets)
+  goto_programt::const_targetst  succ_targets=
+    fn.body.get_successors(elem.get_instruction_iterator());
+  std::unordered_set<std::size_t> processed_locations;
+  for(goto_programt::const_targett succ_target : succ_targets)
   {
     if (0UL == trace.count(elem.get_name_of_function(),succ_target) &&
         0UL == processed_locations.count(succ_target->location_number))
@@ -378,8 +378,7 @@ static void populate_local_distances_to_taint_sink(
   std::map<instruction_iteratort, std::list<instruction_iteratort> > preds;
   for(auto it=prog.instructions.begin(),itend=prog.instructions.end(); it!=itend; ++it)
   {
-    std::list<instruction_iteratort> succs;
-    prog.get_successors(it,succs);
+    std::list<instruction_iteratort> succs=prog.get_successors(it);
     for(auto succ : succs)
       preds[succ].push_back(it);    
   }

src/taint-analysis/taint_trace_recogniser.cpp

@@ -122,8 +122,10 @@ taint_instrumentert::taint_instrumentert(
   for(const auto &loc : props.get_location_props())
   {
     const auto &id=loc.get_function_id();
-    const auto fnit_true=instrumented_functions.function_map.insert({
-      id, program->get_functions().function_map.at(id)});
+    goto_functionst::goto_functiont f;
+    f.copy_from(program->get_functions().function_map.at(id));
+    const auto fnit_true=instrumented_functions.function_map.insert(
+      std::make_pair(id, std::move(f)));
     for(auto &instr : fnit_true.first->second.body.instructions)
       if(instr.type==ASSERT)
         instr.type=ASSUME;

src/taint-slicer/instrumenter.cpp

@@ -113,14 +113,19 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
     for(const auto &fname_fn :
         instrumenter.get_instrumented_functions().function_map)
     {
-      goto_functions.function_map.insert(fname_fn);
+      goto_functionst::goto_functiont f;
+      f.copy_from(fname_fn.second);
+      goto_functions.function_map.insert(
+        std::make_pair(fname_fn.first, std::move(f)));
     }
     for(const auto &fid : props.get_functions())
     {
       if(goto_functions.function_map.count(fid)==0UL)
       {
-        const auto fnit_true=goto_functions.function_map.insert({
-          fid, program->get_functions().function_map.at(fid)});
+        goto_functionst::goto_functiont f;
+        f.copy_from(program->get_functions().function_map.at(fid));
+        const auto fnit_true=goto_functions.function_map.insert(
+          std::make_pair(fid, std::move(f)));
         // We immediatelly substitute all ASSERT statements in the
         // cloned functions into ASSUME statements with the same condition.
         // This is used for to suppress generation of error traces for these
@@ -144,7 +149,8 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
       symbol_table.lookup(fid).value=exprt(ID_nil);
       goto_functionst::goto_functiont empty_fn;
       empty_fn.type=program->get_functions().function_map.at(fid).type;
-      goto_functions.function_map.insert({fid, empty_fn});
+      goto_functions.function_map.insert(
+        std::make_pair(fid, std::move(empty_fn)));
       if(symbol_table.has_symbol(fid+RETURN_VALUE_SUFFIX))
         for(auto &fid_fn : goto_functions.function_map)
           if(fid_fn.second.body_available())