Skip to content

Commit e104827

Browse files
authored
Merge pull request #6934 from tautschnig/cleanup/help-stdout
Goto-harness, memory analyzer: print version, help to stdout
2 parents ea0e1b1 + f7c81f2 commit e104827

File tree

3 files changed

+29
-26
lines changed

3 files changed

+29
-26
lines changed

src/goto-harness/common_harness_generator_options.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -46,9 +46,9 @@ Author: Diffblue Ltd.
4646
" (default: 2)\n" \
4747
"--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \
4848
" <function-name>, name of the function(s) pointer parameters\n" \
49-
" that can be NULL pointing." \
49+
" that can be NULL pointing.\n" \
5050
"--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT \
51-
" path to the member to be havoced\n" \
51+
" <member-expr> path to the member to be havoced\n" \
5252
// COMMON_HARNESS_GENERATOR_HELP
5353

5454
// clang-format on

src/goto-harness/goto_harness_parse_options.cpp

+13-11
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,6 @@ Author: Diffblue Ltd.
88

99
#include "goto_harness_parse_options.h"
1010

11-
#include <algorithm>
12-
#include <fstream>
13-
#include <set>
14-
#include <string>
15-
#include <unordered_set>
16-
#include <utility>
17-
1811
#include <util/config.h>
1912
#include <util/exception_utils.h>
2013
#include <util/exit_codes.h>
@@ -23,15 +16,24 @@ Author: Diffblue Ltd.
2316
#include <util/suffix.h>
2417
#include <util/version.h>
2518

26-
#include <goto-instrument/dump_c.h>
2719
#include <goto-programs/goto_model.h>
2820
#include <goto-programs/read_goto_binary.h>
2921
#include <goto-programs/write_goto_binary.h>
3022

23+
#include <goto-instrument/dump_c.h>
24+
3125
#include "function_call_harness_generator.h"
3226
#include "goto_harness_generator_factory.h"
3327
#include "memory_snapshot_harness_generator.h"
3428

29+
#include <algorithm>
30+
#include <fstream>
31+
#include <iostream>
32+
#include <set>
33+
#include <string>
34+
#include <unordered_set>
35+
#include <utility>
36+
3537
std::unordered_set<irep_idt>
3638
get_symbol_names_from_goto_model(const goto_modelt &goto_model)
3739
{
@@ -96,7 +98,7 @@ int goto_harness_parse_optionst::doit()
9698
{
9799
if(cmdline.isset("version"))
98100
{
99-
log.status() << CBMC_VERSION << '\n';
101+
std::cout << CBMC_VERSION << '\n';
100102
return CPROVER_EXIT_SUCCESS;
101103
}
102104

@@ -170,7 +172,7 @@ int goto_harness_parse_optionst::doit()
170172

171173
void goto_harness_parse_optionst::help()
172174
{
173-
log.status()
175+
std::cout
174176
<< '\n'
175177
<< banner_string("Goto-Harness", CBMC_VERSION) << '\n'
176178
<< align_center_with_border("Copyright (C) 2019") << '\n'
@@ -195,7 +197,7 @@ void goto_harness_parse_optionst::help()
195197
<< "--harness-type one of the harness types listed below\n"
196198
<< "\n\n"
197199
<< FUNCTION_HARNESS_GENERATOR_HELP << "\n\n"
198-
<< MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP << messaget::eom;
200+
<< MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP << '\n';
199201
}
200202

201203
goto_harness_parse_optionst::goto_harness_parse_optionst(

src/memory-analyzer/memory_analyzer_parse_options.cpp

+14-13
Original file line numberDiff line numberDiff line change
@@ -11,24 +11,25 @@ Author: Malte Mues <[email protected]>
1111
/// Commandline parser for the memory analyzer executing main work.
1212

1313
#include "memory_analyzer_parse_options.h"
14-
#include "analyze_symbol.h"
1514

16-
#include <algorithm>
17-
#include <fstream>
18-
19-
#include <ansi-c/ansi_c_language.h>
15+
#include <util/config.h>
16+
#include <util/exit_codes.h>
17+
#include <util/message.h>
18+
#include <util/string_utils.h>
19+
#include <util/version.h>
2020

2121
#include <goto-programs/goto_model.h>
2222
#include <goto-programs/read_goto_binary.h>
2323
#include <goto-programs/show_symbol_table.h>
2424

25+
#include <ansi-c/ansi_c_language.h>
2526
#include <langapi/mode.h>
2627

27-
#include <util/config.h>
28-
#include <util/exit_codes.h>
29-
#include <util/message.h>
30-
#include <util/string_utils.h>
31-
#include <util/version.h>
28+
#include "analyze_symbol.h"
29+
30+
#include <algorithm>
31+
#include <fstream>
32+
#include <iostream>
3233

3334
memory_analyzer_parse_optionst::memory_analyzer_parse_optionst(
3435
int argc,
@@ -53,7 +54,7 @@ int memory_analyzer_parse_optionst::doit()
5354
{
5455
if(cmdline.isset("version"))
5556
{
56-
message.status() << CBMC_VERSION << '\n';
57+
std::cout << CBMC_VERSION << '\n';
5758
return CPROVER_EXIT_SUCCESS;
5859
}
5960

@@ -172,7 +173,7 @@ int memory_analyzer_parse_optionst::doit()
172173

173174
void memory_analyzer_parse_optionst::help()
174175
{
175-
message.status()
176+
std::cout
176177
<< '\n'
177178
<< banner_string("Memory-Analyzer", CBMC_VERSION) << '\n'
178179
<< align_center_with_border("Copyright (C) 2019") << '\n'
@@ -193,5 +194,5 @@ void memory_analyzer_parse_optionst::help()
193194
<< " --symtab-snapshot output snapshot as symbol table\n"
194195
<< " --output-file <file> write snapshot to file\n"
195196
<< " --json-ui output snapshot in JSON format\n"
196-
<< messaget::eom;
197+
<< '\n';
197198
}

0 commit comments

Comments
 (0)