Improve naming of command line options

Drops the 'java' prefix from the most important
java command line options. The prefix is not
required anymore since JBMC and CBMC do not
share the same command line interface anymore.

Author: peterschrammel

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -50,18 +50,38 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   throw_assertion_error = cmd.isset("throw-assertion-error");
   threading_support = cmd.isset("java-threading");
 
-  if(cmd.isset("java-max-input-array-length"))
-    object_factory_parameters.max_nondet_array_length=
+  if(cmd.isset("java-max-input-array-length")) // will go away
+  {
+    object_factory_parameters.max_nondet_array_length =
       std::stoi(cmd.get_value("java-max-input-array-length"));
-  if(cmd.isset("java-max-input-tree-depth"))
-    object_factory_parameters.max_nondet_tree_depth=
+  }
+  if(cmd.isset("max-nondet-array-length"))
+  {
+    object_factory_parameters.max_nondet_array_length =
+      std::stoi(cmd.get_value("max-nondet-array-length"));
+  }
+
+  if(cmd.isset("java-max-input-tree-depth")) // will go away
+  {
+    object_factory_parameters.max_nondet_tree_depth =
       std::stoi(cmd.get_value("java-max-input-tree-depth"));
-  if(cmd.isset("string-max-input-length"))
-    object_factory_parameters.max_nondet_string_length=
+  }
+  if(cmd.isset("max-nondet-tree-depth"))
+  {
+    object_factory_parameters.max_nondet_tree_depth =
+      std::stoi(cmd.get_value("max-nondet-tree-depth"));
+  }
+
+  if(cmd.isset("string-max-input-length")) // will go away
+  {
+    object_factory_parameters.max_nondet_string_length =
       std::stoi(cmd.get_value("string-max-input-length"));
-  else if(cmd.isset("string-max-length"))
+  }
+  if(cmd.isset("max-nondet-string-length"))
+  {
     object_factory_parameters.max_nondet_string_length =
-      std::stoi(cmd.get_value("string-max-length"));
+      std::stoi(cmd.get_value("max-nondet-string-length"));
+  }
 
   object_factory_parameters.string_printable = cmd.isset("string-printable");
   if(cmd.isset("java-max-vla-length"))

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -32,10 +32,13 @@ Author: Daniel Kroening, [email protected]
   "(throw-assertion-error)" \
   "(java-assume-inputs-non-null)" \
   "(java-throw-runtime-exceptions)" \
-  "(java-max-input-array-length):" \
-  "(java-max-input-tree-depth):" \
+  "(java-max-input-array-length):" /* will go a away */ \
+  "(max-nondet-array-length):" \
+  "(java-max-input-tree-depth):"   /* will go a away */ \
+  "(max-nondet-tree-depth):" \
   "(java-max-vla-length):" \
   "(java-cp-include-files):" \
+  "(lazy-methods)"                 /* will go a away */ \
   "(no-lazy-methods)" \
   "(lazy-methods-extra-entry-point):" \
   "(java-load-class):" \
@@ -50,9 +53,9 @@ Author: Daniel Kroening, [email protected]
   " --java-assume-inputs-non-null    never initialize reference-typed parameter to the\n"        /* NOLINT(*) */ \
   "                                  entry point with null\n"                                    /* NOLINT(*) */ \
   " --java-throw-runtime-exceptions  make implicit runtime exceptions explicit\n"                /* NOLINT(*) */ \
-  " --java-max-input-array-length N  limit input array size to <= N\n"                           /* NOLINT(*) */ \
-  " --java-max-input-tree-depth N    object references are (deterministically) set to null in\n" /* NOLINT(*) */ \
-  "                                  the object\n"                                               /* NOLINT(*) */ \
+  " --max-nondet-array-length N      limit nondet (e.g. input) array size to <= N\n"                           /* NOLINT(*) */ \
+  " --max-nondet-tree-depth N        limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
+  "                                  at level N references are set to null\n" /* NOLINT(*) */ \
   " --java-max-vla-length            limit the length of user-code-created arrays\n"             /* NOLINT(*) */ \
   " --java-cp-include-files          regexp or JSON list of files to load (with '@' prefix)\n"   /* NOLINT(*) */ \
   " --lazy-methods                   only translate methods that appear to be reachable from\n"  /* NOLINT(*) */ \

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1140,7 +1140,7 @@ void jbmc_parse_optionst::help()
     " --no-refine-strings          turn off string refinement\n"
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
     " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
-    " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)
+    " --max-nondet-string-length   bound the length of nondet (e.g. input) strings\n" // NOLINT(*)
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)

jbmc/src/jbmc/jbmc_parse_options.h

@@ -59,7 +59,8 @@ class optionst;
   "(no-refine-strings)" \
   "(string-printable)" \
   "(string-max-length):" \
-  "(string-max-input-length):" \
+  "(string-max-input-length):" /* will go away */ \
+  "(max-nondet-string-length):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_CLASS_HIERARCHY \