From 88d867354ff5840a603e25493bd508a2317ff4db Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Thu, 12 Oct 2017 21:05:53 +0100
Subject: [PATCH 1/7] Rename the XML output to something a bit more meaningful.

---
 src/analyses/ai.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 9591d0b2725..8559a943aec 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -37,7 +37,7 @@ xmlt ai_domain_baset::output_xml(
 {
   std::ostringstream out;
   output(out, ai, ns);
-  xmlt xml("domain");
+  xmlt xml("abstract_state");
   xml.data=out.str();
   return xml;
 }
@@ -170,7 +170,7 @@ jsont ai_baset::output_json(
       json_numbert(std::to_string(i_it->location_number));
     location["sourceLocation"]=
       json_stringt(i_it->source_location.as_string());
-    location["domain"]=find_state(i_it).output_json(*this, ns);
+    location["abstractState"]=find_state(i_it).output_json(*this, ns);
 
     // Ideally we need output_instruction_json
     std::ostringstream out;

From f9ca353149593cad25f1f63a8f3e7685c123e9d9 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Tue, 23 May 2017 20:46:55 +0100
Subject: [PATCH 2/7] Add is_bottom() and is_top() to ai_domain_baset and
 derived domains.

---
 src/analyses/ai.h                        |  4 +++
 src/analyses/constant_propagator.h       | 38 ++++++++++++++++++------
 src/analyses/custom_bitvector_analysis.h | 26 ++++++++++++----
 src/analyses/dependence_graph.h          | 38 ++++++++++++++++++++----
 src/analyses/escape_analysis.h           | 26 ++++++++++++----
 src/analyses/global_may_alias.h          | 24 +++++++++++----
 src/analyses/interval_domain.h           | 31 ++++++++++++-------
 src/analyses/invariant_set_domain.h      | 20 +++++++++----
 src/analyses/is_threaded.cpp             | 21 ++++++++++---
 src/analyses/reaching_definitions.h      | 28 ++++++++++++-----
 src/analyses/uninitialized_domain.h      | 22 +++++++++++---
 11 files changed, 218 insertions(+), 60 deletions(-)

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index a04c60547d0..4584df2dfe8 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -80,6 +80,10 @@ class ai_domain_baset
   // a reasonable entry-point state
   virtual void make_entry()=0;
 
+  virtual bool is_bottom() const=0;
+
+  virtual bool is_top() const=0;
+
   // also add
   //
   //   bool merge(const T &b, locationt from, locationt to);
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 695aea8782f..0fc4796e8b7 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -25,7 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai_base,
-    const namespacet &ns) override;
+    const namespacet &ns) final override;
 
   virtual void output(
     std::ostream &out,
@@ -39,23 +39,33 @@ class constant_propagator_domaint:public ai_domain_baset
 
   virtual bool ai_simplify(
     exprt &condition,
-    const namespacet &ns) const override;
+    const namespacet &ns) const final override;
 
-  virtual void make_bottom() override
+  virtual void make_bottom() final override
   {
     values.set_to_bottom();
   }
 
-  virtual void make_top() override
+  virtual void make_top() final override
   {
     values.set_to_top();
   }
 
-  virtual void make_entry() override
+  virtual void make_entry() final override
   {
     make_top();
   }
 
