Move test --nondet-static-matching option from cbmc to goto-instrument

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,7 @@ void goto_instrument_parse_optionst::help()
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
     " --nondet-static-exclude e    same as nondet-static except for the variable e\n" //NOLINT(*)
     "                              (use multiple times if required)\n"
-    " --nondet-static-matching r   add nondeterministic initialization of variables\n"
+    " --nondet-static-matching r   add nondeterministic initialization of variables\n" // NOLINT(*)
     "                              with static lifetime matching regex r\n"
     " --function-enter <f>, --function-exit <f>, --branch <f>\n"
     "                              instruments a call to <f> at the beginning,\n" // NOLINT(*)