Permit static analysis to recurse

A subclass can now override get_allow_recursion in order to allow
recursive calls to be handled as usual, rather than assuming they
have no effects as was previously the case.

Author: smowton

src/analyses/static_analysis.cpp

@@ -518,19 +518,21 @@ void static_analysis_baset::do_function_call_rec(
     }
     return;
   }
-  
+
   if(function.id()==ID_symbol)
   {
     const irep_idt &identifier=function.get(ID_identifier);
 
-    if(recursion_set.find(identifier)!=recursion_set.end())
+    if(ignore_recursion)
     {
-      // recursion detected!
-      return;
+      if(recursion_set.find(identifier)!=recursion_set.end())
+      {
+        // recursion detected!
+        return;
+      }
+      else
+        recursion_set.insert(identifier);
     }
-    else
-      recursion_set.insert(identifier);
-
     goto_functionst::function_mapt::const_iterator it=
       goto_functions.function_map.find(identifier);
 
@@ -544,7 +546,8 @@ void static_analysis_baset::do_function_call_rec(
       arguments,
       new_state);
 
-    recursion_set.erase(identifier);
+    if(ignore_recursion)
+      recursion_set.erase(identifier);
   }
   else if(function.id()==ID_if)
   {

src/analyses/static_analysis.h

@@ -98,6 +98,7 @@ class static_analysis_baset
     ns(_ns),
     initialized(false)
   {
+    ignore_recursion=get_ignore_recursion();
   }
 
   virtual void initialize(
@@ -260,6 +261,10 @@ class static_analysis_baset
     locationt l,
     const exprt &expr,
     std::list<exprt> &dest)=0;
+
+  bool ignore_recursion;
+  virtual bool get_ignore_recursion() { return true; }
+  
 };
 
 // T is expected to be derived from domain_baset