Merge pull request #1339 from diffblue/initialize_goto_model

New API for getting goto models

src/analyses/call_graph.cpp

@@ -18,9 +18,9 @@ call_grapht::call_grapht()
 {
 }
 
-call_grapht::call_grapht(const goto_functionst &goto_functions)
+call_grapht::call_grapht(const goto_modelt &goto_model)
 {
-  forall_goto_functions(f_it, goto_functions)
+  forall_goto_functions(f_it, goto_model.goto_functions)
   {
     const goto_programt &body=f_it->second.body;
     add(f_it->first, body);

src/analyses/call_graph.h

@@ -15,13 +15,13 @@ Author: Daniel Kroening, [email protected]
 #include <iosfwd>
 #include <map>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_model.h>
 
 class call_grapht
 {
 public:
   call_grapht();
-  explicit call_grapht(const goto_functionst &);
+  explicit call_grapht(const goto_modelt &);
 
   void output_dot(std::ostream &out) const;
   void output(std::ostream &out) const;

src/analyses/constant_propagator.h

@@ -110,11 +110,11 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
 {
 public:
   constant_propagator_ait(
-    goto_functionst &goto_functions,
-    const namespacet &ns)
+    goto_modelt &goto_model)
   {
-    operator()(goto_functions, ns);
-    replace(goto_functions, ns);
+    const namespacet ns(goto_model.symbol_table);
+    operator()(goto_model.goto_functions, ns);
+    replace(goto_model.goto_functions, ns);
   }
 
   constant_propagator_ait(

src/analyses/custom_bitvector_analysis.cpp

@@ -682,14 +682,13 @@ void custom_bitvector_analysist::instrument(goto_functionst &)
 }
 
 void custom_bitvector_analysist::check(
-  const namespacet &ns,
-  const goto_functionst &goto_functions,
+  const goto_modelt &goto_model,
   bool use_xml,
   std::ostream &out)
 {
   unsigned pass=0, fail=0, unknown=0;
 
-  forall_goto_functions(f_it, goto_functions)
+  forall_goto_functions(f_it, goto_model.goto_functions)
   {
     if(!f_it->second.body.has_assertion())
        continue;
@@ -715,6 +714,7 @@ void custom_bitvector_analysist::check(
           continue;
 
         exprt tmp=eval(i_it->guard, i_it);
+        const namespacet ns(goto_model.symbol_table);
         result=simplify_expr(tmp, ns);
 
         description=i_it->source_location.get_comment();
@@ -744,6 +744,7 @@ void custom_bitvector_analysist::check(
         if(!description.empty())
           out << ", " << description;
         out << ": ";
+        const namespacet ns(goto_model.symbol_table);
         out << from_expr(ns, f_it->first, result);
         out << '\n';
       }

src/analyses/custom_bitvector_analysis.h

@@ -128,8 +128,7 @@ class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
 public:
   void instrument(goto_functionst &);
   void check(
-    const namespacet &,
-    const goto_functionst &,
+    const goto_modelt &,
     bool xml, std::ostream &);
 
   exprt eval(const exprt &src, locationt loc)

src/analyses/escape_analysis.cpp

@@ -436,10 +436,11 @@ void escape_analysist::insert_cleanup(
 }
 
 void escape_analysist::instrument(
-  goto_functionst &goto_functions,
-  const namespacet &ns)
+  goto_modelt &goto_model)
 {
-  Forall_goto_functions(f_it, goto_functions)
+  const namespacet ns(goto_model.symbol_table);
+
+  Forall_goto_functions(f_it, goto_model.goto_functions)
   {
     Forall_goto_program_instructions(i_it, f_it->second.body)
     {

src/analyses/escape_analysis.h

@@ -95,9 +95,7 @@ class escape_domaint:public ai_domain_baset
 class escape_analysist:public ait<escape_domaint>
 {
 public:
-  void instrument(
-    goto_functionst &,
-    const namespacet &);
+  void instrument(goto_modelt &);
 
 protected:
   virtual void initialize(const goto_functionst &_goto_functions)

src/analyses/goto_rw.h

@@ -19,7 +19,7 @@ Date: April 2010
 
 #include <util/guard.h>
 
-#include <goto-programs/goto_program.h>
+#include <goto-programs/goto_model.h>
 
 #define forall_rw_range_set_r_objects(it, rw_set) \
   for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \
@@ -30,15 +30,15 @@ Date: April 2010
       it!=(rw_set).get_w_set().end(); ++it)
 
 class rw_range_sett;
-class goto_functionst;
+class goto_modelt;
 
 void goto_rw(goto_programt::const_targett target,
              rw_range_sett &rw_set);
 
-void goto_rw(const goto_programt &goto_program,
+void goto_rw(const goto_programt &,
              rw_range_sett &rw_set);
 
-void goto_rw(const goto_functionst &goto_functions,
+void goto_rw(const goto_functionst &,
              const irep_idt &function,
              rw_range_sett &rw_set);
 

src/analyses/interval_analysis.cpp

@@ -76,14 +76,13 @@ void instrument_intervals(
   }
 }
 
-void interval_analysis(
-  const namespacet &ns,
-  goto_functionst &goto_functions)
+void interval_analysis(goto_modelt &goto_model)
 {
   ait<interval_domaint> interval_analysis;
 
-  interval_analysis(goto_functions, ns);
+  const namespacet ns(goto_model.symbol_table);
+  interval_analysis(goto_model.goto_functions, ns);
 
-  Forall_goto_functions(f_it, goto_functions)
+  Forall_goto_functions(f_it, goto_model.goto_functions)
     instrument_intervals(interval_analysis, f_it->second);
 }

src/analyses/interval_analysis.h

@@ -12,11 +12,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANALYSES_INTERVAL_ANALYSIS_H
 #define CPROVER_ANALYSES_INTERVAL_ANALYSIS_H
 
-#include <util/namespace.h>
-#include <goto-programs/goto_functions.h>
+class goto_modelt;
 
-void interval_analysis(
-  const namespacet &ns,
-  goto_functionst &goto_functions);
+void interval_analysis(goto_modelt &);
 
 #endif // CPROVER_ANALYSES_INTERVAL_ANALYSIS_H

src/analyses/is_threaded.h

@@ -16,7 +16,7 @@ Date: October 2012
 
 #include <set>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_model.h>
 
 class is_threadedt
 {
@@ -27,6 +27,12 @@ class is_threadedt
     compute(goto_functions);
   }
 
+  explicit is_threadedt(
+    const goto_modelt &goto_model)
+  {
+    compute(goto_model.goto_functions);
+  }
+
   bool operator()(const goto_programt::const_targett t) const
   {
     return is_threaded_set.find(t)!=is_threaded_set.end();

src/analyses/natural_loops.cpp

@@ -13,9 +13,9 @@ Author: Georg Weissenbacher, [email protected]
 
 #include <iostream>
 
-void show_natural_loops(const goto_functionst &goto_functions)
+void show_natural_loops(const goto_modelt &goto_model)
 {
-  forall_goto_functions(it, goto_functions)
+  forall_goto_functions(it, goto_model.goto_functions)
   {
     std::cout << "*** " << it->first << '\n';
 

src/analyses/natural_loops.h

@@ -16,8 +16,7 @@ Author: Georg Weissenbacher, [email protected]
 #include <iosfwd>
 #include <set>
 
-#include <goto-programs/goto_program.h>
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_model.h>
 
 #include "cfg_dominators.h"
 
@@ -70,7 +69,7 @@ class natural_loopst:
 typedef natural_loops_templatet<goto_programt, goto_programt::targett>
     natural_loops_mutablet;
 
-void show_natural_loops(const goto_functionst &goto_functions);
+void show_natural_loops(const goto_modelt &);
 
 /// Finds all back-edges and computes the natural loops
 #ifdef DEBUG

src/cbmc/bmc.h

@@ -16,14 +16,15 @@ Author: Daniel Kroening, [email protected]
 #include <map>
 
 #include <util/options.h>
+#include <util/ui_message.h>
 
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
 #include <solvers/sat/cnf.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/smt1/smt1_dec.h>
 #include <solvers/smt2/smt2_dec.h>
-#include <langapi/language_ui.h>
+
 #include <goto-symex/symex_target_equation.h>
 #include <goto-programs/safety_checker.h>
 
@@ -56,7 +57,7 @@ class bmct:public safety_checkert
   // additional stuff
   expr_listt bmc_constraints;
 
-  void set_ui(language_uit::uit _ui) { ui=_ui; }
+  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
   // the safety_checkert interface
   virtual resultt operator()(
@@ -74,7 +75,7 @@ class bmct:public safety_checkert
   prop_convt &prop_conv;
 
   // use gui format
-  language_uit::uit ui;
+  ui_message_handlert::uit ui;
 
   virtual decision_proceduret::resultt
     run_decision_procedure(prop_convt &prop_conv);