remove spurious references to langapi/language_ui.h

Author: Daniel Kroening

src/cbmc/bmc.h

@@ -57,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()(
@@ -75,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);

src/cbmc/cbmc_parse_options.h

@@ -15,8 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 
-#include <langapi/language_ui.h>
-
 #include <analyses/goto_check.h>
 
 #include <java_bytecode/java_bytecode_language.h>

src/cbmc/cbmc_solvers.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <util/options.h>
+#include <util/ui_message.h>
 
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
@@ -25,7 +26,6 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/prop/aig_prop.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 "bv_cbmc.h"
@@ -123,15 +123,15 @@ class cbmc_solverst:public messaget
   {
   }
 
-  void set_ui(language_uit::uit _ui) { ui=_ui; }
+  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
 protected:
   const optionst &options;
   const symbol_tablet &symbol_table;
   namespacet ns;
 
   // use gui format
-  language_uit::uit ui;
+  ui_message_handlert::uit ui;
 
   std::unique_ptr<solvert> get_default();
   std::unique_ptr<solvert> get_dimacs();

src/cbmc/fault_localization.h

@@ -15,7 +15,6 @@ Author: Peter Schrammel
 #include <util/namespace.h>
 #include <util/options.h>
 #include <util/threeval.h>
-#include <langapi/language_ui.h>
 
 #include <goto-symex/symex_target_equation.h>
 

src/goto-cc/gcc_mode.h

@@ -14,12 +14,12 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_GCC_MODE_H
 #define CPROVER_GOTO_CC_GCC_MODE_H
 
-#include <util/cout_message.h>
-
 #include "compile.h"
 #include "goto_cc_mode.h"
 
-class compilet;
+#include <util/cout_message.h>
+
+#include <set>
 
 class gcc_modet:public goto_cc_modet
 {

src/goto-cc/goto_cc_mode.h

@@ -14,10 +14,10 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_GOTO_CC_MODE_H
 #define CPROVER_GOTO_CC_GOTO_CC_MODE_H
 
-#include <langapi/language_ui.h>
-
 #include "goto_cc_cmdline.h"
 
+#include <util/message.h>
+
 class goto_cc_modet:public messaget
 {
 public:

src/goto-diff/goto_diff.h

@@ -13,9 +13,9 @@ Author: Peter Schrammel
 #define CPROVER_GOTO_DIFF_GOTO_DIFF_H
 
 #include <goto-programs/goto_model.h>
-#include <langapi/language_ui.h>
-#include <util/message.h>
+
 #include <util/json.h>
+#include <util/ui_message.h>
 
 #include <ostream>
 
@@ -37,14 +37,14 @@ class goto_difft:public messaget
 
   virtual bool operator()()=0;
 
-  void set_ui(language_uit::uit _ui) { ui=_ui; }
+  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
   virtual std::ostream &output_functions(std::ostream &out) const;
 
 protected:
   const goto_modelt &goto_model1;
   const goto_modelt &goto_model2;
-  language_uit::uit ui;
+  ui_message_handlert::uit ui;
 
   unsigned total_functions_count;
   typedef std::set<irep_idt> irep_id_sett;

src/goto-diff/goto_diff_parse_options.h

@@ -15,8 +15,6 @@ Author: Peter Schrammel
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 
-#include <langapi/language_ui.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 

src/goto-instrument/goto_instrument_parse_options.h

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 
-#include <langapi/language_ui.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/remove_const_function_pointers.h>
@@ -82,15 +81,15 @@ Author: Daniel Kroening, [email protected]
 
 class goto_instrument_parse_optionst:
   public parse_options_baset,
-  public language_uit
+  public messaget
 {
 public:
   virtual int doit();
   virtual void help();
 
   goto_instrument_parse_optionst(int argc, const char **argv):
     parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv),
-    language_uit(cmdline, ui_message_handler),
+    messaget(ui_message_handler),
     ui_message_handler(cmdline, "goto-instrument"),
     function_pointer_removal_done(false),
     partial_inlining_done(false),

src/goto-programs/read_goto_binary.cpp

@@ -30,8 +30,6 @@ Module: Read Goto Programs
 #include <util/base_type.h>
 #include <util/config.h>
 
-#include <langapi/language_ui.h>
-
 #include "goto_model.h"
 #include "link_goto_model.h"
 #include "read_bin_goto_object.h"

src/solvers/refinement/bv_refinement.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
 #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
 
-#include <langapi/language_ui.h>
+#include <util/ui_message.h>
 
 #include <solvers/flattening/bv_pointers.h>
 
@@ -114,7 +114,7 @@ class bv_refinementt:public bv_pointerst
 
 protected:
   // use gui format
-  language_uit::uit ui;
+  ui_message_handlert::uit ui;
 };
 
 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H

src/solvers/refinement/string_constraint.h

@@ -20,7 +20,6 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 
-#include <langapi/language_ui.h>
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <util/refined_string_type.h>

src/symex/symex_parse_options.h

@@ -18,8 +18,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 
-#include <langapi/language_ui.h>
-
 #include <analyses/goto_check.h>
 
 #include <java_bytecode/java_bytecode_language.h>

unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -122,7 +122,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
   bv_refinementt::infot info;
   info.ns=&ns;
   info.prop=&sat_check;
-  const auto ui=language_uit::uit::PLAIN;
+  const auto ui=ui_message_handlert::uit::PLAIN;
   info.ui=ui;
   bv_refinementt solver(info);
   solver << expr;