From 548baea93463d493a3bfe63f30a5bb6328d6c0ff Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 31 Jan 2018 16:59:55 +0000 Subject: [PATCH] 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. --- .../java_bytecode/java_bytecode_language.cpp | 36 ++++++++++++++----- .../java_bytecode/java_bytecode_language.h | 12 ++++--- jbmc/src/jbmc/jbmc_parse_options.cpp | 2 +- jbmc/src/jbmc/jbmc_parse_options.h | 3 +- 4 files changed, 38 insertions(+), 15 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 6f051e971ee..8518e40ace8 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -51,18 +51,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 = safe_string2size_t(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 = + safe_string2size_t(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 = safe_string2size_t(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 = + safe_string2size_t(cmd.get_value("max-nondet-tree-depth")); + } + + if(cmd.isset("string-max-input-length")) // will go away + { + object_factory_parameters.max_nondet_string_length = safe_string2size_t(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 = - safe_string2size_t(cmd.get_value("string-max-length")); + safe_string2size_t(cmd.get_value("max-nondet-string-length")); + } object_factory_parameters.string_printable = cmd.isset("string-printable"); if(cmd.isset("java-max-vla-length")) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index f900ac2c52d..67c45630e1e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -32,8 +32,10 @@ Author: Daniel Kroening, kroening@kroening.com "(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 away */ \ + "(max-nondet-array-length):" \ + "(java-max-input-tree-depth):" /* will go away */ \ + "(max-nondet-tree-depth):" \ "(java-max-vla-length):" \ "(java-cp-include-files):" \ "(lazy-methods)" /* will go away */ \ @@ -51,9 +53,9 @@ Author: Daniel Kroening, kroening@kroening.com " --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(*) */ \ " --no-lazy-methods load and translate all methods given on the command line\n" /* NOLINT(*) */ \ diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 481b181b818..0283c9346f6 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -1143,7 +1143,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(*) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 177c4f92b57..9f5da915be3 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/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 \