Add test for --nondet-static-matching

Author: peterschrammel

regression/goto-instrument/nondet_static_matching/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int do_nondet_init1;
+int init1;
+
+int main(int argc, char **argv)
+{
+  static int do_nondet_init2;
+  static int init2;
+
+  assert(do_nondet_init1 == 0);
+  assert(init1 == 0);
+  assert(do_nondet_init2 == 0);
+  assert(init2 == 0);
+
+  return 0;
+}

regression/goto-instrument/nondet_static_matching/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--nondet-static-matching '.*\.c:.*nondet.*'
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+assertion do_nondet_init1 == 0: FAILURE
+assertion init1 == 0: SUCCESS
+assertion do_nondet_init2 == 0: FAILURE
+assertion init2 == 0: SUCCESS
+--
+--

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1909,7 +1909,8 @@ void goto_instrument_parse_optionst::help()
     "                              sequences match <seq>\n"
     " --undefined-function-is-assume-false\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "                              convert each call to an undefined function to assume(false)\n"
+    "                              convert each call to an undefined function"
+    " to assume(false)\n"
     HELP_INSERT_FINAL_ASSERT_FALSE
     HELP_REPLACE_FUNCTION_BODY
     HELP_RESTRICT_FUNCTION_POINTER