Add nondet-static option to JBMC

The option already appears in process_goto_functions before, the flag just needed to be read.

Author: svorenova

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -124,6 +124,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("cover"))
     parse_cover_options(cmdline, options);
 
+  if(cmdline.isset("nondet-static"))
+    options.set_option("nondet-static", true);
+
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
 
@@ -1095,6 +1098,10 @@ void jbmc_parse_optionst::help()
     "                              will be restricted to loaded methods in this case,\n" // NOLINT(*)
     "                              and only output after the symex phase.\n"
     "\n"
+    "Semantic transformations:\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --nondet-static              add nondeterministic initialization of variables with static lifetime\n"
+    "\n"
     "BMC options:\n"
     HELP_BMC
     "\n"

jbmc/src/jbmc/jbmc_parse_options.h

@@ -67,6 +67,7 @@ class optionst;
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(verbosity):" \
+  "(nondet-static)" \
   "(version)" \
   "(cover):(symex-coverage-report):" \
   OPT_TIMESTAMP \