Skip to content

Commit 618512b

Browse files
tautschnigtautschnig
committed
Use a single implementation of eval_verbosity
Each front-end had its own, often literally same, implementation. Also this implementation implicitly referred to the maximum permitted value of "verbosity", which could possibly change.
1 parent 53ed5f9 commit 618512b

19 files changed

+61
-153
lines changed

‎src/cbmc/cbmc_parse_options.cpp

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

19-
#include <util/string2int.h>
2019
#include <util/config.h>
2120
#include <util/unicode.h>
2221
#include <util/invariant.h>
@@ -100,21 +99,6 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
10099
options.set_option("arrays-uf", "auto");
101100
}
102101

103-
void cbmc_parse_optionst::eval_verbosity()
104-
{
105-
// this is our default verbosity
106-
unsigned int v=messaget::M_STATISTICS;
107-
108-
if(cmdline.isset("verbosity"))
109-
{
110-
v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
111-
if(v>10)
112-
v=10;
113-
}
114-
115-
ui_message_handler.set_verbosity(v);
116-
}
117-
118102
void cbmc_parse_optionst::get_command_line_options(optionst &options)
119103
{
120104
if(config.set(cmdline))
@@ -435,7 +419,8 @@ int cbmc_parse_optionst::doit()
435419
return CPROVER_EXIT_EXCEPTION;
436420
}
437421

