make_top, make_bottom, make_entry are now are required

src/analyses/ai.h

@@ -54,19 +54,13 @@ class ai_domain_baset
   }
 
   // no states
-  virtual void make_bottom()
-  {
-  }
+  virtual void make_bottom()=0;
 
   // all states
-  virtual void make_top()
-  {
-  }
+  virtual void make_top()=0;
 
   // a reasonable entry-point state
-  virtual void make_entry()
-  {
-  }
+  virtual void make_entry()=0;
 
   // also add
   //

src/analyses/constant_propagator.h

@@ -16,8 +16,11 @@ Author: Peter Schrammel
 class constant_propagator_domaint:public ai_domain_baset
 {
 public:
-  virtual void transform(locationt, locationt, ai_baset &, const namespacet &);
-  virtual void output(std::ostream &, const ai_baset &, const namespacet &) const;
+  void transform(locationt, locationt, ai_baset &, const namespacet &) override final;
+  void output(std::ostream &, const ai_baset &, const namespacet &) const override final;
+  void make_top() override final { values.set_to_top(); }
+  void make_bottom() override final { values.set_to_bottom(); }
+  void make_entry() override final { values.set_to_top(); }
   bool merge(const constant_propagator_domaint &, locationt, locationt);
 
   struct valuest

src/analyses/dependence_graph.h

@@ -83,12 +83,27 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett from,
     goto_programt::const_targett to,
     ai_baset &ai,
-    const namespacet &ns);
+    const namespacet &ns) final override;
+
+  void output(
+    std::ostream &out,
+    const ai_baset &ai,
+    const namespacet &ns) const final override;
+
+  void make_top() final override
+  {
+    node_id=std::numeric_limits<node_indext>::max();
+  }
 
-  virtual void output(
-      std::ostream &out,
-      const ai_baset &ai,
-      const namespacet &ns) const;
+  void make_bottom() final override
+  {
+    node_id=std::numeric_limits<node_indext>::max();
+  }
+
+  void make_entry() final override
+  {
+    node_id=std::numeric_limits<node_indext>::max();
+  }
 
   void set_node_id(node_indext id)
   {
@@ -111,6 +126,7 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett from,
     goto_programt::const_targett to,
     dependence_grapht &dep_graph);
+
   void data_dependencies(
     goto_programt::const_targett from,
     goto_programt::const_targett to,

src/analyses/escape_analysis.h

@@ -32,33 +32,38 @@ class escape_domaint:public ai_domain_baset
   {
   }
 
-  virtual void transform(
+  void transform(
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns);
+    const namespacet &ns) override final;
 
-  virtual void output(
+  void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const;
+    const namespacet &ns) const override final;
 
   bool merge(
     const escape_domaint &b,
     locationt from,
     locationt to);
 
-  void make_bottom()
+  void make_bottom() override final
   {
     cleanup_map.clear();
     is_bottom=true;
   }
 
-  void make_top()
+  void make_top() override final
   {
     cleanup_map.clear();
     is_bottom=false;
   }
+
+  void make_entry() override final
+  {
+    make_top();
+  }
 
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;

src/analyses/global_may_alias.h

@@ -54,6 +54,11 @@ class global_may_alias_domaint:public ai_domain_baset
     aliases.clear();
   }
 
+  void make_entry()
+  {
+    aliases.clear();
+  }
+
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;
 

src/analyses/interval_domain.h

@@ -24,39 +24,48 @@ class interval_domaint:public ai_domain_baset
   // Trivial, conjunctive interval domain for both float
   // and integers. The categorization 'float' and 'integers'
   // is done by is_int and is_float.
+
+  interval_domaint():bottom(true)
+  {
+  }
 
-  virtual void transform(
+  void transform(
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns);
+    const namespacet &ns) override final;
 
-  virtual void output(
+  void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const;
+    const namespacet &ns) const override final;
 
   bool merge(
     const interval_domaint &b,
     locationt from,
     locationt to);
 
   // no states
-  virtual void make_bottom()
+  void make_bottom() override final
   {
     int_map.clear();
     float_map.clear();
     bottom=true;
   }
 
   // all states
-  virtual void make_top()
+  void make_top() override final
   {
     int_map.clear();
     float_map.clear();
     bottom=false;
   }
 
+  void make_entry() override final
+  {
+    make_top();
+  }
+
   exprt make_expression(const symbol_exprt &) const;
 
   void assume(const exprt &, const namespacet &);

