From 50383edd22465c2903bc86e59cf6a59664fe62f7 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 29 Nov 2016 23:17:05 +0000
Subject: [PATCH 1/2] Require bottom/top to be implemented by ai domains

Domains without bottom would not be able to distinguish states being
uninitialized from ones being empty/the smallest element. Thus even the
very first merge into such a state possibly had no effect, which in turn
would cause functions not being entered. Thus effects, such as
assignments to global variables, would not be seen.

Als use and enforce the implementation of make_entry.
ai_baset::entry_point now uses make_entry; implementations may still use
make_top to implement make_entry.

Fixes #325
---
 regression/goto-instrument/data-flow1/main.c  | 18 +++++++++++++
 .../goto-instrument/data-flow1/test.desc      |  8 ++++++
 src/analyses/ai.cpp                           |  3 +--
 src/analyses/custom_bitvector_analysis.cpp    | 15 +++++++----
 src/analyses/custom_bitvector_analysis.h      | 16 ++++++------
 src/analyses/dependence_graph.cpp             |  9 ++++---
 src/analyses/dependence_graph.h               |  9 +++++--
 src/analyses/escape_analysis.cpp              | 10 +++++---
 src/analyses/escape_analysis.h                | 20 ++++++++-------
 src/analyses/global_may_alias.cpp             | 11 +++++++-
 src/analyses/global_may_alias.h               | 14 ++++++++---
 src/analyses/invariant_set_domain.h           | 23 ++++++++++++++---
 src/analyses/is_threaded.cpp                  |  6 ++---
 src/analyses/reaching_definitions.cpp         | 25 +++++++++++++------
 src/analyses/reaching_definitions.h           | 19 ++++++++++++--
 src/analyses/uninitialized_domain.cpp         | 18 ++++++-------
 src/analyses/uninitialized_domain.h           | 16 ++++++------
 17 files changed, 170 insertions(+), 70 deletions(-)
 create mode 100644 regression/goto-instrument/data-flow1/main.c
 create mode 100644 regression/goto-instrument/data-flow1/test.desc

diff --git a/regression/goto-instrument/data-flow1/main.c b/regression/goto-instrument/data-flow1/main.c
new file mode 100644
index 00000000000..1aecb44916d
--- /dev/null
+++ b/regression/goto-instrument/data-flow1/main.c
@@ -0,0 +1,18 @@
+int d=0;
+
+void f1()
+{
+  d=1;
+}
+
+int main()
+{
+  int x=2;
+  int y=3;
+
+  f1();
+
+  if(x && y && d)
+    return 0;
+}
+
diff --git a/regression/goto-instrument/data-flow1/test.desc b/regression/goto-instrument/data-flow1/test.desc
new file mode 100644
index 00000000000..e7413631c0f
--- /dev/null
+++ b/regression/goto-instrument/data-flow1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+"--show-dependence-graph"
+^EXIT=0$
+^SIGNAL=0$
+Data dependencies: .*33.*
+--
+^warning: ignoring
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index f98a3f807ae..3f72fee17e6 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -120,8 +120,7 @@ Function: ai_baset::entry_state
 
 void ai_baset::entry_state(const goto_programt &goto_program)
 {
-  // The first instruction of 'goto_program' is the entry point,
-  // and we make that 'top'.
+  // The first instruction of 'goto_program' is the entry point
   get_state(goto_program.instructions.begin()).make_entry();
 }
 
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 883ea1ef188..878a7037320 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -326,6 +326,8 @@ void custom_bitvector_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
+  if(has_values.is_false()) return;
+
   // upcast of ai
   custom_bitvector_analysist &cba=
     static_cast<custom_bitvector_analysist &>(ai);
@@ -565,8 +567,11 @@ void custom_bitvector_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
-  if(is_bottom)
-    out << "BOTTOM\n";
+  if(has_values.is_known())
+  {
+    out << has_values.to_string() << '\n';
+    return;
+  }
 
   const custom_bitvector_analysist &cba=
     static_cast<const custom_bitvector_analysist &>(ai);
