Re-enable old function signatures for test-gen compat

smowton · Sep 14, 2017 · 1264b4d · 1264b4d
1 parent 63c9a1e
commit 1264b4d
Show file tree

Hide file tree

Showing 7 changed files with 50 additions and 4 deletions.
diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp
@@ -18,9 +18,14 @@ call_grapht::call_grapht()
 {
 }
 
-call_grapht::call_grapht(const goto_modelt &goto_model)
+call_grapht::call_grapht(const goto_modelt &goto_model):
+  call_grapht(goto_model.goto_functions)
 {
-  forall_goto_functions(f_it, goto_model.goto_functions)
+}
+
+call_grapht::call_grapht(const goto_functionst &goto_functions)
+{
+  forall_goto_functions(f_it, goto_functions)
   {
     const goto_programt &body=f_it->second.body;
     add(f_it->first, body);

diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h
@@ -22,6 +22,7 @@ class call_grapht
 public:
   call_grapht();
   explicit call_grapht(const goto_modelt &);
+  explicit call_grapht(const goto_functionst &);
 
   void output_dot(std::ostream &out) const;
   void output(std::ostream &out) const;

diff --git a/src/goto-instrument/nondet_static.h b/src/goto-instrument/nondet_static.h
@@ -16,6 +16,12 @@ Date: November 2011
 #define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
 
 class goto_modelt;
+class namespacet;
+class goto_functionst;
+
+void nondet_static(
+  const namespacet &ns,
+  goto_functionst &goto_functions);
 
 void nondet_static(goto_modelt &);
 

diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp
@@ -109,6 +109,19 @@ void remove_static_init_loops(
   optionst &options,
   message_handlert &msg)
 {
-  remove_static_init_loopst remove_loops(goto_model.symbol_table);
-  remove_loops.unwind_enum_static(goto_model.goto_functions, options, msg);
+  remove_static_init_loops(
+    goto_model.symbol_table,
+    goto_model.goto_functions,
+    options,
+    msg);
+}
+
+void remove_static_init_loops(
+  const symbol_tablet &symbol_table,
+  const goto_functionst &goto_functions,
+  optionst &options,
+  message_handlert &msg)
+{
+  remove_static_init_loopst remove_loops(symbol_table);
+  remove_loops.unwind_enum_static(goto_functions, options, msg);
 }
diff --git a/src/goto-programs/remove_static_init_loops.h b/src/goto-programs/remove_static_init_loops.h
@@ -19,10 +19,18 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 
 class goto_modelt;
+class symbol_tablet;
+class goto_functionst;
 
 void remove_static_init_loops(
   const goto_modelt &,
   optionst &,
   message_handlert &);
 
+void remove_static_init_loops(
+  const symbol_tablet &symbol_table,
+  const goto_functionst &goto_functions,
+  optionst &,
+  message_handlert &);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H
diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h
@@ -16,13 +16,19 @@ Author: Peter Schrammel
 
 class namespacet;
 class goto_modelt;
+class goto_functionst;
 
 #define OPT_SHOW_GOTO_FUNCTIONS \
   "(show-goto-functions)"
 
 #define HELP_SHOW_GOTO_FUNCTIONS \
   " --show-goto-functions        show goto program\n"
 
+void show_goto_functions(
+  const namespacet &ns,
+  ui_message_handlert::uit ui,
+  const goto_functionst &goto_functions);
+
 void show_goto_functions(
   const goto_modelt &,
   ui_message_handlert::uit ui);

diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h
@@ -16,9 +16,16 @@ Author: Daniel Kroening, [email protected]
 
 class namespacet;
 class goto_modelt;
+class symbol_tablet;
+class goto_functionst;
 
 void show_properties(
   const goto_modelt &,
   ui_message_handlert::uit ui);
 
+void show_properties(
+  const namespacet &ns,
+  ui_message_handlert::uit ui,
+  const goto_functionst &goto_functions);
+
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H