Add a disable option for enum-range-check

Author: angelhof

regression/goto-instrument/enum-range-check-disable/main.c

@@ -0,0 +1,22 @@
+#include <stdio.h>
+
+enum day
+{
+  sunday = 1,
+  monday,
+  tuesday = 5,
+  wednesday,
+  thursday = 10,
+  friday,
+  saturday
+};
+
+int main()
+{
+#pragma CPROVER check push
+#pragma CPROVER check disable "enum-range"
+  enum day temp = 100;
+  printf("%d\n", temp);
+#pragma CPROVER check pop
+  return 0;
+}

regression/goto-instrument/enum-range-check-disable/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--enum-range-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -1843,6 +1843,8 @@ void goto_checkt::goto_check(
         flag_resetter.set_flag(enable_memory_leak_check, false);
       else if(d.first == "disable:div-by-zero-check")
         flag_resetter.set_flag(enable_div_by_zero_check, false);
+      else if(d.first == "disable:enum-range-check")
+        flag_resetter.set_flag(enable_enum_range_check, false);
       else if(d.first == "disable:signed-overflow-check")
         flag_resetter.set_flag(enable_signed_overflow_check, false);
       else if(d.first == "disable:unsigned-overflow-check")

src/analyses/goto_check.h

@@ -54,6 +54,7 @@ void goto_check(
   " --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) */ \
 // clang-format on
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \

src/ansi-c/scanner.l

@@ -235,9 +235,10 @@ string_lit      ("L"|"u"|"U"|"u8")?["]{s_char}*["]
 CPROVER_PREFIX  "__CPROVER_"
 
 arith_check     ("conversion"|"undefined-shift"|"nan"|"div-by-zero")
+enum_check      "enum-range"
 memory_check    ("bounds"|"pointer"|"memory_leak")
 overflow_check  ("signed"|"unsigned"|"pointer"|"float")"-overflow"
-named_check     ["]({arith_check}|{memory_check}|{overflow_check})["]
+named_check     ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check})["]
 
 %x GRAMMAR
 %x COMMENT1

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1624,7 +1624,6 @@ void goto_instrument_parse_optionst::help()
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"
     HELP_GOTO_CHECK
-    " --enum-range-check           checks that all enum type expressions have values in the enum range\n" // NOLINT(*)
     " --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(*)