438-
eval_verbosity();
422+
eval_verbosity(
423+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
439424

440425
//
441426
// Print a banner

‎src/cbmc/cbmc_parse_options.h

-1
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,6 @@ class cbmc_parse_optionst:
112112
ui_message_handlert ui_message_handler;
113113
const path_strategy_choosert path_strategy_chooser;
114114

115-
void eval_verbosity();
116115
void register_languages();
117116
void get_command_line_options(optionst &);
118117
void preprocessing();

‎src/clobber/clobber_parse_options.cpp

+2-19
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
#include <fstream>
1616
#include <cstdlib>
1717

18-
#include <util/string2int.h>
1918
#include <util/config.h>
2019
#include <util/options.h>
2120
#include <util/memory_info.h>
@@ -45,23 +44,6 @@ clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
4544
{
4645
}
4746

48-
void clobber_parse_optionst::eval_verbosity()
49-
{
50-
// this is our default verbosity
51-
int v=messaget::M_STATISTICS;
52-
53-
if(cmdline.isset("verbosity"))
54-
{
55-
v=unsafe_string2int(cmdline.get_value("verbosity"));
56-
if(v<0)
57-
v=0;
58-
else if(v>10)
59-
v=10;
60-
}
61-
62-
ui_message_handler.set_verbosity(v);
63-
}
64-
6547
void clobber_parse_optionst::get_command_line_options(optionst &options)
6648
{
6749
if(config.set(cmdline))
@@ -115,7 +97,8 @@ int clobber_parse_optionst::doit()
11597
optionst options;
11698
get_command_line_options(options);
11799

118-
eval_verbosity();
100+
eval_verbosity(
101+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
119102

120103
goto_modelt goto_model;
121104

‎src/clobber/clobber_parse_options.h

-2
Original file line numberDiff line numberDiff line change
@@ -69,8 +69,6 @@ class clobber_parse_optionst:
6969
void report_success();
7070
void report_failure();
7171
void show_counterexample(const class goto_tracet &);
72-
73-
void eval_verbosity();
7472
};
7573

7674
#endif // CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

+2-17
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,6 @@ Author: Daniel Kroening, [email protected]
5151

5252
#include <util/options.h>
5353
#include <util/config.h>
54-
#include <util/string2int.h>
5554
#include <util/unicode.h>
5655
#include <util/exit_codes.h>
5756

@@ -81,21 +80,6 @@ void goto_analyzer_parse_optionst::register_languages()
8180
register_language(new_jsil_language);
8281
}
8382

84-
void goto_analyzer_parse_optionst::eval_verbosity()
85-
{
86-
// this is our default verbosity
87-
unsigned int v=messaget::M_STATISTICS;
88-
89-
if(cmdline.isset("verbosity"))
90-
{
91-
v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
92-
if(v>10)
93-
v=10;
94-
}
95-
96-
ui_message_handler.set_verbosity(v);
97-
}
98-
9983
void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
10084
{
10185
if(config.set(cmdline))
@@ -386,7 +370,8 @@ int goto_analyzer_parse_optionst::doit()
386370

387371
optionst options;
388372
get_command_line_options(options);
389-
eval_verbosity();
373+
eval_verbosity(
374+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
390375

391376
//
392377
// Print a banner

‎src/goto-analyzer/goto_analyzer_parse_options.h

-2
Original file line numberDiff line numberDiff line change
@@ -178,8 +178,6 @@ class goto_analyzer_parse_optionst:
178178

179179
ai_baset *build_analyzer(const optionst &, const namespacet &ns);
180180

181-
void eval_verbosity();
182-
183181
ui_message_handlert::uit get_ui()
184182
{
185183
return ui_message_handler.get_ui();

‎src/goto-cc/armcc_mode.cpp

+2-7
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ Author: CM Wintersteiger, 2006
2121

2222
#include <iostream>
2323

24-
#include <util/string2int.h>
2524
#include <util/message.h>
2625
#include <util/prefix.h>
2726
#include <util/config.h>
@@ -37,8 +36,6 @@ int armcc_modet::doit()
3736
return EX_OK;
3837
}
3938

40-
unsigned int verbosity=1;
41-
4239
compilet compiler(cmdline, message_handler, cmdline.isset("diag_error="));
4340

4441
#if 0
@@ -49,10 +46,8 @@ int armcc_modet::doit()
4946
has_prefix(base_name, "goto-link");
5047
#endif
5148

52-
if(cmdline.isset("verbosity"))
53-
verbosity=unsafe_string2int(cmdline.get_value("verbosity"));
54-
55-
message_handler.set_verbosity(verbosity);
49+
const auto verbosity = eval_verbosity(
50+
cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);
5651

5752
debug() << "ARM mode" << eom;
5853

‎src/goto-cc/as_mode.cpp

+4-10
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ Author: Michael Tautschnig
2424
#include <cstring>
2525

2626
#include <util/run.h>
27-
#include <util/string2int.h>
2827
#include <util/tempdir.h>
2928
#include <util/config.h>
3029
#include <util/get_base_name.h>
@@ -76,8 +75,6 @@ int as_modet::doit()
7675
return EX_OK;
7776
}
7877

79-
unsigned int verbosity=1;
80-
8178
bool act_as_as86=
8279
base_name=="as86" ||
8380
base_name.find("goto-as86")!=std::string::npos;
@@ -101,13 +98,10 @@ int as_modet::doit()
10198
return EX_OK; // Exit!
10299
}
103100

104-
if(cmdline.isset("w-") || cmdline.isset("warn"))
105-
verbosity=2;
106-
107-
if(cmdline.isset("verbosity"))
108-
verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
109-
110-
message_handler.set_verbosity(verbosity);
101+
auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
102+
messaget::M_WARNING : messaget::M_ERROR;
103+
eval_verbosity(
104+
cmdline.get_value("verbosity"), default_verbosity, message_handler);
111105

112106
if(act_as_as86)
113107
{

‎src/goto-cc/cw_mode.cpp

+2-7
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ Author: CM Wintersteiger, 2006
2121

2222
#include <iostream>
2323

24-
#include <util/string2int.h>
2524
#include <util/message.h>
2625
#include <util/prefix.h>
2726
#include <util/config.h>
@@ -37,8 +36,6 @@ int cw_modet::doit()
3736
return EX_OK;
3837
}
3938

40-
unsigned int verbosity=1;
41-
4239
compilet compiler(cmdline, message_handler, cmdline.isset("Werror"));
4340

4441
#if 0
@@ -49,10 +46,8 @@ int cw_modet::doit()
4946
has_prefix(base_name, "goto-link");
5047
#endif
5148

52-
if(cmdline.isset("verbosity"))
53-
verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
54-
55-
message_handler.set_verbosity(verbosity);
49+
const auto verbosity = eval_verbosity(
50+
cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);
5651

5752
debug() << "CodeWarrior mode" << eom;
5853

‎src/goto-cc/gcc_mode.cpp

+4-10
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,6 @@ Author: CM Wintersteiger, 2006
3434
#include <util/expr.h>
3535
#include <util/c_types.h>
3636
#include <util/arith_tools.h>
37-
#include <util/string2int.h>
3837
#include <util/invariant.h>
3938
#include <util/tempdir.h>
4039
#include <util/tempfile.h>
@@ -331,15 +330,10 @@ int gcc_modet::doit()
331330
linker_name(cmdline, base_name) :
332331
compiler_name(cmdline, base_name);
333332

334-
unsigned int verbosity=1;
335-
336-
if(cmdline.isset("Wall") || cmdline.isset("Wextra"))
337-
verbosity=2;
338-
339-
if(cmdline.isset("verbosity"))
340-
verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
341-
342-
gcc_message_handler.set_verbosity(verbosity);
333+
auto default_verbosity = (cmdline.isset("Wall") || cmdline.isset("Wextra")) ?
334+
messaget::M_WARNING : messaget::M_ERROR;
335+
eval_verbosity(
336+
cmdline.get_value("verbosity"), default_verbosity, gcc_message_handler);
343337

344338
bool act_as_bcc=
345339
base_name=="bcc" ||

‎src/goto-cc/ms_cl_mode.cpp

+2-7
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ Author: CM Wintersteiger, 2006
2121

2222
#include <iostream>
2323

24-
#include <util/string2int.h>
2524
#include <util/message.h>
2625
#include <util/prefix.h>
2726
#include <util/config.h>
@@ -50,8 +49,6 @@ int ms_cl_modet::doit()
5049
return EX_OK;
5150
}
5251

