Skip to content

Commit fa1c003

Browse files
author
thk123
committed
Replaced all instances of show-goto-functions a define
This way if the help or command flag wants to change it can be done in one place. Also ensures that all programs that support the --show-goto- functions have it in the help output. Also ensures they all call the correct function which means flags like --json-ui will work as expected.
1 parent b5a205a commit fa1c003

12 files changed

+32
-25
lines changed

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1114,7 +1114,7 @@ void cbmc_parse_optionst::help()
11141114
"Program representations:\n"
11151115
" --show-parse-tree show parse tree\n"
11161116
" --show-symbol-table show symbol table\n"
1117-
" --show-goto-functions show goto program\n"
1117+
HELP_SHOW_GOTO_FUNCTIONS
11181118
"\n"
11191119
"Program instrumentation options:\n"
11201120
GOTO_CHECK_HELP

‎src/clobber/clobber_parse_options.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -425,7 +425,7 @@ bool clobber_parse_optionst::process_goto_program(
425425
// show it?
426426
if(cmdline.isset("show-goto-functions"))
427427
{
428-
goto_functions.output(ns, std::cout);
428+
show_goto_functions(ns, get_ui(), goto_functions);
429429
return true;
430430
}
431431
}
@@ -655,7 +655,7 @@ void clobber_parse_optionst::help()
655655
" --unsigned-char make \"char\" unsigned by default\n"
656656
" --show-parse-tree show parse tree\n"
657657
" --show-symbol-table show symbol table\n"
658-
" --show-goto-functions show goto program\n"
658+
HELP_SHOW_GOTO_FUNCTIONS
659659
" --ppc-macos set MACOS/PPC architecture\n"
660660
" --mm model set memory model (default: sc)\n"
661661
" --arch set architecture (default: "

‎src/clobber/clobber_parse_options.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,15 @@ Author: Daniel Kroening, kroening@kroening.com
1515
#include <langapi/language_ui.h>
1616

1717
#include <analyses/goto_check.h>
18+
#include <goto-programs/show_goto_functions.h>
1819

1920
class goto_functionst;
2021
class optionst;
2122

2223
#define CLOBBER_OPTIONS \
2324
"(depth):(context-bound):(unwind):" \
2425
GOTO_CHECK_OPTIONS \
26+
OPT_SHOW_GOTO_FUNCTIONS \
2527
"(no-assertions)(no-assumptions)" \
2628
"(error-label):(verbosity):(no-library)" \
2729
"(version)" \

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -406,9 +406,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
406406
// show it?
407407
if(cmdline.isset("show-goto-functions"))
408408
{
409-
namespacet ns(goto_model.symbol_table);
410-
411-
goto_model.goto_functions.output(ns, std::cout);
409+
show_goto_functions(goto_model, get_ui());
412410
return true;
413411
}
414412

@@ -521,7 +519,7 @@ void goto_analyzer_parse_optionst::help()
521519
"Program representations:\n"
522520
" --show-parse-tree show parse tree\n"
523521
" --show-symbol-table show symbol table\n"
524-
" --show-goto-functions show goto program\n"
522+
HELP_SHOW_GOTO_FUNCTIONS
525523
" --show-properties show the properties, but don't run analysis\n"
526524
"\n"
527525
"Other options:\n"

‎src/goto-analyzer/goto_analyzer_parse_options.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
1515
#include <langapi/language_ui.h>
1616

1717
#include <goto-programs/get_goto_model.h>
18+
#include <goto-programs/show_goto_functions.h>
1819

1920
class bmct;
2021
class goto_functionst;
@@ -26,7 +27,8 @@ class optionst;
2627
"(classpath):(cp):(main-class):" \
2728
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
2829
"(little-endian)(big-endian)" \
29-
"(show-goto-functions)(show-loops)" \
30+
OPT_SHOW_GOTO_FUNCTIONS \
31+
"(show-loops)" \
3032
"(show-symbol-table)(show-parse-tree)" \
3133
"(show-properties)(show-reachable-properties)(property):" \
3234
"(verbosity):(version)" \

‎src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -335,13 +335,8 @@ int goto_diff_parse_optionst::doit()
335335

336336
if(cmdline.isset("show-goto-functions"))
337337
{
338-
//ENHANCE: make UI specific
339-
std::cout << "*******************************************************\n";
340-
namespacet ns1(goto_model1.symbol_table);
341-
goto_model1.goto_functions.output(ns1, std::cout);
342-
std::cout << "*******************************************************\n";
343-
namespacet ns2(goto_model2.symbol_table);
344-
goto_model2.goto_functions.output(ns2, std::cout);
338+
show_goto_functions(goto_model1, get_ui());
339+
show_goto_functions(goto_model2, get_ui());
345340
return 0;
346341
}
347342

