Skip to content

Commit f212624

Browse files
author
Daniel Kroening
committed
remove spurious references to langapi/language_ui.h
1 parent fac6d26 commit f212624

13 files changed

+25
-28
lines changed

‎src/cbmc/bmc.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
#include <list>
1616
#include <map>
1717

18+
#include <util/ui_message.h>
1819
#include <util/options.h>
1920

2021
#include <solvers/prop/prop.h>
@@ -23,7 +24,6 @@ Author: Daniel Kroening, [email protected]
2324
#include <solvers/sat/satcheck.h>
2425
#include <solvers/smt1/smt1_dec.h>
2526
#include <solvers/smt2/smt2_dec.h>
26-
#include <langapi/language_ui.h>
2727
#include <goto-symex/symex_target_equation.h>
2828
#include <goto-programs/safety_checker.h>
2929

@@ -56,7 +56,7 @@ class bmct:public safety_checkert
5656
// additional stuff
5757
expr_listt bmc_constraints;
5858

59-
void set_ui(language_uit::uit _ui) { ui=_ui; }
59+
void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
6060

6161
// the safety_checkert interface
6262
virtual resultt operator()(
@@ -74,7 +74,7 @@ class bmct:public safety_checkert
7474
prop_convt &prop_conv;
7575

7676
// use gui format
77-
language_uit::uit ui;
77+
ui_message_handlert::uit ui;
7878

7979
virtual decision_proceduret::resultt
8080
run_decision_procedure(prop_convt &prop_conv);

‎src/cbmc/cbmc_parse_options.h

-2
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/ui_message.h>
1616
#include <util/parse_options.h>
1717

18-
#include <langapi/language_ui.h>
19-
2018
#include <analyses/goto_check.h>
2119

2220
#include <java_bytecode/java_bytecode_language.h>

‎src/cbmc/cbmc_solvers.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
1717
#include <memory>
1818

1919
#include <util/options.h>
20+
#include <util/ui_message.h>
2021

2122
#include <solvers/prop/prop.h>
2223
#include <solvers/prop/prop_conv.h>
@@ -25,7 +26,6 @@ Author: Daniel Kroening, [email protected]
2526
#include <solvers/prop/aig_prop.h>
2627
#include <solvers/smt1/smt1_dec.h>
2728
#include <solvers/smt2/smt2_dec.h>
28-
#include <langapi/language_ui.h>
2929
#include <goto-symex/symex_target_equation.h>
3030

3131
#include "bv_cbmc.h"
@@ -123,15 +123,15 @@ class cbmc_solverst:public messaget
123123
{
124124
}
125125

126-
void set_ui(language_uit::uit _ui) { ui=_ui; }
126+
void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
127127

128128
protected:
129129
const optionst &options;
130130
const symbol_tablet &symbol_table;
131131
namespacet ns;
132132

133133
// use gui format
134-
language_uit::uit ui;
134+
ui_message_handlert::uit ui;
135135

136136
std::unique_ptr<solvert> get_default();
137137
std::unique_ptr<solvert> get_dimacs();

‎src/cbmc/fault_localization.h

-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Peter Schrammel
1515
#include <util/namespace.h>
1616
#include <util/options.h>
1717
#include <util/threeval.h>
18-
#include <langapi/language_ui.h>
1918

2019
#include <goto-symex/symex_target_equation.h>
2120

‎src/goto-cc/gcc_mode.h

+2
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ Date: June 2006
1818

1919
#include "goto_cc_mode.h"
2020

21+
#include <set>
22+
2123
class gcc_modet:public goto_cc_modet
2224
{
2325
public:

‎src/goto-cc/goto_cc_mode.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,10 @@ Date: June 2006
1414
#ifndef CPROVER_GOTO_CC_GOTO_CC_MODE_H
1515
#define CPROVER_GOTO_CC_GOTO_CC_MODE_H
1616

17-
#include <langapi/language_ui.h>
18-
1917
#include "goto_cc_cmdline.h"
2018

19+
#include <util/message.h>
20+
2121
class goto_cc_modet:public messaget
2222
{
2323
public:

‎src/goto-diff/goto_diff.h

+4-4
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ Author: Peter Schrammel
1313
#define CPROVER_GOTO_DIFF_GOTO_DIFF_H
1414

1515
#include <goto-programs/goto_model.h>
16-
#include <langapi/language_ui.h>
17-
#include <util/message.h>
16+
1817
#include <util/json.h>
18+
#include <util/ui_message.h>
1919

2020
#include <ostream>
2121

@@ -37,14 +37,14 @@ class goto_difft:public messaget
3737

3838
virtual bool operator()()=0;
3939

40-
void set_ui(language_uit::uit _ui) { ui=_ui; }
40+
void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
4141

4242
virtual std::ostream &output_functions(std::ostream &out) const;
4343

4444
protected:
4545
const goto_modelt &goto_model1;
4646
const goto_modelt &goto_model2;
47-
language_uit::uit ui;
47+
ui_message_handlert::uit ui;
4848

4949
unsigned total_functions_count;
5050
typedef std::set<irep_idt> irep_id_sett;

‎src/goto-diff/goto_diff_parse_options.h

-2
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,6 @@ Author: Peter Schrammel
1515
#include <util/ui_message.h>
1616
#include <util/parse_options.h>
1717

18-
#include <langapi/language_ui.h>
19-
2018
#include <goto-programs/goto_model.h>
2119
#include <goto-programs/show_goto_functions.h>
2220

‎src/goto-instrument/goto_instrument_parse_options.h

+8-3
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/ui_message.h>
1616
#include <util/parse_options.h>
1717

18-
#include <langapi/language_ui.h>
1918
#include <goto-programs/goto_functions.h>
2019
#include <goto-programs/show_goto_functions.h>
2120
#include <goto-programs/remove_const_function_pointers.h>
@@ -81,15 +80,15 @@ Author: Daniel Kroening, [email protected]
8180

8281
class goto_instrument_parse_optionst:
8382
public parse_options_baset,
84-
public language_uit
83+
public messaget
8584
{
8685
public:
8786
virtual int doit();
8887
virtual void help();
8988

9089
goto_instrument_parse_optionst(int argc, const char **argv):
9190
parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv),
92-
language_uit(cmdline, ui_message_handler),
91+
messaget(ui_message_handler),
9392
ui_message_handler(cmdline, "goto-instrument"),
9493
function_pointer_removal_done(false),
9594
partial_inlining_done(false),
@@ -115,7 +114,13 @@ class goto_instrument_parse_optionst:
115114
bool partial_inlining_done;
116115
bool remove_returns_done;
117116

117+
symbol_tablet symbol_table;
118118
goto_functionst goto_functions;
119+
120+
ui_message_handlert::uit get_ui()
121+
{
122+
return ui_message_handler.get_ui();
123+
}
119124
};
120125

121126
#endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H

‎src/goto-programs/read_goto_binary.cpp

-2
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,6 @@ Module: Read Goto Programs
3030
#include <util/base_type.h>
3131
#include <util/config.h>
3232

33-
#include <langapi/language_ui.h>
34-
3533
#include "goto_model.h"
3634
#include "link_goto_model.h"
3735
#include "read_bin_goto_object.h"

‎src/solvers/refinement/bv_refinement.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
1313
#define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
1414

15-
#include <langapi/language_ui.h>
15+
#include <util/ui_message.h>
1616

1717
#include <solvers/flattening/bv_pointers.h>
1818

@@ -42,7 +42,7 @@ class bv_refinementt:public bv_pointerst
4242

4343
using bv_pointerst::is_in_conflict;
4444

45-
void set_ui(language_uit::uit _ui) { ui=_ui; }
45+
void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
4646

4747
protected:
4848
resultt prop_solve();
@@ -113,7 +113,7 @@ class bv_refinementt:public bv_pointerst
113113
bvt parent_assumptions;
114114

115115
// use gui format
116-
language_uit::uit ui;
116+
ui_message_handlert::uit ui;
117117
};
118118

119119
#endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H

‎src/solvers/refinement/string_constraint.h

-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ Author: Romain Brenguier, [email protected]
2020
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
2121
#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
2222

23-
#include <langapi/language_ui.h>
2423
#include <solvers/refinement/bv_refinement.h>
2524
#include <solvers/refinement/string_refinement_invariant.h>
2625
#include <util/refined_string_type.h>

‎src/symex/symex_parse_options.h

-2
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,6 @@ Author: Daniel Kroening, [email protected]
1818
#include <goto-programs/goto_model.h>
1919
#include <goto-programs/show_goto_functions.h>
2020

21-
#include <langapi/language_ui.h>
22-
2321
#include <analyses/goto_check.h>
2422

2523
#include <java_bytecode/java_bytecode_language.h>

0 commit comments

Comments
 (0)