Merge pull request #454 from thk123/refactor/generalise-show-goto-fun…

…ctions-flag

Replaced all instances of show-goto-functions with a define

src/analyses/goto_check.h

@@ -29,13 +29,13 @@ void goto_check(
   const optionst &options,
   goto_modelt &goto_model);
 
-#define GOTO_CHECK_OPTIONS \
+#define OPT_GOTO_CHECK \
   "(bounds-check)(pointer-check)(memory-leak-check)" \
   "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
   "(float-overflow-check)(nan-check)"
 
-#define GOTO_CHECK_HELP \
+#define HELP_GOTO_CHECK \
   " --bounds-check               enable array bounds checks\n" \
   " --pointer-check              enable pointer checks\n" \
   " --memory-leak-check          enable memory leak checks\n" \
@@ -48,7 +48,7 @@ void goto_check(
   " --float-overflow-check       check floating-point for +/-Inf\n" \
   " --nan-check                  check floating-point for NaN\n" \
 
-#define GOTO_CHECK_PARSE_OPTIONS(cmdline, options) \
+#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
   options.set_option("pointer-check", cmdline.isset("pointer-check")); \
   options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \

src/cbmc/cbmc_parse_options.cpp

@@ -220,7 +220,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("propagation", true);
 
   // all checks supported by goto_check
-  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
+  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // unwind loops in java enum static initialization
   if(cmdline.isset("java-unwind-enum-static"))
@@ -1121,10 +1121,10 @@ void cbmc_parse_optionst::help()
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
-    " --show-goto-functions        show goto program\n"
+    HELP_SHOW_GOTO_FUNCTIONS
     "\n"
     "Program instrumentation options:\n"
-    GOTO_CHECK_HELP
+    HELP_GOTO_CHECK
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"

src/cbmc/cbmc_parse_options.h

@@ -30,7 +30,7 @@ class optionst;
   "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \
   "(classpath):(cp):(main-class):" \
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
-  GOTO_CHECK_OPTIONS \
+  OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \

src/clobber/clobber_parse_options.cpp

@@ -112,7 +112,7 @@ void clobber_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("unwindset", cmdline.get_value("unwindset"));
 
   // all checks supported by goto_check
-  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
+  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -425,7 +425,7 @@ bool clobber_parse_optionst::process_goto_program(
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      goto_functions.output(ns, std::cout);
+      show_goto_functions(ns, get_ui(), goto_functions);
       return true;
     }
   }
@@ -655,7 +655,7 @@ void clobber_parse_optionst::help()
     " --unsigned-char              make \"char\" unsigned by default\n"
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
-    " --show-goto-functions        show goto program\n"
+    HELP_SHOW_GOTO_FUNCTIONS
     " --ppc-macos                  set MACOS/PPC architecture\n"
     " --mm model                   set memory model (default: sc)\n"
     " --arch                       set architecture (default: "
@@ -673,7 +673,7 @@ void clobber_parse_optionst::help()
     " --round-to-zero              IEEE floating point rounding mode\n"
     "\n"
     "Program instrumentation options:\n"
-    GOTO_CHECK_HELP
+    HELP_GOTO_CHECK
     " --show-properties            show the properties\n"
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"

src/clobber/clobber_parse_options.h

@@ -15,13 +15,15 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language_ui.h>
 
 #include <analyses/goto_check.h>
+#include <goto-programs/show_goto_functions.h>
 
 class goto_functionst;
 class optionst;
 
 #define CLOBBER_OPTIONS \
   "(depth):(context-bound):(unwind):" \
-  GOTO_CHECK_OPTIONS \
+  OPT_GOTO_CHECK \
+  OPT_SHOW_GOTO_FUNCTIONS \
   "(no-assertions)(no-assumptions)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -406,9 +406,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      namespacet ns(goto_model.symbol_table);
-
-      goto_model.goto_functions.output(ns, std::cout);
+      show_goto_functions(goto_model, get_ui());
       return true;
     }
 
@@ -521,7 +519,7 @@ void goto_analyzer_parse_optionst::help()
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
-    " --show-goto-functions        show goto program\n"
+    HELP_SHOW_GOTO_FUNCTIONS
     " --show-properties            show the properties, but don't run analysis\n"
     "\n"
     "Other options:\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language_ui.h>
 
 #include <goto-programs/get_goto_model.h>
+#include <goto-programs/show_goto_functions.h>
 
 class bmct;
 class goto_functionst;
@@ -26,7 +27,8 @@ class optionst;
   "(classpath):(cp):(main-class):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
-  "(show-goto-functions)(show-loops)" \
+  OPT_SHOW_GOTO_FUNCTIONS \
+  "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)" \
   "(show-properties)(show-reachable-properties)(property):" \
   "(verbosity):(version)" \

src/goto-diff/goto_diff_parse_options.cpp

@@ -334,13 +334,8 @@ int goto_diff_parse_optionst::doit()
 
   if(cmdline.isset("show-goto-functions"))
   {
-    //ENHANCE: make UI specific
-    std::cout << "*******************************************************\n";
-    namespacet ns1(goto_model1.symbol_table);
-    goto_model1.goto_functions.output(ns1, std::cout);
-    std::cout << "*******************************************************\n";
-    namespacet ns2(goto_model2.symbol_table);
-    goto_model2.goto_functions.output(ns2, std::cout);
+    show_goto_functions(goto_model1, get_ui());
+    show_goto_functions(goto_model2, get_ui());
     return 0;
   }
 
@@ -512,7 +507,7 @@ bool goto_diff_parse_optionst::process_goto_program(
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      goto_functions.output(ns, std::cout);
+      show_goto_functions(ns, get_ui(), goto_functions);
       return true;
     }
   }