@@ -513,7 +508,7 @@ bool goto_diff_parse_optionst::process_goto_program(
513508
// show it?
514509
if(cmdline.isset("show-goto-functions"))
515510
{
516-
goto_functions.output(ns, std::cout);
511+
show_goto_functions(ns, get_ui(), goto_functions);
517512
return true;
518513
}
519514
}
@@ -570,7 +565,7 @@ void goto_diff_parse_optionst::help()
570565
" goto_diff old new goto binaries to be compared\n"
571566
"\n"
572567
"Diff options:\n"
573-
" --show-functions show functions (default)\n"
568+
HELP_SHOW_GOTO_FUNCTIONS
574569
" --syntactic do syntactic diff (default)\n"
575570
" -u | --unified output unified diff\n"
576571
" --change-impact | \n"

‎src/goto-diff/goto_diff_parse_options.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Peter Schrammel
1515
#include <langapi/language_ui.h>
1616

1717
#include <goto-programs/goto_model.h>
18+
#include <goto-programs/show_goto_functions.h>
1819

1920
#include "goto_diff_languages.h"
2021

@@ -23,7 +24,7 @@ class optionst;
2324

2425
#define GOTO_DIFF_OPTIONS \
2526
"(json-ui)" \
26-
"(show-goto-functions)" \
27+
OPT_SHOW_GOTO_FUNCTIONS \
2728
"(verbosity):(version)" \
2829
"u(unified)(change-impact)(forward-impact)(backward-impact)" \
2930
"(compact-output)"

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -576,7 +576,7 @@ int goto_instrument_parse_optionst::doit()
576576
if(cmdline.isset("show-goto-functions"))
577577
{
578578
namespacet ns(symbol_table);
579-
goto_functions.output(ns, std::cout);
579+
show_goto_functions(ns, get_ui(), goto_functions);
580580
return 0;
581581
}
582582

@@ -1457,7 +1457,7 @@ void goto_instrument_parse_optionst::help()
14571457
" --show-properties show the properties\n"
14581458
" --show-symbol-table show symbol table\n"
14591459
" --list-symbols list symbols with type information\n"
1460-
" --show-goto-functions show goto program\n"
1460+
HELP_SHOW_GOTO_FUNCTIONS
14611461
" --list-undefined-functions list functions without body\n"
14621462
" --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
14631463
" --show-natural-loops show natural loop heads\n"

‎src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
1414

1515
#include <langapi/language_ui.h>
1616
#include <goto-programs/goto_functions.h>
17+
#include <goto-programs/show_goto_functions.h>
1718

1819
#include <analyses/goto_check.h>
1920

@@ -43,7 +44,8 @@ Author: Daniel Kroening, kroening@kroening.com
4344
"(nondet-volatile)(isr):" \
4445
"(stack-depth):(nondet-static)" \
4546
"(function-enter):(function-exit):(branch):" \
46-
"(show-goto-functions)(show-value-sets)" \
47+
OPT_SHOW_GOTO_FUNCTIONS \
48+
"(show-value-sets)" \
4749
"(show-global-may-alias)" \
4850
"(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
4951
"(show-escape-analysis)(escape-analysis)" \

‎src/goto-programs/show_goto_functions.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,12 @@ class goto_functionst;
1515
class namespacet;
1616
class goto_modelt;
1717

18+
#define OPT_SHOW_GOTO_FUNCTIONS \
19+
"(show-goto-functions)"
20+
21+
#define HELP_SHOW_GOTO_FUNCTIONS \
22+
" --show-goto-functions show goto program\n"
23+
1824
void show_goto_functions(
1925
const namespacet &ns,
2026
ui_message_handlert::uit ui,

‎src/symex/symex_parse_options.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -409,8 +409,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
409409
// show it?
410410
if(cmdline.isset("show-goto-functions"))
411411
{
412-
const namespacet ns(goto_model.symbol_table);
413-
goto_model.goto_functions.output(ns, std::cout);
412+
show_goto_functions(goto_model, get_ui());
414413
return true;
415414
}
416415
}
@@ -677,7 +676,7 @@ void symex_parse_optionst::help()
677676
" --unsigned-char make \"char\" unsigned by default\n"
678677
" --show-parse-tree show parse tree\n"
679678
" --show-symbol-table show symbol table\n"
680-
" --show-goto-functions show goto program\n"
679+
HELP_SHOW_GOTO_FUNCTIONS
681680
" --ppc-macos set MACOS/PPC architecture\n"
682681
" --mm model set memory model (default: sc)\n"
683682
" --arch set architecture (default: "

‎src/symex/symex_parse_options.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
1313
#include <util/parse_options.h>
1414

1515
#include <goto-programs/get_goto_model.h>
16+
#include <goto-programs/show_goto_functions.h>
1617

1718
#include <langapi/language_ui.h>
1819

@@ -39,7 +40,8 @@ class optionst;
3940
"(ppc-macos)(unsigned-char)" \
4041
"(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \
4142
"(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
42-
"(show-locs)(show-vcc)(show-properties)(show-goto-functions)" \
43+
"(show-locs)(show-vcc)(show-properties)" \
44+
OPT_SHOW_GOTO_FUNCTIONS \
4345
"(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
4446
"(no-simplify)(no-unwinding-assertions)(no-propagation)"
4547
// the last line is for CBMC-regression testing only

0 commit comments

Comments
 (0)