Abstract interpreter: add finalize hook

At least dependence_grapht has good reason to do work at the end of the day--
namely to create an alternative data representation that is trickier to keep
up to date incrementally than to produce in one go at the end. It seems likely
other AIs will have use for a post-fixedpoint hook.

Author: smowton

src/analyses/ai.cpp

@@ -280,6 +280,11 @@ void ai_baset::initialize(const goto_functionst &goto_functions)
     initialize(it->second);
 }
 
+void ai_baset::finalize()
+{
+  // Nothing to do per default
+}
+
 ai_baset::locationt ai_baset::get_next(
   working_sett &working_set)
 {

src/analyses/ai.h

@@ -133,6 +133,7 @@ class ai_baset
     initialize(goto_program);
     entry_state(goto_program);
     fixedpoint(goto_program, goto_functions, ns);
+    finalize();
   }
 
   void operator()(
@@ -142,6 +143,7 @@ class ai_baset
     initialize(goto_functions);
     entry_state(goto_functions);
     fixedpoint(goto_functions, ns);
+    finalize();
   }
 
   void operator()(const goto_modelt &goto_model)
@@ -150,6 +152,7 @@ class ai_baset
     initialize(goto_model.goto_functions);
     entry_state(goto_model.goto_functions);
     fixedpoint(goto_model.goto_functions, ns);
+    finalize();
   }
 
   void operator()(
@@ -160,6 +163,7 @@ class ai_baset
     initialize(goto_function);
     entry_state(goto_function.body);
     fixedpoint(goto_function.body, goto_functions, ns);
+    finalize();
   }
 
   /// Returns the abstract state before the given instruction
@@ -264,6 +268,9 @@ class ai_baset
   virtual void initialize(const goto_functionst::goto_functiont &);
   virtual void initialize(const goto_functionst &);
 
+  // override to add a cleanup step after fixedpoint has run
+  virtual void finalize();
+
   void entry_state(const goto_programt &);
   void entry_state(const goto_functionst &);