Merge pull request #1275 from diffblue/goto-model-service-functions

variants of service functions for goto_modelt

Author: Daniel Kroening

src/goto-instrument/cover.cpp

@@ -1572,3 +1572,15 @@ bool instrument_cover_goals(
   goto_functions.update();
   return false;
 }
+
+bool instrument_cover_goals(
+  const cmdlinet &cmdline,
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  return instrument_cover_goals(
+    cmdline,
+    goto_model.symbol_table,
+    goto_model.goto_functions,
+    message_handler);
+}

src/goto-instrument/cover.h

@@ -42,41 +42,46 @@ enum class coverage_criteriont
   PATH, MCDC, ASSERTION, COVER };
 
 bool consider_goals(
-  const goto_programt &goto_program,
-  coverage_goalst &goals);
+  const goto_programt &,
+  coverage_goalst &);
 
 void instrument_cover_goals(
-  const symbol_tablet &symbol_table,
-  goto_functionst &goto_functions,
+  const symbol_tablet &,
+  goto_functionst &,
   coverage_criteriont,
   bool function_only=false);
 
 void instrument_cover_goals(
-  const symbol_tablet &symbol_table,
-  goto_programt &goto_program,
+  const symbol_tablet &,
+  goto_programt &,
   coverage_criteriont,
   bool function_only=false);
 
 void instrument_cover_goals(
-  const symbol_tablet &symbol_table,
-  goto_functionst &goto_functions,
+  const symbol_tablet &,
+  goto_functionst &,
   coverage_criteriont,
-  coverage_goalst &goals,
+  coverage_goalst &,
   bool function_only=false,
   bool ignore_trivial=false);
 
 void instrument_cover_goals(
-  const symbol_tablet &symbol_table,
-  goto_programt &goto_program,
+  const symbol_tablet &,
+  goto_programt &,
   coverage_criteriont,
   coverage_goalst &goals,
   bool function_only=false,
   bool ignore_trivial=false);
 
 bool instrument_cover_goals(
-  const cmdlinet &cmdline,
-  const symbol_tablet &symbol_table,
-  goto_functionst &goto_functions,
-  message_handlert &msgh);
+  const cmdlinet &,
+  const symbol_tablet &,
+  goto_functionst &,
+  message_handlert &);
+
+bool instrument_cover_goals(
+  const cmdlinet &,
+  goto_modelt &,
+  message_handlert &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_COVER_H

src/goto-instrument/full_slicer.cpp

@@ -382,6 +382,13 @@ void full_slicer(
   full_slicert()(goto_functions, ns, a);
 }
 
+void full_slicer(goto_modelt &goto_model)
+{
+  assert_criteriont a;
+  const namespacet ns(goto_model.symbol_table);
+  full_slicert()(goto_model.goto_functions, ns, a);
+}
+
 void property_slicer(
   goto_functionst &goto_functions,
   const namespacet &ns,
@@ -391,6 +398,14 @@ void property_slicer(
   full_slicert()(goto_functions, ns, p);
 }
 
+void property_slicer(
+  goto_modelt &goto_model,
+  const std::list<std::string> &properties)
+{
+  const namespacet ns(goto_model.symbol_table);
+  property_slicer(goto_model.goto_functions, ns, properties);
+}
+
 slicing_criteriont::~slicing_criteriont()
 {
 }

src/goto-instrument/full_slicer.h

@@ -12,15 +12,21 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H
 #define CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_model.h>
 
 void full_slicer(
-  goto_functionst &goto_functions,
-  const namespacet &ns);
+  goto_functionst &,
+  const namespacet &);
+
+void full_slicer(goto_modelt &);
 
 void property_slicer(
-  goto_functionst &goto_functions,
-  const namespacet &ns,
+  goto_functionst &,
+  const namespacet &,
+  const std::list<std::string> &properties);
+
+void property_slicer(
+  goto_modelt &,
   const std::list<std::string> &properties);
 
 class slicing_criteriont

src/goto-instrument/nondet_static.cpp

@@ -19,6 +19,7 @@ Date: November 2011
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 
+#include <goto-programs/goto_model.h>
 #include <goto-programs/goto_functions.h>
 
 void nondet_static(
@@ -70,7 +71,6 @@ void nondet_static(
   }
 }
 
-
 void nondet_static(
   const namespacet &ns,
   goto_functionst &goto_functions)
@@ -80,3 +80,9 @@ void nondet_static(
   // update counters etc.
   goto_functions.update();
 }
+
+void nondet_static(goto_modelt &goto_model)
+{
+  const namespacet ns(goto_model.symbol_table);
+  nondet_static(ns, goto_model.goto_functions);
+}

src/goto-instrument/nondet_static.h

@@ -17,9 +17,12 @@ Date: November 2011
 
 class goto_functionst;
 class namespacet;
+class goto_modelt;
 
 void nondet_static(
-  const namespacet &ns,
-  goto_functionst &goto_functions);
+  const namespacet &,
+  goto_functionst &);
+
+void nondet_static(goto_modelt &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H

src/goto-programs/convert_nondet.cpp

@@ -9,15 +9,16 @@ Author: Reuben Thomas, [email protected]
 /// \file
 /// Convert side_effect_expr_nondett expressions
 
-#include "goto-programs/convert_nondet.h"
-#include "goto-programs/goto_convert.h"
-#include "goto-programs/goto_model.h"
-#include "goto-programs/remove_skip.h"
+#include "convert_nondet.h"
+#include "goto_convert.h"
+#include "goto_model.h"
+#include "remove_skip.h"
 
-#include <memory>
-#include "java_bytecode/java_object_factory.h" // gen_nondet_init
+#include <java_bytecode/java_object_factory.h> // gen_nondet_init
+
+#include <util/irep_ids.h>
 
-#include "util/irep_ids.h"
+#include <memory>
 
 /// Checks an instruction to see whether it contains an assignment from
 /// side_effect_expr_nondet.  If so, replaces the instruction with a range of
@@ -111,7 +112,7 @@ static goto_programt::targett insert_nondet_init_code(
 /// \param symbol_table: The global symbol table.
 /// \param message_handler: Handles logging.
 /// \param max_nondet_array_length: Maximum size of new nondet arrays.
-static void convert_nondet(
+void convert_nondet(
   goto_programt &goto_program,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
@@ -132,8 +133,6 @@ static void convert_nondet(
   }
 }
 
-
-
 void convert_nondet(
   goto_functionst &goto_functions,
   symbol_tablet &symbol_table,
@@ -155,3 +154,17 @@ void convert_nondet(
 
   remove_skip(goto_functions);
 }
+
+void convert_nondet(
+  goto_modelt &goto_model,
+  message_handlert &message_handler,
+  size_t max_nondet_array_length,
+  size_t max_nondet_tree_depth)
+{
+  convert_nondet(
+    goto_model.goto_functions,
+    goto_model.symbol_table,
+    message_handler,
+    max_nondet_array_length,
+    max_nondet_tree_depth);
+}

src/goto-programs/convert_nondet.h

@@ -16,6 +16,7 @@ Author: Reuben Thomas, [email protected]
 
 class goto_functionst;
 class symbol_tablet;
+class goto_modelt;
 class message_handlert;
 
 /// Replace calls to nondet library functions with an internal nondet
@@ -27,10 +28,16 @@ class message_handlert;
 /// \param max_nondet_tree_depth: Maximum depth for object hierarchy on input
 ///   parameterers.
 void convert_nondet(
-  goto_functionst &goto_functions,
-  symbol_tablet &symbol_table,
-  message_handlert &message_handler,
-  size_t max_nondet_array_length,
-  size_t max_nondet_tree_depth);
+  goto_functionst &,
+  symbol_tablet &,
+  message_handlert &,
+  std::size_t max_nondet_array_length,
+  std::size_t max_nondet_tree_depth);
+
+void convert_nondet(
+  goto_modelt &,
+  message_handlert &,
+  std::size_t max_nondet_array_length,
+  std::size_t max_nondet_tree_depth);
 
 #endif

src/goto-programs/remove_skip.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 /// Program Transformation
 
 #include "remove_skip.h"
+#include "goto_model.h"
 
 static bool is_skip(goto_programt::instructionst::iterator it)
 {
@@ -160,3 +161,9 @@ void remove_skip(goto_functionst &goto_functions)
   Forall_goto_functions(f_it, goto_functions)
     remove_skip(f_it->second.body);
 }
+
+void remove_skip(goto_modelt &goto_model)
+{
+  remove_skip(goto_model.goto_functions);
+}
+

src/goto-programs/remove_skip.h

@@ -14,7 +14,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_functions.h"
 
-void remove_skip(goto_programt &goto_program);
-void remove_skip(goto_functionst &goto_functions);
+class goto_modelt;
+
+void remove_skip(goto_programt &);
+void remove_skip(goto_functionst &);
+void remove_skip(goto_modelt &);
 
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H

src/goto-programs/remove_unused_functions.cpp

@@ -13,6 +13,13 @@ Author: CM Wintersteiger
 
 #include <util/message.h>
 
+void remove_unused_functions(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  remove_unused_functions(goto_model.goto_functions, message_handler);
+}
+
 void remove_unused_functions(
   goto_functionst &functions,
   message_handlert &message_handler)

src/goto-programs/remove_unused_functions.h

@@ -14,11 +14,15 @@ Author: CM Wintersteiger
 
 #include <util/message.h>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_model.h>
 
 void remove_unused_functions(
-  goto_functionst &functions,
-  message_handlert &message_handler);
+  goto_functionst &,
+  message_handlert &);
+
+void remove_unused_functions(
+  goto_modelt &,
+  message_handlert &);
 
 void find_used_functions(
   const irep_idt &current,

src/goto-programs/replace_java_nondet.cpp

@@ -235,8 +235,6 @@ static void replace_java_nondet(goto_programt &goto_program)
   }
 }
 
-
-
 void replace_java_nondet(goto_functionst &goto_functions)
 {
   for(auto &goto_program : goto_functions.function_map)
@@ -248,3 +246,9 @@ void replace_java_nondet(goto_functionst &goto_functions)
 
   remove_skip(goto_functions);
 }
+
+void replace_java_nondet(goto_modelt &goto_model)
+{
+  replace_java_nondet(goto_model.goto_functions);
+}
+

src/goto-programs/replace_java_nondet.h

@@ -12,11 +12,14 @@ Author: Reuben Thomas, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H
 #define CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H
 
+class goto_modelt;
 class goto_functionst;
 
 /// Replace calls to nondet library functions with an internal nondet
 /// representation.
-/// \param goto_functions: The set of goto programs to modify.
-void replace_java_nondet(goto_functionst &goto_functions);
+/// \param goto_model: The goto program to modify.
+void replace_java_nondet(goto_modelt &);
+
+void replace_java_nondet(goto_functionst &);
 
 #endif

src/goto-programs/string_abstraction.cpp

@@ -82,6 +82,16 @@ void string_abstraction(
   string_abstraction(dest);
 }
 
+void string_abstraction(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  string_abstraction(
+    goto_model.symbol_table,
+    message_handler,
+    goto_model.goto_functions);
+}
+
 string_abstractiont::string_abstractiont(
   symbol_tablet &_symbol_table,
   message_handlert &_message_handler):