uninitialized_domaint now has bottom

Author: Daniel Kroening

src/analyses/uninitialized_domain.cpp

@@ -31,6 +31,8 @@ void uninitialized_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
+  if(is_bottom) return;
+
   switch(from->type)
   {
   case DECL:
@@ -96,11 +98,13 @@ void uninitialized_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
-  for(uninitializedt::const_iterator
-      it=uninitialized.begin();
-      it!=uninitialized.end();
-      it++)
-    out << *it << '\n';
+  if(is_bottom)
+    out << "BOTTOM";
+  else
+  {
+    for(const auto & id : uninitialized)
+      out << id << '\n';
+  }
 }
 
 /*******************************************************************\
@@ -120,11 +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_uninitialized!=uninitialized.size();
+  return old_is_bottom!=is_bottom ||
+         old_uninitialized!=uninitialized.size();
 }

src/analyses/uninitialized_domain.h

@@ -16,7 +16,13 @@ Date: January 2010
 class uninitialized_domaint:public ai_domain_baset
 {
 public:
-  // locals that are not initialized
+  uninitialized_domaint():is_bottom(true)
+  {
+  }
+  
+  bool is_bottom;
+
+  // Locals that are declared but may not be initialized
   typedef std::set<irep_idt> uninitializedt;
   uninitializedt uninitialized;
 
@@ -33,17 +39,19 @@ class uninitialized_domaint:public ai_domain_baset
 
   void make_top() override final
   {
-    uninitialized.clear();
+    // We don't have a proper 'top', and refuse to do this.
+    assert(false);
   }
 
   void make_bottom() override final
   {
     uninitialized.clear();
+    is_bottom=true;
   }
 
   void make_entry() override final
   {
-    uninitialized.clear();
+    make_top();
   }
 
   // returns true iff there is s.th. new