Don't stop when recursion found

Since we are finding a fixed point we do the same things we do for loops
when we find a recurssive function - we descend into it and carry on.

Previously we were never doing the transforms from the recurssive
function call to the start of the function meaning we would not realise
it can be called with multiple parameters. Further, we weren't doing the
transform from after the recursive function call onwards, meaning for
some inputs it would incorrectly conclude the function never returned.

Now we just do the transforms ignoring the fact it could be recursive.
For the constants domain this is OK as a fixed point will be found
quickly. For other domains we will need to implement some sort of
widening.

Included a test for recursion.

Author: thk123

regression/goto-analyzer/sensitivity-function-call-recursive/main.c

@@ -0,0 +1,56 @@
+#include <assert.h>
+
+int bar(int other)
+{
+  if(other > 0)
+  {
+    int value = bar(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int bar_clean(int other)
+{
+  if(other > 0)
+  {
+    int value = bar_clean(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int fun(int changing, int constant)
+{
+  if(changing > 0)
+  {
+    int value = fun(changing - 1, constant);
+    return value;
+  }
+  else
+  {
+    return constant;
+  }
+}
+
+int main(int argc, char *argv[])
+{
+  int x=3;
+  int y=bar(x+1);
+  assert(y==4); // Unknown in the constants domain
+
+  int y2 = bar(0);
+  assert(y2==0); // Unknown since we are not sensitive to call domain
+
+  int z = bar_clean(0);
+  assert(z==0); // Unknown as the function has parameter as top
+
+  int w = fun(5, 18);
+  assert(w==18);
+}

regression/goto-analyzer/sensitivity-function-call-recursive/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--variable --pointers --arrays --structs --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion y==4: Unknown$
+^\[main\.assertion\.2\] .* assertion y2==0: Unknown$
+^\[main\.assertion\.3\] .* assertion z==0: Success$
+^\[main\.assertion\.4\] .* assertion w==18: Success$
+--
+^warning: ignoring

src/analyses/ai.cpp

@@ -459,14 +459,6 @@ bool ai_baset::do_function_call_rec(
   {
     const irep_idt &identifier=function.get(ID_identifier);
 
-    if(recursion_set.find(identifier)!=recursion_set.end())
-    {
-      // recursion detected!
-      return new_data;
-    }
-    else
-      recursion_set.insert(identifier);
-
     goto_functionst::function_mapt::const_iterator it=
       goto_functions.function_map.find(identifier);
 
@@ -479,8 +471,6 @@ bool ai_baset::do_function_call_rec(
       it,
       arguments,
       ns);
-
-    recursion_set.erase(identifier);
   }
   else if(function.id()==ID_if)
   {

src/analyses/ai.h

@@ -311,9 +311,6 @@ class ai_baset
     const goto_functionst &goto_functions,
     const namespacet &ns);
 
-  typedef std::set<irep_idt> recursion_sett;
-  recursion_sett recursion_set;
-
   // function calls
   bool do_function_call_rec(
     locationt l_call, locationt l_return,