Merge pull request #2603 from smowton/smowton/fix/stub-string-lengths

Fix stub string lengths
diffblue · Jul 24, 2018 · f6c34f2 · f6c34f2
2 parents 05bebb7 + c98688b
commit f6c34f2
Show file tree

Hide file tree

Showing 5 changed files with 29 additions and 3 deletions.
diff --git a/jbmc/regression/jbmc-strings/stub-string-length/Opaque.java b/jbmc/regression/jbmc-strings/stub-string-length/Opaque.java
@@ -0,0 +1,6 @@
+
+public class Opaque {
+
+  public static String getstr() { return null; }
+
+}
diff --git a/jbmc/regression/jbmc-strings/stub-string-length/Test.class b/jbmc/regression/jbmc-strings/stub-string-length/Test.class
diff --git a/jbmc/regression/jbmc-strings/stub-string-length/Test.java b/jbmc/regression/jbmc-strings/stub-string-length/Test.java
@@ -0,0 +1,12 @@
+
+public class Test {
+
+  public static void main() {
+
+    String s = Opaque.getstr();
+    if(s != null)
+      assert s.length() <= 10;
+
+  }
+
+}
diff --git a/jbmc/regression/jbmc-strings/stub-string-length/test.desc b/jbmc/regression/jbmc-strings/stub-string-length/test.desc
@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.main --max-nondet-string-length 10
+VERIFICATION SUCCESSFUL
+EXIT=0
+SIGNAL=0
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -499,9 +499,11 @@ int jbmc_parse_optionst::doit()
       ? std::stoul(cmdline.get_value("java-max-input-array-length"))
       : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
   object_factory_params.max_nondet_string_length =
-    cmdline.isset("string-max-input-length")
-      ? std::stoul(cmdline.get_value("string-max-input-length"))
-      : MAX_NONDET_STRING_LENGTH;
+    cmdline.isset("max-nondet-string-length")
+      ? std::stoul(cmdline.get_value("max-nondet-string-length"))
+      : cmdline.isset("string-max-input-length") // obsolete; will go away
+        ? std::stoul(cmdline.get_value("string-max-input-length"))
+        : MAX_NONDET_STRING_LENGTH;
   object_factory_params.max_nondet_tree_depth =
     cmdline.isset("java-max-input-tree-depth")
       ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))