Add options that goto-check uses to the macros

goto-check makes use of the options assertions, assumptions,
assert-to-assume and retain-trivial.  These were handled to different
degrees and in different way in each of the tools.  This commit adds
these options to the set of options in the *_GOTO_CHECK macros.  This
reduces the amount of duplication and parallel maintenance.

Author: martin

src/analyses/goto_check.h

@@ -39,7 +39,9 @@ void goto_check(
   "overflow-check)"                                                            \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
   "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
-  "(pointer-primitive-check)"
+  "(pointer-primitive-check)(error-label):"                                    \
+  "(no-assertions)(no-assumptions)"                                            \
+  "(assert-to-assume)(retain-trivial)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -54,9 +56,15 @@ void goto_check(
   " --undefined-shift-check      check shift greater than bit-width\n" \
   " --float-overflow-check       check floating-point for +/-Inf\n" \
   " --nan-check                  check floating-point for NaN\n" \
-  " --no-built-in-assertions     ignore assertions in built-in library\n" \
   " --enum-range-check           checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
-  " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */
+  " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \
+  " --error-label label          check that label is unreachable\n" \
+  " --no-built-in-assertions     ignore assertions in built-in library\n" \
+  " --no-assertions              ignore user assertions\n" \
+  " --no-assumptions             ignore user assumptions\n" \
+  " --assert-to-assume           convert user assertions to assumptions\n" \
+  " --retain-trivial             keep checks which are obviously true\n" \
+
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
@@ -72,7 +80,13 @@ void goto_check(
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("nan-check", cmdline.isset("nan-check")); \
   options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
-  options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")) /* NOLINT(whitespace/line_length) */
+  options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \
+  if(cmdline.isset("error-label")) \
+    options.set_option("error-label", cmdline.get_values("error-label")) \
 // clang-format on
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H

src/cbmc/cbmc_parse_options.cpp

@@ -114,8 +114,6 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
 void cbmc_parse_optionst::set_default_options(optionst &options)
 {
   // Default true
-  options.set_option("assertions", true);
-  options.set_option("assumptions", true);
   options.set_option("built-in-assertions", true);
   options.set_option("pretty-names", true);
   options.set_option("propagation", true);
@@ -313,18 +311,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
-  // check assertions
-  if(cmdline.isset("no-assertions"))
-    options.set_option("assertions", false);
-
-  // use assumptions
-  if(cmdline.isset("no-assumptions"))
-    options.set_option("assumptions", false);
-
-  // magic error label
-  if(cmdline.isset("error-label"))
-    options.set_option("error-label", cmdline.get_values("error-label"));
-
   // generate unwinding assertions
   if(cmdline.isset("unwinding-assertions"))
   {
@@ -1135,9 +1121,6 @@ void cbmc_parse_optionst::help()
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
-    " --no-assertions              ignore user assertions\n"
-    " --no-assumptions             ignore user assumptions\n"
-    " --error-label label          check that label is unreachable\n"
     HELP_COVER
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     // NOLINTNEXTLINE(whitespace/line_length)

src/cbmc/cbmc_parse_options.h

@@ -53,7 +53,6 @@ class optionst;
   "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
   "(object-bits):" \
   OPT_GOTO_CHECK \
-  "(no-assertions)(no-assumptions)" \
   "(malloc-fail-assert)(malloc-fail-null)" \
   "(malloc-may-fail)" \
   OPT_XML_INTERFACE \
@@ -73,7 +72,7 @@ class optionst;
   "(drop-unused-functions)" \
   "(havoc-undefined-functions)" \
   "(property):(stop-on-fail)(trace)" \
-  "(error-label):(verbosity):(no-library)" \
+  "(verbosity):(no-library)" \
   "(nondet-static)" \
   "(version)" \
   OPT_COVER \

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -131,24 +131,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     config.cpp.set_cpp11();
 #endif
 
-#if 0
-  // check assertions
-  if(cmdline.isset("no-assertions"))
-    options.set_option("assertions", false);
-  else
-    options.set_option("assertions", true);
-
-  // use assumptions
-  if(cmdline.isset("no-assumptions"))
-    options.set_option("assumptions", false);
-  else
-    options.set_option("assumptions", true);
-
-  // magic error label
-  if(cmdline.isset("error-label"))
-    options.set_option("error-label", cmdline.get_values("error-label"));
-#endif
-
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -133,22 +133,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
-  // check assertions
-  if(cmdline.isset("no-assertions"))
-    options.set_option("assertions", false);
-  else
-    options.set_option("assertions", true);
-
-  // use assumptions
-  if(cmdline.isset("no-assumptions"))
-    options.set_option("assumptions", false);
-  else
-    options.set_option("assumptions", true);
-
-  // magic error label
-  if(cmdline.isset("error-label"))
-    options.set_option("error-label", cmdline.get_values("error-label"));
-
   // generate unwinding assertions
   if(cmdline.isset("cover"))
     options.set_option("unwinding-assertions", false);

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1010,31 +1010,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   else
     options.set_option("simplify", true);
 
-  // use assumptions instead of assertions?
-  if(cmdline.isset("assert-to-assume"))
-    options.set_option("assert-to-assume", true);
-  else
-    options.set_option("assert-to-assume", false);
-
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
-  // check assertions
-  if(cmdline.isset("no-assertions"))
-    options.set_option("assertions", false);
-  else
-    options.set_option("assertions", true);
-
-  // use assumptions
-  if(cmdline.isset("no-assumptions"))
-    options.set_option("assumptions", false);
-  else
-    options.set_option("assumptions", true);
-
-  // magic error label
-  if(cmdline.isset("error-label"))
-    options.set_option("error-label", cmdline.get_value("error-label"));
-
   // unwind loops
   if(cmdline.isset("unwind"))
   {
@@ -1806,7 +1784,6 @@ void goto_instrument_parse_optionst::help()
     " --no-assertions              ignore user assertions\n"
     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(*)
     " --race-check                 add floating-point data race checks\n"
     "\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -52,8 +52,7 @@ Author: Daniel Kroening, [email protected]
   "(no-nan-check)" \
   "(remove-pointers)" \
   "(no-simplify)" \
-  "(assert-to-assume)" \
-  "(no-assertions)(no-assumptions)(uninitialized-check)" \
+  "(uninitialized-check)" \
   "(race-check)(scc)(one-event-per-cycle)" \
   "(minimum-interference)" \
   "(mm):(my-events)" \
@@ -92,7 +91,7 @@ Author: Daniel Kroening, [email protected]
   "(cav11)" \
   OPT_TIMESTAMP \
   "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
-  "(error-label):(string-abstraction)" \
+  "(string-abstraction)" \
   "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
   "(accelerate)(constant-propagator)" \
   "(k-induction):(step-case)(base-case)" \