53-
unsigned int verbosity=1;
54-
5552
compilet compiler(cmdline, message_handler, cmdline.isset("WX"));
5653

5754
#if 0
@@ -60,10 +57,8 @@ int ms_cl_modet::doit()
6057
has_prefix(base_name, "goto-link");
6158
#endif
6259

63-
if(cmdline.isset("verbosity"))
64-
verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
65-
66-
message_handler.set_verbosity(verbosity);
60+
const auto verbosity = eval_verbosity(
61+
cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);
6762

6863
debug() << "Visual Studio mode" << eom;
6964

‎src/goto-diff/goto_diff_parse_options.cpp

+2-17
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ Author: Peter Schrammel
1616
#include <iostream>
1717
#include <memory>
1818

19-
#include <util/string2int.h>
2019
#include <util/config.h>
2120
#include <util/options.h>
2221
#include <util/make_unique.h>
@@ -83,21 +82,6 @@ ::goto_diff_parse_optionst::goto_diff_parse_optionst(
8382
{
8483
}
8584

86-
void goto_diff_parse_optionst::eval_verbosity()
87-
{
88-
// this is our default verbosity
89-
unsigned int v=messaget::M_STATISTICS;
90-
91-
if(cmdline.isset("verbosity"))
92-
{
93-
v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
94-
if(v>10)
95-
v=10;
96-
}
97-
98-
ui_message_handler.set_verbosity(v);
99-
}
100-
10185
void goto_diff_parse_optionst::get_command_line_options(optionst &options)
10286
{
10387
if(config.set(cmdline))
@@ -255,7 +239,8 @@ int goto_diff_parse_optionst::doit()
255239

256240
optionst options;
257241
get_command_line_options(options);
258-
eval_verbosity();
242+
eval_verbosity(
243+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
259244

260245
//
261246
// Print a banner

‎src/goto-diff/goto_diff_parse_options.h

-2
Original file line numberDiff line numberDiff line change
@@ -70,8 +70,6 @@ class goto_diff_parse_optionst:
7070
const optionst &options,
7171
goto_modelt &goto_model);
7272

73-
void eval_verbosity();
74-
7573
void preprocessing();
7674
};
7775

‎src/goto-instrument/goto_instrument_parse_options.cpp

+2-15
Original file line numberDiff line numberDiff line change
@@ -99,20 +99,6 @@ Author: Daniel Kroening, [email protected]
9999
#include "remove_function.h"
100100
#include "splice_call.h"
101101

102-
void goto_instrument_parse_optionst::eval_verbosity()
103-
{
104-
unsigned int v=8;
105-
106-
if(cmdline.isset("verbosity"))
107-
{
108-
v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
109-
if(v>10)
110-
v=10;
111-
}
112-
113-
ui_message_handler.set_verbosity(v);
114-
}
115-
116102
/// invoke main modules
117103
int goto_instrument_parse_optionst::doit()
118104
{
@@ -128,7 +114,8 @@ int goto_instrument_parse_optionst::doit()
128114
return CPROVER_EXIT_USAGE_ERROR;
129115
}
130116

131-
eval_verbosity();
117+
eval_verbosity(
118+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
132119

133120
try
134121
{

‎src/goto-instrument/goto_instrument_parse_options.h

-2
Original file line numberDiff line numberDiff line change
@@ -119,8 +119,6 @@ class goto_instrument_parse_optionst:
119119
void get_goto_program();
120120
void instrument_goto_program();
121121

122-
void eval_verbosity();
123-
124122
void do_indirect_call_and_rtti_removal(bool force=false);
125123
void do_remove_const_function_pointers_only();
126124
void do_partial_inlining();

0 commit comments

Comments
 (0)