Create a new kind of abstract interpreter that does function-local analysis

Author: martin

src/analyses/ai.cpp

@@ -531,6 +531,27 @@ bool ai_baset::visit_end_function(
   return false;
 }
 
+void ai_localt::
+operator()(const goto_functionst &goto_functions, const namespacet &ns)
+{
+  initialize(goto_functions);
+  for(const auto &gf_entry : goto_functions.function_map)
+  {
+    if(gf_entry.second.body_available())
+    {
+      trace_ptrt p = entry_state(gf_entry.second.body);
+      fixedpoint(p, gf_entry.first, gf_entry.second.body, goto_functions, ns);
+    }
+  }
+  finalize();
+}
+
+void ai_localt::operator()(const abstract_goto_modelt &goto_model)
+{
+  const namespacet ns(goto_model.get_symbol_table());
+  operator()(goto_model.get_goto_functions(), ns);
+}
+
 void ai_recursive_interproceduralt::
 operator()(const goto_functionst &goto_functions, const namespacet &ns)
 {

src/analyses/ai.h

@@ -505,6 +505,27 @@ class ai_baset
   message_handlert &message_handler;
 };
 
+// Perform function local analysis on all functions in a program.
+// No interprocedural analysis other than what a domain does when
+// visit()'ing an edge that skips a function call.
+class ai_localt : public ai_baset
+{
+public:
+  ai_localt(
+    std::unique_ptr<ai_history_factory_baset> &&hf,
+    std::unique_ptr<ai_domain_factory_baset> &&df,
+    std::unique_ptr<ai_storage_baset> &&st,
+    message_handlert &mh)
+    : ai_baset(std::move(hf), std::move(df), std::move(st), mh)
+  {
+  }
+
+  // Handle every function independently
+  void operator()(const goto_functionst &goto_functions, const namespacet &ns)
+    override;
+  void operator()(const abstract_goto_modelt &goto_model) override;
+};
+
 // Perform interprocedural analysis by simply recursing in the interpreter
 // This can lead to a call stack overflow if the domain has a large height
 class ai_recursive_interproceduralt : public ai_baset