+  virtual bool is_bottom() const final override
+  {
+    return values.is_bot();
+  }
+
+  virtual bool is_top() const final override
+  {
+    return values.is_top();
+  }
+
   struct valuest
   {
   public:
@@ -70,27 +80,37 @@ class constant_propagator_domaint:public ai_domain_baset
 
     // set whole state
 
-    inline void set_to_bottom()
+    void set_to_bottom()
     {
       replace_const.clear();
       is_bottom=true;
     }
 
-    inline void set_to_top()
+    void set_to_top()
     {
       replace_const.clear();
       is_bottom=false;
     }
 
+    bool is_bot() const
+    {
+      return is_bottom && replace_const.empty();
+    }
+
+    bool is_top() const
+    {
+      return !is_bottom && replace_const.empty();
+    }
+
     // set single identifier
 
-    inline void set_to(const irep_idt &lhs, const exprt &rhs)
+    void set_to(const irep_idt &lhs, const exprt &rhs)
     {
       replace_const.expr_map[lhs]=rhs;
       is_bottom=false;
     }
 
-    inline void set_to(const symbol_exprt &lhs, const exprt &rhs)
+    void set_to(const symbol_exprt &lhs, const exprt &rhs)
     {
       set_to(lhs.get_identifier(), rhs);
     }
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index f0c298f84d6..55d5d444af8 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -27,32 +27,48 @@ class custom_bitvector_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     may_bits.clear();
     must_bits.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     may_bits.clear();
     must_bits.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const final override
+  {
+    DATA_INVARIANT(!has_values.is_false() ||
+                   (may_bits.empty() && must_bits.empty()),
+                   "If the domain is bottom, it must have no bits set");
+    return has_values.is_false();
+  }
+
+  bool is_top() const final override
+  {
+    DATA_INVARIANT(!has_values.is_true() ||
+                   (may_bits.empty() && must_bits.empty()),
+                   "If the domain is top, it must have no bits set");
+    return has_values.is_true();
+  }
+
   bool merge(
     const custom_bitvector_domaint &b,
     locationt from,
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index 4cd7be4c589..2508174b443 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -83,12 +83,12 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett from,
     goto_programt::const_targett to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   jsont output_json(
     const ai_baset &ai,
@@ -96,27 +96,53 @@ class dep_graph_domaint:public ai_domain_baset
 
   void make_top() final override
   {
-    assert(node_id!=std::numeric_limits<node_indext>::max());
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must not be valid");
 
     has_values=tvt(true);
     control_deps.clear();
     data_deps.clear();
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
-    assert(node_id!=std::numeric_limits<node_indext>::max());
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
 
     has_values=tvt(false);
     control_deps.clear();
     data_deps.clear();
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const final override
+  {
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
+
+    DATA_INVARIANT(!has_values.is_true() ||
+                   (control_deps.empty() && data_deps.empty()),
+                   "If the domain is top, it must have no dependencies");
+
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const final override
+  {
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
+
+    DATA_INVARIANT(!has_values.is_false() ||
+                   (control_deps.empty() && data_deps.empty()),
+                   "If the domain is bottom, it must have no dependencies");
+
+    return has_values.is_false();
+  }
+
   void set_node_id(node_indext id)
   {
     node_id=id;
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index 7a4c606e1d4..52de2b5dfc8 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -32,33 +32,49 @@ class escape_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   bool merge(
     const escape_domaint &b,
     locationt from,
     locationt to);
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     cleanup_map.clear();
     aliases.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     cleanup_map.clear();
     aliases.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  bool is_bottom() const override final
+  {
+    DATA_INVARIANT(!has_values.is_false() ||
+                   (cleanup_map.empty() && (aliases.size()==0)),
+                   "If the domain is bottom, all maps must be empty");
+    return has_values.is_false();
+  }
+
+  bool is_top() const override final
+  {
+    DATA_INVARIANT(!has_values.is_true() ||
+                   (cleanup_map.empty() && (aliases.size()==0)),
+                   "If the domain is top, all maps must be empty");
+    return has_values.is_true();
+  }
+
+  void make_entry() override final
   {
     make_top();
   }
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index d946b371c05..a5e1b0cd49a 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -32,35 +32,49 @@ class global_may_alias_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   bool merge(
     const global_may_alias_domaint &b,
     locationt from,
     locationt to);
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     aliases.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     aliases.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const final override
+  {
+    DATA_INVARIANT(!has_values.is_false() || (aliases.size()==0),
+                   "If the domain is bottom, there must be no aliases");
+    return has_values.is_false();
+  }
+
+  bool is_top() const final override
+  {
+    DATA_INVARIANT(!has_values.is_true() || (aliases.size()==0),
+                   "If the domain is top, there must be no aliases");
+    return has_values.is_true();
+  }
+
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;
 
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index d078324679f..7702990d53d 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -36,12 +36,12 @@ class interval_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const override;
 
 protected:
   bool join(const interval_domaint &b);
@@ -56,7 +56,7 @@ class interval_domaint:public ai_domain_baset
   }
 
   // no states
-  void make_bottom() final
+  void make_bottom() final override
   {
     int_map.clear();
     float_map.clear();
@@ -64,18 +64,34 @@ class interval_domaint:public ai_domain_baset
   }
 
   // all states
-  void make_top() final
+  void make_top() final override
   {
     int_map.clear();
     float_map.clear();
     bottom=false;
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const override final
+  {
+    #if 0
+    // This invariant should hold but is not correctly enforced at the moment.
+    DATA_INVARIANT(!bottom || (int_map.empty() && float_map.empty()),
+                   "If the domain is bottom the value maps must be empty");
+    #endif
+
+    return bottom;
+  }
+
+  bool is_top() const override final
+  {
+    return !bottom && int_map.empty() && float_map.empty();
+  }
+
   exprt make_expression(const symbol_exprt &) const;
 
   void assume(const exprt &, const namespacet &);
@@ -90,11 +106,6 @@ class interval_domaint:public ai_domain_baset
     return src.id()==ID_floatbv;
   }
 
-  bool is_bottom() const
-  {
-    return bottom;
-  }
-
   virtual bool ai_simplify(
     exprt &condition,
     const namespacet &ns) const override;
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 4d38b6b2657..367e987c709 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -44,7 +44,7 @@ class invariant_set_domaint:public ai_domain_baset
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final
+    const namespacet &ns) const final override
   {
     if(has_values.is_known())
       out << has_values.to_string() << '\n';
@@ -56,25 +56,35 @@ class invariant_set_domaint:public ai_domain_baset
     locationt from_l,
     locationt to_l,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
-  void make_top() final
+  void make_top() final override
   {
     invariant_set.make_true();
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     invariant_set.make_false();
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     invariant_set.make_true();
     has_values=tvt(true);
   }
+
+  bool is_top() const override final
+  {
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    return has_values.is_false();
+  }
 };
 
 #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 1ac32d2341c..54a3fa2d70d 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -52,7 +52,7 @@ class is_threaded_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final
+    const namespacet &ns) final override
   {
     // assert(reachable);
 
@@ -63,23 +63,36 @@ class is_threaded_domaint:public ai_domain_baset
       is_threaded=true;
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     reachable=false;
     is_threaded=false;
   }
 
-  void make_top() final
+  void make_top() final override
   {
     reachable=true;
     is_threaded=true;
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     reachable=true;
     is_threaded=false;
   }
+
+  bool is_bottom() const override final
+  {
+    DATA_INVARIANT(reachable || !is_threaded,
+                   "A location cannot be threaded if it is not reachable.");
+
+    return !reachable;
+  }
+
+  bool is_top() const override final
+  {
+    return reachable && is_threaded;
+  }
 };
 
 void is_threadedt::compute(const goto_functionst &goto_functions)
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index c62bd5e4b51..e218eb19bca 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -117,17 +117,17 @@ class rd_range_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final
+    const namespacet &ns) const final override
   {
     output(out);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     values.clear();
     if(bv_container)
@@ -135,7 +135,7 @@ class rd_range_domaint:public ai_domain_baset
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     values.clear();
     if(bv_container)
@@ -143,11 +143,25 @@ class rd_range_domaint:public ai_domain_baset
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const override final
+  {
+    DATA_INVARIANT(!has_values.is_true() || values.empty(),
+                   "If domain is top, the value map must be empty");
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    DATA_INVARIANT(!has_values.is_false() || values.empty(),
+                   "If domain is bottom, the value map must be empty");
+    return has_values.is_false();
+  }
+
   // returns true iff there is something new
   bool merge(
     const rd_range_domaint &other,
@@ -246,9 +260,9 @@ class reaching_definitions_analysist:
   virtual ~reaching_definitions_analysist();
 
   virtual void initialize(
-    const goto_functionst &goto_functions);
+    const goto_functionst &goto_functions) override;
 
-  virtual statet &get_state(goto_programt::const_targett l)
+  virtual statet &get_state(goto_programt::const_targett l) override
   {
     statet &s=concurrency_aware_ait<rd_range_domaint>::get_state(l);
 
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index 11dcaa02170..45a9d085c99 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -33,30 +33,44 @@ class uninitialized_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
     const namespacet &ns) const final;
 
-  void make_top() final
+  void make_top() final override
   {
     uninitialized.clear();
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     uninitialized.clear();
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const override final
+  {
+    DATA_INVARIANT(!has_values.is_true() || uninitialized.empty(),
+                   "If domain is top, the uninitialized set must be empty");
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    DATA_INVARIANT(!has_values.is_false() || uninitialized.empty(),
+                   "If domain is bottom, the uninitialized set must be empty");
+    return has_values.is_false();
+  }
+
   // returns true iff there is something new
   bool merge(
     const uninitialized_domaint &other,

From 5b604ae0c886a7ec13348343de8b9e66afbecd35 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 16 Oct 2017 11:58:31 +0100
Subject: [PATCH 3/7] Update the mock domain with the new ai_domain_baset
 interface.

---
 unit/analyses/ai/ai_simplify_lhs.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
index d345468fd99..c8ea9dae2d2 100644
--- a/unit/analyses/ai/ai_simplify_lhs.cpp
+++ b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -33,6 +33,16 @@ class constant_simplification_mockt:public ai_domain_baset
   {}
   void make_entry() override
   {}
+  bool is_bottom() const override
+  {
+    UNREACHABLE;
+    return true;
+  }
+  bool is_top() const override
+  {
+    UNREACHABLE;
+    return true;
+  }
 
   bool ai_simplify(exprt &condition, const namespacet &ns) const override;
 };

From 93f2e1f24347d78fb964595fcf5f37b2a9f4de88 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Thu, 12 Oct 2017 21:06:24 +0100
Subject: [PATCH 4/7] Use is_bottom() to catch unreachable functions.

---
 src/analyses/ai.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 8559a943aec..30fceccbaa3 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -431,7 +431,12 @@ bool ai_baset::do_function_call(
     assert(l_end->is_end_function());
 
     // do edge from end of function to instruction after call
-    std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_end)));
+    const statet &end_state=get_state(l_end);
+
+    if(end_state.is_bottom())
+      return false; // function exit point not reachable
+
+    std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
     tmp_state->transform(l_end, l_return, *this, ns);
 
     // Propagate those

From 3050c53e86d5243406029a175dc19f280d7ba872 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Mon, 27 Mar 2017 15:17:38 +0100
Subject: [PATCH 5/7] 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.
---
 .../main.c                                    | 56 +++++++++++++++++++
 .../test.desc                                 | 11 ++++
 src/analyses/ai.cpp                           | 10 ----
 src/analyses/ai.h                             |  3 -
 4 files changed, 67 insertions(+), 13 deletions(-)
 create mode 100644 regression/goto-analyzer/sensitivity-function-call-recursive/main.c
 create mode 100644 regression/goto-analyzer/sensitivity-function-call-recursive/test.desc

diff --git a/regression/goto-analyzer/sensitivity-function-call-recursive/main.c b/regression/goto-analyzer/sensitivity-function-call-recursive/main.c
new file mode 100644
index 00000000000..b9e6daf3347
--- /dev/null
+++ b/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);
+}
diff --git a/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc b/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc
new file mode 100644
index 00000000000..c3670bb5cc9
--- /dev/null
+++ b/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
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 30fceccbaa3..c70206a41ad 100644
--- a/src/analyses/ai.cpp
+++ b/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)
   {
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index 4584df2dfe8..2e41914e4ea 100644
--- a/src/analyses/ai.h
+++ b/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,

From aae984a7df7b05b86c6ff14eab069012a38d8adc Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 16 Oct 2017 12:38:32 +0100
Subject: [PATCH 6/7] Disable the regression test for now as it depends on the
 variable sensitivity domain.

This change was cherry-picked from much later in the variable-sensitivity patch set.
It makes sense to include it here as the changes are independent and apply to many
domains.  However the test case requires options that have not been added yet and
so is disabled for now.
---
 .../goto-analyzer/sensitivity-function-call-recursive/test.desc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc b/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc
index c3670bb5cc9..88534789621 100644
--- a/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc
+++ b/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --variable --pointers --arrays --structs --verify
 ^EXIT=0$

From eef32dbcddeb45592a9c2d7fc9f1ba5408c59099 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 16 Oct 2017 10:51:25 +0100
Subject: [PATCH 7/7] Methods for ai_baset to allow access to the
 ai_base_domaint for a location.

Previously, to access the domain for at a particular location, you had to
use the operator[] interface in ait<domainT> (or subclass), which meant that
the code had to be written / templated / duplicated for each domainT, even
when the only interface that was being used was the ai_base_domaint one.
This is the case for various tasks in goto-analyzer.  This interface should
also support flow-insensitive or context-dependent AI engines.
---
 src/analyses/ai.h | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index 2e41914e4ea..1cecf984953 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -162,6 +162,17 @@ class ai_baset
     fixedpoint(goto_function.body, goto_functions, ns);
   }
 
+  /// Returns the abstract state before the given instruction
+  virtual const ai_domain_baset & abstract_state_before(
+    goto_programt::const_targett t) const = 0;
+
+  /// Returns the abstract state after the given instruction
+  virtual const ai_domain_baset & abstract_state_after(
+    goto_programt::const_targett t) const
+  {
+    return abstract_state_before(std::next(t));
+  }
+
   virtual void clear()
   {
   }
@@ -370,6 +381,12 @@ class ait:public ai_baset
     return it->second;
   }
 
+  const ai_domain_baset & abstract_state_before(
+    goto_programt::const_targett t) const override
+  {
+    return (*this)[t];
+  }
+
   void clear() override
   {
     state_map.clear();