Permit keeping trivially-true assertions

In some settings it is desirable to obtain a report of all properties
being checked, including those that are trivially true. There used to be
an option "all-claims", then renamed to "retain-trivial", but the latter
was never made available in command-line front-ends.

The option is now renamed to retain-trivial-checks, and made available
in all front-ends.

Author: tautschnig

regression/cbmc/bounds_check2/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  int A[2];
+  int x = A[1];
+}

regression/cbmc/bounds_check2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--bounds-check --retain-trivial-checks
+^Generated \d+ VCC\(s\), 0 remaining after simplification$
+^\[main.array_bounds.1\] line 4 array 'A' lower bound in A\[\(signed (long (long )?)?int\)1\]: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Generated 0 VCC\(s\), 0 remaining after simplification$

src/analyses/goto_check.cpp

@@ -70,7 +70,7 @@ class goto_checkt
       _options.get_bool_option("float-overflow-check");
     enable_simplify=_options.get_bool_option("simplify");
     enable_nan_check=_options.get_bool_option("nan-check");
-    retain_trivial=_options.get_bool_option("retain-trivial");
+    retain_trivial = _options.get_bool_option("retain-trivial-checks");
     enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
     enable_assertions=_options.get_bool_option("assertions");
     enable_built_in_assertions=_options.get_bool_option("built-in-assertions");

src/analyses/goto_check.h

@@ -39,7 +39,8 @@ 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)"                                                  \
+  "(retain-trivial-checks)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -54,9 +55,10 @@ 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) */ \
+  " --no-built-in-assertions     ignore assertions in built-in library\n" \
+  " --retain-trivial-checks      include checks that are trivially true\n" \
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
@@ -72,7 +74,10 @@ 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("retain-trivial-checks", \
+                     cmdline.isset("retain-trivial-checks")); \
+  (void)0
 // clang-format on
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H