Renamed the GOTO_CHECK defintions according to the new naming convention

Author: thk123

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);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -1117,7 +1117,7 @@ void cbmc_parse_optionst::help()
     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"))
@@ -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

@@ -22,7 +22,7 @@ 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)" \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -885,7 +885,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"))
@@ -1464,7 +1464,7 @@ void goto_instrument_parse_optionst::help()
     "\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

@@ -23,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)" \

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"))
@@ -695,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

@@ -28,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)" \