diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index bb62a16a6592..a03ba3270c8c 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -537,6 +537,25 @@ bool ai_baset::visit_end_function( return false; } +void ai_recursive_interproceduralt:: +operator()(const goto_functionst &goto_functions, const namespacet &ns) +{ + initialize(goto_functions); + trace_ptrt p = entry_state(goto_functions); + fixedpoint(p, goto_functions, ns); + finalize(); +} + +void ai_recursive_interproceduralt:: +operator()(const abstract_goto_modelt &goto_model) +{ + const namespacet ns(goto_model.get_symbol_table()); + initialize(goto_model.get_goto_functions()); + trace_ptrt p = entry_state(goto_model.get_goto_functions()); + fixedpoint(p, goto_model.get_goto_functions(), ns); + finalize(); +} + bool ai_recursive_interproceduralt::visit_edge_function_call( const irep_idt &calling_function_id, trace_ptrt p_call, diff --git a/src/analyses/ai.h b/src/analyses/ai.h index cf58737d13ae..cec1e110cca3 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -155,28 +155,12 @@ class ai_baset } /// Run abstract interpretation on a whole program - void operator()( - const goto_functionst &goto_functions, - const namespacet &ns) - { - initialize(goto_functions); - trace_ptrt p = entry_state(goto_functions); - fixedpoint(p, goto_functions, ns); - finalize(); - } - - /// Run abstract interpretation on a whole program - void operator()(const abstract_goto_modelt &goto_model) - { - const namespacet ns(goto_model.get_symbol_table()); - initialize(goto_model.get_goto_functions()); - trace_ptrt p = entry_state(goto_model.get_goto_functions()); - fixedpoint(p, goto_model.get_goto_functions(), ns); - finalize(); - } + virtual void + operator()(const goto_functionst &goto_functions, const namespacet &ns) = 0; + virtual void operator()(const abstract_goto_modelt &goto_model) = 0; /// Run abstract interpretation on a single function - void operator()( + virtual void operator()( const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) @@ -288,9 +272,7 @@ class ai_baset std::ostream &out) const; /// Output the abstract states for a whole program - void output( - const goto_modelt &goto_model, - std::ostream &out) const + virtual void output(const goto_modelt &goto_model, std::ostream &out) const { const namespacet ns(goto_model.symbol_table); output(ns, goto_model.goto_functions, out); @@ -537,6 +519,11 @@ class ai_recursive_interproceduralt : public ai_baset { } + // Whole program analysis by starting at the entry function and recursing + void operator()(const goto_functionst &goto_functions, const namespacet &ns) + override; + void operator()(const abstract_goto_modelt &goto_model) override; + protected: // Override the function that handles a single function call edge bool visit_edge_function_call( diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index b054db09c352..a530be8c9b31 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -212,7 +212,7 @@ class constant_propagator_ait:public ait should_track_valuet should_track_value = track_all_values) : dirty(goto_function), should_track_value(should_track_value) { - operator()(function_identifier, goto_function, ns); + ai_baset::operator()(function_identifier, goto_function, ns); replace(goto_function, ns); }