@@ -625,10 +630,10 @@ bool custom_bitvector_domaint::merge(
   locationt from,
   locationt to)
 {
-  if(b.is_bottom)
+  if(b.has_values.is_false())
     return false; // no change
 
-  if(is_bottom)
+  if(has_values.is_false())
   {
     *this=b;
     return true; // change
@@ -858,7 +863,7 @@ void custom_bitvector_analysist::check(
         if(!custom_bitvector_domaint::has_get_must_or_may(i_it->guard))
           continue;
 
-        if(operator[](i_it).is_bottom) continue;
+        if(operator[](i_it).has_values.is_false()) continue;
 
         exprt tmp=eval(i_it->guard, i_it);
         result=simplify_expr(tmp, ns);
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index d964f34f3ec..3cdf0895ddb 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
 
 #include <util/numbering.h>
+#include <util/threeval.h>
 
 #include "ai.h"
 #include "local_may_alias.h"
@@ -42,20 +43,19 @@ class custom_bitvector_domaint:public ai_domain_baset
   {
     may_bits.clear();
     must_bits.clear();
-    is_bottom=true;
+    has_values=tvt(false);
   }
 
   void make_top() final override
   {
-    // We don't have a proper top, and refuse to do this.
-    assert(false);
+    may_bits.clear();
+    must_bits.clear();
+    has_values=tvt(true);
   }
 
   void make_entry() final override
   {
-    may_bits.clear();
-    must_bits.clear();
-    is_bottom=false;
+    make_top();
   }
 
   bool merge(
@@ -90,9 +90,9 @@ class custom_bitvector_domaint:public ai_domain_baset
   vectorst get_rhs(const exprt &) const;
   vectorst get_rhs(const irep_idt &) const;
 
-  bool is_bottom;
+  tvt has_values;
 
-  custom_bitvector_domaint():is_bottom(true)
+  custom_bitvector_domaint():has_values(true)
   {
   }
 
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index c5ff3153ca5..0114058e0dc 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -32,7 +32,8 @@ bool dep_graph_domaint::merge(
   goto_programt::const_targett from,
   goto_programt::const_targett to)
 {
-  bool change=false;
+  bool changed=has_values.is_false();
+  has_values=tvt::unknown();
 
   depst::iterator it=control_deps.begin();
   for(depst::const_iterator ito=src.control_deps.begin();
@@ -44,7 +45,7 @@ bool dep_graph_domaint::merge(
     if(it==control_deps.end() || *ito<*it)
     {
       control_deps.insert(it, *ito);
-      change=true;
+      changed=true;
     }
     else if(it!=control_deps.end())
       ++it;
@@ -60,13 +61,13 @@ bool dep_graph_domaint::merge(
     if(it==data_deps.end() || *ito<*it)
     {
       data_deps.insert(it, *ito);
-      change=true;
+      changed=true;
     }
     else if(it!=data_deps.end())
       ++it;
   }
 
-  return change;
+  return changed;
 }
 
 /*******************************************************************\
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index e783fae8fda..15c0828fef6 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -13,6 +13,7 @@ Date: August 2013
 #define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
 
 #include <util/graph.h>
+#include <util/threeval.h>
 
 #include "ai.h"
 #include "cfg_dominators.h"
@@ -70,6 +71,7 @@ class dep_graph_domaint:public ai_domain_baset
   typedef graph<dep_nodet>::node_indext node_indext;
 
   dep_graph_domaint():
+    has_values(false),
     node_id(std::numeric_limits<node_indext>::max())
   {
   }
@@ -89,20 +91,22 @@ class dep_graph_domaint:public ai_domain_baset
     std::ostream &out,
     const ai_baset &ai,
     const namespacet &ns) const final override;
-    
+
   void make_top() final override
   {
+    has_values=tvt(true);
     node_id=std::numeric_limits<node_indext>::max();
   }
 
   void make_bottom() final override
   {
+    has_values=tvt(false);
     node_id=std::numeric_limits<node_indext>::max();
   }
 
   void make_entry() final override
   {
-    node_id=std::numeric_limits<node_indext>::max();
+    make_top();
   }
 
   void set_node_id(node_indext id)
@@ -117,6 +121,7 @@ class dep_graph_domaint:public ai_domain_baset
   }
 
 protected:
+  tvt has_values;
   node_indext node_id;
 
   typedef std::set<goto_programt::const_targett> depst;
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index 7d610c3198a..711dd35d170 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -266,6 +266,8 @@ void escape_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
+  if(has_values.is_false()) return;
+
   // upcast of ai
   //escape_analysist &ea=
   //  static_cast<escape_analysist &>(ai);
@@ -364,9 +366,9 @@ void escape_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
-  if(is_bottom)
+  if(has_values.is_known())
   {
-    out << "BOTTOM\n";
+    out << has_values.to_string() << '\n';
     return;
   }
 
@@ -422,10 +424,10 @@ bool escape_domaint::merge(
   locationt from,
   locationt to)
 {
-  if(b.is_bottom)
+  if(b.has_values.is_false())
     return false; // no change
 
-  if(is_bottom)
+  if(has_values.is_false())
   {
     *this=b;
     return true; // change
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index c485a01140e..3cccec91a30 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
 
 #include <util/numbering.h>
+#include <util/threeval.h>
 #include <util/union_find.h>
 
 #include "ai.h"
@@ -28,7 +29,7 @@ class escape_analysist;
 class escape_domaint:public ai_domain_baset
 {
 public:
-  escape_domaint():is_bottom(true)
+  escape_domaint():has_values(false)
   {
   }
 
@@ -51,19 +52,20 @@ class escape_domaint:public ai_domain_baset
   void make_bottom() override final
   {
     cleanup_map.clear();
-    is_bottom=true;
+    aliases.clear();
+    has_values=tvt(false);
   }
 
   void make_top() override final
   {
-    // We don't have a proper top.
-    assert(false);
+    cleanup_map.clear();
+    aliases.clear();
+    has_values=tvt(true);
   }
-  
+
   void make_entry() override final
   {
-    cleanup_map.clear();
-    is_bottom=false;
+    make_top();
   }
 
   typedef union_find<irep_idt> aliasest;
@@ -80,9 +82,9 @@ class escape_domaint:public ai_domain_baset
   typedef std::map<irep_idt, cleanupt > cleanup_mapt;
   cleanup_mapt cleanup_map;
 
-  bool is_bottom;
-
 protected:
+  tvt has_values;
+
   void assign_lhs_cleanup(const exprt &, const std::set<irep_idt> &);
   void get_rhs_cleanup(const exprt &, std::set<irep_idt> &);
   void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
index 0e3e190aa29..f89530d3ed8 100644
--- a/src/analyses/global_may_alias.cpp
+++ b/src/analyses/global_may_alias.cpp
@@ -130,6 +130,8 @@ void global_may_alias_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
+  if(has_values.is_false()) return;
+
   const goto_programt::instructiont &instruction=*from;
 
   switch(instruction.type)
@@ -179,6 +181,12 @@ void global_may_alias_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
+  if(has_values.is_known())
+  {
+    out << has_values.to_string() << '\n';
+    return;
+  }
+
   for(aliasest::const_iterator a_it1=aliases.begin();
       a_it1!=aliases.end();
       a_it1++)
@@ -218,7 +226,8 @@ bool global_may_alias_domaint::merge(
   locationt from,
   locationt to)
 {
-  bool changed=false;
+  bool changed=has_values.is_false();
+  has_values=tvt::unknown();
 
   // do union
   for(aliasest::const_iterator it=b.aliases.begin();
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index 0b4d178baab..69eaa22404b 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
 
 #include <util/numbering.h>
+#include <util/threeval.h>
 #include <util/union_find.h>
 
 #include "ai.h"
@@ -28,6 +29,10 @@ class global_may_alias_analysist;
 class global_may_alias_domaint:public ai_domain_baset
 {
 public:
+  global_may_alias_domaint():has_values(false)
+  {
+  }
+
   void transform(
     locationt from,
     locationt to,
@@ -47,23 +52,26 @@ class global_may_alias_domaint:public ai_domain_baset
   void make_bottom() final override
   {
     aliases.clear();
+    has_values=tvt(false);
   }
 
   void make_top() final override
   {
-    // We don't have a proper top.
-    assert(false);
+    aliases.clear();
+    has_values=tvt(true);
   }
 
   void make_entry() final override
   {
-    aliases.clear();
+    make_top();
   }
 
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;
 
 protected:
+  tvt has_values;
+
   void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
   void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
   void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 2190b0503b4..99923f536f9 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -9,12 +9,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
 #define CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
 
+#include <util/threeval.h>
+
 #include "ai.h"
 #include "invariant_set.h"
 
 class invariant_set_domaint:public ai_domain_baset
 {
 public:
+  invariant_set_domaint():has_values(false)
+  {
+  }
+
+  tvt has_values;
   invariant_sett invariant_set;
 
   // overloading
@@ -24,7 +31,11 @@ class invariant_set_domaint:public ai_domain_baset
     locationt from,
     locationt to)
   {
-    return invariant_set.make_union(other.invariant_set);
+    bool changed=invariant_set.make_union(other.invariant_set) ||
+                 has_values.is_false();
+    has_values=tvt::unknown();
+
+    return changed;
   }
 
   void output(
@@ -32,7 +43,10 @@ class invariant_set_domaint:public ai_domain_baset
     const ai_baset &ai,
     const namespacet &ns) const override final
   {
-    invariant_set.output("", out);
+    if(has_values.is_known())
+      out << has_values.to_string() << '\n';
+    else
+      invariant_set.output("", out);
   }
 
   virtual void transform(
@@ -40,20 +54,23 @@ class invariant_set_domaint:public ai_domain_baset
     locationt to_l,
     ai_baset &ai,
     const namespacet &ns) override final;
-    
+
   void make_top() override final
   {
     invariant_set.make_true();
+    has_values=tvt(true);
   }
 
   void make_bottom() override final
   {
     invariant_set.make_false();
+    has_values=tvt(false);
   }
 
   void make_entry() override final
   {
     invariant_set.make_true();
+    has_values=tvt(true);
   }
 };
 
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 0b3df79a553..1c14ad9d424 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -34,7 +34,7 @@ class is_threaded_domaint:public ai_domain_baset
     bool old_reachable=reachable;
     if(src.reachable)
       reachable=true;
-  
+
     bool old_h_s=has_spawn;
     if(src.has_spawn &&
        (from->is_end_function() ||
@@ -66,7 +66,7 @@ class is_threaded_domaint:public ai_domain_baset
       is_threaded=true;
     }
   }
-  
+
   void make_bottom() override final
   {
     reachable=has_spawn=is_threaded=false;
@@ -76,7 +76,7 @@ class is_threaded_domaint:public ai_domain_baset
   {
     reachable=has_spawn=is_threaded=true;
   }
-  
+
   void make_entry() override final
   {
     reachable=true;
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index c0cda391b9e..04809464c70 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -679,6 +679,13 @@ Function: rd_range_domaint::output
 void rd_range_domaint::output(std::ostream &out) const
 {
   out << "Reaching definitions:" << std::endl;
+
+  if(has_values.is_known())
+  {
+    out << has_values.to_string() << '\n';
+    return;
+  }
+
   for(valuest::const_iterator
       it=values.begin();
       it!=values.end();
@@ -797,7 +804,8 @@ bool rd_range_domaint::merge(
   locationt from,
   locationt to)
 {
-  bool more=false;
+  bool changed=has_values.is_false();
+  has_values=tvt::unknown();
 
   valuest::iterator it=values.begin();
   for(valuest::const_iterator ito=other.values.begin();
@@ -809,7 +817,7 @@ bool rd_range_domaint::merge(
     if(it==values.end() || ito->first<it->first)
     {
       values.insert(*ito);
-      more=true;
+      changed=true;
     }
     else if(it!=values.end())
     {
@@ -817,7 +825,7 @@ bool rd_range_domaint::merge(
 
       if(merge_inner(it->second, ito->second))
       {
-        more=true;
+        changed=true;
         export_cache.erase(it->first);
       }
 
@@ -825,7 +833,7 @@ bool rd_range_domaint::merge(
     }
   }
 
-  return more;
+  return changed;
 }
 
 /*******************************************************************\
@@ -853,7 +861,8 @@ bool rd_range_domaint::merge_shared(
   assert(rd!=0);
 #endif
 
-  bool more=false;
+  bool changed=has_values.is_false();
+  has_values=tvt::unknown();
 
   valuest::iterator it=values.begin();
   for(valuest::const_iterator ito=other.values.begin();
@@ -871,7 +880,7 @@ bool rd_range_domaint::merge_shared(
     if(it==values.end() || ito->first<it->first)
     {
       values.insert(*ito);
-      more=true;
+      changed=true;
     }
     else if(it!=values.end())
     {
@@ -879,7 +888,7 @@ bool rd_range_domaint::merge_shared(
 
       if(merge_inner(it->second, ito->second))
       {
-        more=true;
+        changed=true;
         export_cache.erase(it->first);
       }
 
@@ -887,7 +896,7 @@ bool rd_range_domaint::merge_shared(
     }
   }
 
-  return more;
+  return changed;
 }
 
 /*******************************************************************\
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 0d1d2e36f39..a047e5cd782 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -12,6 +12,8 @@ Date: February 2013
 #ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H
 #define CPROVER_ANALYSES_REACHING_DEFINITIONS_H
 
+#include <util/threeval.h>
+
 #include "ai.h"
 #include "goto_rw.h"
 
@@ -44,6 +46,12 @@ class sparse_bitvector_analysist
     return entry.first->second;
   }
 
+  void clear()
+  {
+    value_map.clear();
+    values.clear();
+  }
+
 protected:
   typedef typename std::map<V, std::size_t> inner_mapt;
   std::vector<typename inner_mapt::const_iterator> values;
@@ -83,6 +91,7 @@ class rd_range_domaint:public ai_domain_baset
 public:
   rd_range_domaint():
     ai_domain_baset(),
+    has_values(false),
     bv_container(0)
   {
   }
@@ -106,20 +115,24 @@ class rd_range_domaint:public ai_domain_baset
   {
     output(out);
   }
-  
+
   void make_top() override final
   {
     values.clear();
+    if(bv_container) bv_container->clear();
+    has_values=tvt(true);
   }
 
   void make_bottom() override final
   {
     values.clear();
+    if(bv_container) bv_container->clear();
+    has_values=tvt(false);
   }
 
   void make_entry() override final
   {
-    values.clear();
+    make_top();
   }
 
   // returns true iff there is s.th. new
@@ -145,6 +158,8 @@ class rd_range_domaint:public ai_domain_baset
   }
 
 protected:
+  tvt has_values;
+
   sparse_bitvector_analysist<reaching_definitiont> *bv_container;
 
   typedef std::set<std::size_t> values_innert;
diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp
index e0aa7b0c057..36640250fa8 100644
--- a/src/analyses/uninitialized_domain.cpp
+++ b/src/analyses/uninitialized_domain.cpp
@@ -31,7 +31,7 @@ void uninitialized_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
-  if(is_bottom) return;
+  if(has_values.is_false()) return;
 
   switch(from->type)
   {
@@ -98,8 +98,8 @@ void uninitialized_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
-  if(is_bottom)
-    out << "BOTTOM";
+  if(has_values.is_known())
+    out << has_values.to_string() << '\n';
   else
   {
     for(const auto & id : uninitialized)
@@ -124,16 +124,16 @@ bool uninitialized_domaint::merge(
   locationt from,
   locationt to)
 {
-  bool old_is_bottom=is_bottom;
-  
-  is_bottom=is_bottom && other.is_bottom;
-  
   unsigned old_uninitialized=uninitialized.size();
 
   uninitialized.insert(
     other.uninitialized.begin(),
     other.uninitialized.end());
 
-  return old_is_bottom!=is_bottom ||
-         old_uninitialized!=uninitialized.size();
+  bool changed=
+    (has_values.is_false() && !other.has_values.is_false()) ||
+    old_uninitialized!=uninitialized.size();
+  has_values=tvt::unknown();
+
+  return changed;
 }
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index 89943ef8054..93f1f2fd2b8 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -11,16 +11,16 @@ Date: January 2010
 #ifndef CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
 #define CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
 
+#include <util/threeval.h>
+
 #include "ai.h"
 
 class uninitialized_domaint:public ai_domain_baset
 {
 public:
-  uninitialized_domaint():is_bottom(true)
+  uninitialized_domaint():has_values(false)
   {
   }
-  
-  bool is_bottom;
 
   // Locals that are declared but may not be initialized
   typedef std::set<irep_idt> uninitializedt;
@@ -36,17 +36,17 @@ class uninitialized_domaint:public ai_domain_baset
     std::ostream &out,
     const ai_baset &ai,
     const namespacet &ns) const override final;
-    
+
   void make_top() override final
   {
-    // We don't have a proper 'top', and refuse to do this.
-    assert(false);
+    uninitialized.clear();
+    has_values=tvt(true);
   }
 
   void make_bottom() override final
   {
     uninitialized.clear();
-    is_bottom=true;
+    has_values=tvt(false);
   }
 
   void make_entry() override final
@@ -61,6 +61,8 @@ class uninitialized_domaint:public ai_domain_baset
     locationt to);
 
 protected:
+  tvt has_values;
+
   void assign(const exprt &lhs);
 };
 

From bda847fdd4aa405ed1c95523321cff33e686d521 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 30 Nov 2016 22:44:12 +0000
Subject: [PATCH 2/2] Initialize working set to first instruction only

All other instructions, if reachable, will be seen via visit.
Unreachable instructions should have their states remain bottom.
---
 src/analyses/ai.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 3f72fee17e6..0e95e233e44 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -225,9 +225,11 @@ bool ai_baset::fixedpoint(
 {
   working_sett working_set;
 
-  // We will put all locations at least once into the working set.
-  forall_goto_program_instructions(i_it, goto_program)
-    put_in_working_set(working_set, i_it);
+  // Put the first location in the working set
+  if(!goto_program.empty())
+    put_in_working_set(
+      working_set,
+      goto_program.instructions.begin());
 
   bool new_data=false;