diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index dd2d5b275fd..93850f64d1d 100644 --- 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 index ea4539147fd..684f74c3a3a 100644 --- 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 index cddbb52c636..ac99134c5bf 100644 --- 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 index 92554c50e4d..c0f3c05150f 100644 --- 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 index 5c31ac527d7..a78001046aa 100644 --- 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, kroening@kroening.com #include 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 index 8cfcbff3ad9..d13c83557bc 100644 --- a/src/goto-programs/show_goto_functions.h +++ b/src/goto-programs/show_goto_functions.h @@ -16,6 +16,7 @@ Author: Peter Schrammel class namespacet; class goto_modelt; +class goto_functionst; #define OPT_SHOW_GOTO_FUNCTIONS \ "(show-goto-functions)" @@ -23,6 +24,11 @@ class goto_modelt; #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 index 98ccc8a948c..0cb0d1c641f 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -16,9 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com 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