@@ -569,7 +564,7 @@ void goto_diff_parse_optionst::help()
     " goto_diff old new                 goto binaries to be compared\n"
     "\n"
     "Diff options:\n"
-    " --show-functions             show functions (default)\n"
+    HELP_SHOW_GOTO_FUNCTIONS
     " --syntactic                  do syntactic diff (default)\n"
     " -u | --unified               output unified diff\n"
     " --change-impact | \n"

src/goto-diff/goto_diff_parse_options.h

@@ -15,6 +15,7 @@ Author: Peter Schrammel
 #include <langapi/language_ui.h>
 
 #include <goto-programs/goto_model.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include "goto_diff_languages.h"
 
@@ -23,7 +24,7 @@ class optionst;
 
 #define GOTO_DIFF_OPTIONS \
   "(json-ui)" \
-  "(show-goto-functions)" \
+  OPT_SHOW_GOTO_FUNCTIONS \
   "(verbosity):(version)" \
   "u(unified)(change-impact)(forward-impact)(backward-impact)" \
   "(compact-output)"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -575,7 +575,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-goto-functions"))
     {
       namespacet ns(symbol_table);
-      goto_functions.output(ns, std::cout);
+      show_goto_functions(ns, get_ui(), goto_functions);
       return 0;
     }
 
@@ -884,7 +884,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     options.set_option("assert-to-assume", false);
 
   // all checks supported by goto_check
-  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
+  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -1456,14 +1456,14 @@ void goto_instrument_parse_optionst::help()
     " --show-properties            show the properties\n"
     " --show-symbol-table          show symbol table\n"
     " --list-symbols               list symbols with type information\n"
-    " --show-goto-functions        show goto program\n"
+    HELP_SHOW_GOTO_FUNCTIONS
     " --list-undefined-functions   list functions without body\n"
     " --show-struct-alignment      show struct members that might be concurrently accessed\n" // NOLINT(*)
     " --show-natural-loops         show natural loop heads\n"
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"
-    GOTO_CHECK_HELP
+    HELP_GOTO_CHECK
     " --uninitialized-check        add checks for uninitialized locals (experimental)\n" // NOLINT(*)
     " --error-label label          check that label is unreachable\n"
     " --stack-depth n              add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_ui.h>
 #include <goto-programs/goto_functions.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <analyses/goto_check.h>
 
@@ -22,7 +23,7 @@ Author: Daniel Kroening, [email protected]
   "(document-claims-latex)(document-claims-html)" \
   "(document-properties-latex)(document-properties-html)" \
   "(dump-c)(dump-cpp)(use-system-headers)(dot)(xml)" \
-  GOTO_CHECK_OPTIONS \
+  OPT_GOTO_CHECK \
   /* no-X-check are deprecated and ignored */ \
   "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
   "(no-nan-check)" \
@@ -43,7 +44,8 @@ Author: Daniel Kroening, [email protected]
   "(nondet-volatile)(isr):" \
   "(stack-depth):(nondet-static)" \
   "(function-enter):(function-exit):(branch):" \
-  "(show-goto-functions)(show-value-sets)" \
+  OPT_SHOW_GOTO_FUNCTIONS \
+  "(show-value-sets)" \
   "(show-global-may-alias)" \
   "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
   "(show-escape-analysis)(escape-analysis)" \

src/goto-programs/show_goto_functions.h

@@ -15,6 +15,12 @@ class goto_functionst;
 class namespacet;
 class goto_modelt;
 
+#define OPT_SHOW_GOTO_FUNCTIONS \
+  "(show-goto-functions)"
+
+#define HELP_SHOW_GOTO_FUNCTIONS \
+  " --show-goto-functions         show goto program\n"
+
 void show_goto_functions(
   const namespacet &ns,
   ui_message_handlert::uit ui,

src/symex/symex_parse_options.cpp

@@ -119,7 +119,7 @@ void symex_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("unwindset", cmdline.get_value("unwindset"));
 
   // all checks supported by goto_check
-  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
+  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -409,8 +409,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      const namespacet ns(goto_model.symbol_table);
-      goto_model.goto_functions.output(ns, std::cout);
+      show_goto_functions(goto_model, get_ui());
       return true;
     }
   }
@@ -677,7 +676,7 @@ void symex_parse_optionst::help()
     " --unsigned-char              make \"char\" unsigned by default\n"
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
-    " --show-goto-functions        show goto program\n"
+    HELP_SHOW_GOTO_FUNCTIONS
     " --ppc-macos                  set MACOS/PPC architecture\n"
     " --mm model                   set memory model (default: sc)\n"
     " --arch                       set architecture (default: "
@@ -696,7 +695,7 @@ void symex_parse_optionst::help()
     " --function name              set main function name\n"
     "\n"
     "Program instrumentation options:\n"
-    GOTO_CHECK_HELP
+    HELP_GOTO_CHECK
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"

src/symex/symex_parse_options.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/parse_options.h>
 
 #include <goto-programs/get_goto_model.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <langapi/language_ui.h>
 
@@ -27,7 +28,7 @@ class optionst;
   "(function):" \
   "D:I:" \
   "(depth):(context-bound):(branch-bound):(unwind):" \
-  GOTO_CHECK_OPTIONS \
+  OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
@@ -39,7 +40,8 @@ class optionst;
   "(ppc-macos)(unsigned-char)" \
   "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
-  "(show-locs)(show-vcc)(show-properties)(show-goto-functions)" \
+  "(show-locs)(show-vcc)(show-properties)" \
+  OPT_SHOW_GOTO_FUNCTIONS \
   "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
   "(no-simplify)(no-unwinding-assertions)(no-propagation)"
   // the last line is for CBMC-regression testing only