@@ -155,28 +155,12 @@ class ai_baset
155155 }
156156
157157 // / Run abstract interpretation on a whole program
158- void operator ()(
159- const goto_functionst &goto_functions,
160- const namespacet &ns)
161- {
162- initialize (goto_functions);
163- trace_ptrt p = entry_state (goto_functions);
164- fixedpoint (p, goto_functions, ns);
165- finalize ();
166- }
167-
168- // / Run abstract interpretation on a whole program
169- void operator ()(const abstract_goto_modelt &goto_model)
170- {
171- const namespacet ns (goto_model.get_symbol_table ());
172- initialize (goto_model.get_goto_functions ());
173- trace_ptrt p = entry_state (goto_model.get_goto_functions ());
174- fixedpoint (p, goto_model.get_goto_functions (), ns);
175- finalize ();
176- }
158+ virtual void
159+ operator ()(const goto_functionst &goto_functions, const namespacet &ns) = 0 ;
160+ virtual void operator ()(const abstract_goto_modelt &goto_model) = 0;
177161
178162 // / Run abstract interpretation on a single function
179- void operator ()(
163+ virtual void operator ()(
180164 const irep_idt &function_id,
181165 const goto_functionst::goto_functiont &goto_function,
182166 const namespacet &ns)
@@ -288,9 +272,7 @@ class ai_baset
288272 std::ostream &out) const ;
289273
290274 // / Output the abstract states for a whole program
291- void output (
292- const goto_modelt &goto_model,
293- std::ostream &out) const
275+ virtual void output (const goto_modelt &goto_model, std::ostream &out) const
294276 {
295277 const namespacet ns (goto_model.symbol_table );
296278 output (ns, goto_model.goto_functions , out);
@@ -537,6 +519,11 @@ class ai_recursive_interproceduralt : public ai_baset
537519 {
538520 }
539521
522+ // Whole program analysis by starting at the entry function and recursing
523+ void operator ()(const goto_functionst &goto_functions, const namespacet &ns)
524+ override ;
525+ void operator ()(const abstract_goto_modelt &goto_model) override ;
526+
540527protected:
541528 // Override the function that handles a single function call edge
542529 bool visit_edge_function_call (
0 commit comments