src/analyses/invariant_propagation.h

@@ -35,15 +35,15 @@ class invariant_propagationt:public
 
   virtual void initialize(const goto_programt &goto_program);
   virtual void initialize(const goto_functionst &goto_functions);
-
+  
   void make_all_true();
   void make_all_false();
 
   void simplify(goto_programt &goto_program);
   void simplify(goto_functionst &goto_functions);
 
   typedef ait<invariant_set_domaint> baset;
-
+  
 protected:
   const namespacet &ns;
   value_setst &value_sets;

src/analyses/invariant_set_domain.h

@@ -27,26 +27,34 @@ class invariant_set_domaint:public ai_domain_baset
     return invariant_set.make_union(other.invariant_set);
   }
 
-  virtual void output(
+  void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const
+    const namespacet &ns) const override final
   {
     invariant_set.output("", out);
   }
 
-  virtual void initialize(
-    const namespacet &ns,
-    locationt l)
-  {
-    invariant_set.make_true();
-  }
-
   virtual void transform(
     locationt from_l,
     locationt to_l,
     ai_baset &ai,
-    const namespacet &ns);
+    const namespacet &ns) override final;
+
+  void make_top() override final
+  {
+    invariant_set.make_true();
+  }
+
+  void make_bottom() override final
+  {
+    invariant_set.make_false();
+  }
+
+  void make_entry() override final
+  {
+    invariant_set.make_true();
+  }
 };
 
 #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H

src/analyses/is_threaded.cpp

@@ -13,19 +13,28 @@ Date: October 2012
 
 class is_threaded_domaint:public ai_domain_baset
 {
-  bool has_spawn;
 public:
+  bool reachable;
+  bool has_spawn;
   bool is_threaded;
 
-  inline is_threaded_domaint():has_spawn(false), is_threaded(false)
+  inline is_threaded_domaint():
+    reachable(false),
+    has_spawn(false),
+    is_threaded(false)
   {
+    // this is bottom
   }
 
   inline bool merge(
     const is_threaded_domaint &src,
     locationt from,
     locationt to)
   {
+    bool old_reachable=reachable;
+    if(src.reachable)
+      reachable=true;
+
     bool old_h_s=has_spawn;
     if(src.has_spawn &&
        (from->is_end_function() ||
@@ -38,22 +47,41 @@ class is_threaded_domaint:public ai_domain_baset
        !from->is_end_function()))
       is_threaded=true;
 
-    return old_i_t!=is_threaded || old_h_s!=has_spawn;
+    return old_reachable!=reachable ||
+           old_i_t!=is_threaded ||
+           old_h_s!=has_spawn;
   }
 
   void transform(
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns)
+    const namespacet &ns) override final
   {
+    if(!reachable) return;
     if(from->is_start_thread() ||
        to->is_end_thread())
     {
       has_spawn=true;
       is_threaded=true;
     }
   }
+
+  void make_bottom() override final
+  {
+    reachable=has_spawn=is_threaded=false;
+  }
+
+  void make_top() override final
+  {
+    reachable=has_spawn=is_threaded=true;
+  }
+
+  void make_entry() override final
+  {
+    reachable=true;
+    has_spawn=is_threaded=false;
+  }
 };
 
 /*******************************************************************\

src/analyses/reaching_definitions.h

@@ -93,25 +93,41 @@ class rd_range_domaint:public ai_domain_baset
     bv_container=&_bv_container;
   }
 
-  virtual void transform(
-      locationt from,
-      locationt to,
-      ai_baset &ai,
-      const namespacet &ns);
-
-  virtual void output(
-      std::ostream &out,
-      const ai_baset &ai,
-      const namespacet &ns) const
+  void transform(
+    locationt from,
+    locationt to,
+    ai_baset &ai,
+    const namespacet &ns) override final;
+
+  void output(
+    std::ostream &out,
+    const ai_baset &ai,
+    const namespacet &ns) const override final
   {
     output(out);
   }
+
+  void make_top() override final
+  {
+    values.clear();
+  }
+
+  void make_bottom() override final
+  {
+    values.clear();
+  }
+
+  void make_entry() override final
+  {
+    values.clear();
+  }
 
   // returns true iff there is s.th. new
   bool merge(
     const rd_range_domaint &other,
     locationt from,
     locationt to);
+
   bool merge_shared(
     const rd_range_domaint &other,
     locationt from,