From c98688b34f3426fbde7d263618eae90f68ec79d6 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Tue, 24 Jul 2018 17:11:32 +0100
Subject: [PATCH] Fix stub string lengths

The --max-nondet-string-length parameter accidentally stopped applying to them when its name was changed.
---
 .../jbmc-strings/stub-string-length/Opaque.java   |   6 ++++++
 .../jbmc-strings/stub-string-length/Test.class    | Bin 0 -> 623 bytes
 .../jbmc-strings/stub-string-length/Test.java     |  12 ++++++++++++
 .../jbmc-strings/stub-string-length/test.desc     |   6 ++++++
 jbmc/src/jbmc/jbmc_parse_options.cpp              |   8 +++++---
 5 files changed, 29 insertions(+), 3 deletions(-)
 create mode 100644 jbmc/regression/jbmc-strings/stub-string-length/Opaque.java
 create mode 100644 jbmc/regression/jbmc-strings/stub-string-length/Test.class
 create mode 100644 jbmc/regression/jbmc-strings/stub-string-length/Test.java
 create mode 100644 jbmc/regression/jbmc-strings/stub-string-length/test.desc

diff --git a/jbmc/regression/jbmc-strings/stub-string-length/Opaque.java b/jbmc/regression/jbmc-strings/stub-string-length/Opaque.java
new file mode 100644
index 00000000000..135bff8ea8c
--- /dev/null
+++ 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
new file mode 100644
index 0000000000000000000000000000000000000000..4aef7129e1cd81411009d6f2981d6797b675a53b
GIT binary patch
literal 623
zcmY*WT~8B16g_u$+i90YN~yJc3Du%)AK-;IiP3;2gs;RlB=R<GCv{-i!tRtG!!wD`
zU;;)Hee=QJWQ=!KX=5gtk9*HO_nbRFe}DM~U>!{#d6a!TLM0D@Ss!zl7g+F-L0MqY
z$73uBEE8sGGD%cy^dL&MbRs*U>JjLOkloOcHZKWoy>UqJHU~XLnA+8m+8>^FRNS^;
zPMk^|5hhzkc2D-?SsE6o5^@{e@E?cY8VuvEdaG?kzO53odMqzwfB=&MPXateEr5>+
zE)1}OXM~Cctc5b_uf4vP_$H1AF}Jh?0?z}~(I6DY$b-(Y>YD#TEfedg&wdWh<oS@>
zXZy+|hG|Om#_qWEFYX2BLlyPSht&8sJ03$eLmn2P+*65;Rc|DVt(zeycv45G^1$=_
z3sk6BLws{V)+g@|__fF<@tJAffvznOQ@m%>pu?qw5%e9LG`jp5&Q9|O=5F9#qSU;F
zSMaYe@fDf(cgTLXEKbT&gqL!8EF#Bii6u;PBnSFsf4s=InGyeb$_`8y#VvA|5Z*_4
X?kBio!h2bkBm*aSWyP1$eh>cuN~?0X

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc-strings/stub-string-length/Test.java b/jbmc/regression/jbmc-strings/stub-string-length/Test.java
new file mode 100644
index 00000000000..1aa33736c5a
--- /dev/null
+++ 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
new file mode 100644
index 00000000000..fd2d62e8e45
--- /dev/null
+++ 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
index 00e11ad3bcc..100d28b660f 100644
--- 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"))