From bcb076b28c5f6f3c17f85097192a8896fc7ddd33 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 19 Jan 2018 13:58:21 +0000
Subject: [PATCH] Correct tests for String.indexOf

These were using String.charAt which is no longer supported by CBMC and
we should use CProverString.charAt instead (the two differ in that
CProverString.charAt does not throw exceptions).

This problem was undecteted before because the constant "hello" was
interferring with the string-max-length value.
So this parameter is replaced by string-max-input-length which only
constrain inputs.
---
 .../jbmc-strings/StringIndexOf/Test.class     | Bin 1179 -> 1228 bytes
 .../jbmc-strings/StringIndexOf/Test.java      |   9 ++++++---
 .../jbmc-strings/StringIndexOf/test.desc      |   2 +-
 .../jbmc-strings/StringIndexOf/test2.desc     |  14 +++++++-------
 4 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/regression/jbmc-strings/StringIndexOf/Test.class b/regression/jbmc-strings/StringIndexOf/Test.class
index 736603942034bf2239b6a3d3fb85377f4ae2bceb..095327fb14f8fe56c26d68a97a2b33265038fa35 100644
GIT binary patch
delta 346
zcmYL_%Su9F6otS4s2!DKbi*>Fi{&jZry?PVD2YHQB1mW^9YoYPc<R?2G>oPV<V=Dd
zAZQRl5YnIrh~A|)i2iC28`fg8S!=QOUEm`SeE)iV1J+pS2WLj-nD-OYSqQR7Tqn^l
zK9-XPDbfZ8A%i6{f~ixhXPLIuZkVM`r!KoKr@bqsBXzO{Ir0Kuvu@jtz+0(zx;m!8
zvYQoq#fT#tX6;Nmy}C4a4uAQmD_iY`V5ru#WT`6%r}qC7{;nJDm9T}^{S;L(a1XSC
z!fP$2@Lr1-{rCwoONa%ANi#y0F;*F8iwTYupAhDPNp6U6%QR1lUx+^YJRVVq5m3VD
wPiHmjBq))jqH0%_*|{oxNk&PtN}A(=JOfO3(_0REl|A^-jBSB>j9N4z-@&6r*Z=?k

delta 297
zcmWlU&q@Me6vcnv=rlThQc_q_<e${ktbxeLRn0;O+6wKYAtZ}IX`EWL=?PlMY=YjP
zMFf&Wiyk0)fSxA0ZO-9vIp?19oqS5#U%wxpz#h)TUeByjNKmvW*=$g@s7%@~ovLP&
znnsh>)M+SIuDn~%@x9@N<BrGuAiNw6J3%lCG+Q(k=AiHUBSpO1ABPs(nw`i|C#kvf
zffu-;9BR>2`AS6vqo-!kz0neUGfIL#Mx||%z#`9oi<G=f(`24q7C0ossqh(#+_1z0
zSsq#DRd_~jx*v<FR-PmU)+kb;#DRpkl<A7<QRQ0J+))#2U91hBrSm(@Xc#}vDv1OW
MLmw$*rwD`GA0dD=rvLx|

diff --git a/regression/jbmc-strings/StringIndexOf/Test.java b/regression/jbmc-strings/StringIndexOf/Test.java
index 6732eba723a..87f3d1ee3c8 100644
--- a/regression/jbmc-strings/StringIndexOf/Test.java
+++ b/regression/jbmc-strings/StringIndexOf/Test.java
@@ -1,3 +1,6 @@
+// This test uses CProverString so should be compiled with
+// javac Test.java ../cprover/CProverString.java
+
 public class Test {
 
     public boolean check(String input_String, char input_char, int input_int) {
@@ -14,13 +17,13 @@ public boolean check(String input_String, char input_char, int input_int) {
 
         if (i == -1) {
             for (int j = lower_bound; j < input_String.length(); j++)
-                assert input_String.charAt(j) != input_char;
+                assert org.cprover.CProverString.charAt(input_String, j) != input_char;
         } else {
             assert i >= lower_bound;
-            assert input_String.charAt(i) == input_char;
+            assert org.cprover.CProverString.charAt(input_String, i) == input_char;
 
             for (int j = lower_bound; j < i; j++)
-                assert input_String.charAt(j) != input_char;
+                assert org.cprover.CProverString.charAt(input_String, j) != input_char;
         }
         return true;
     }
diff --git a/regression/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc
index 9c17878eb94..8b52eaea4dd 100644
--- a/regression/jbmc-strings/StringIndexOf/test.desc
+++ b/regression/jbmc-strings/StringIndexOf/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --function Test.check --unwind 4 --string-max-length 3 --java-assume-inputs-non-null
+--refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/jbmc-strings/StringIndexOf/test2.desc b/regression/jbmc-strings/StringIndexOf/test2.desc
index 6fdbcd101f0..3bb7fe6b973 100644
--- a/regression/jbmc-strings/StringIndexOf/test2.desc
+++ b/regression/jbmc-strings/StringIndexOf/test2.desc
@@ -3,12 +3,12 @@ Test.class
 --refine-strings --function Test.check2 --unwind 10 --string-max-length 10 --java-assume-inputs-non-null
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 32 .* SUCCESS
-assertion at file Test.java line 34 .* SUCCESS
-assertion at file Test.java line 36 .* SUCCESS
-assertion at file Test.java line 38 .* SUCCESS
-assertion at file Test.java line 40 .* SUCCESS
-assertion at file Test.java line 42 .* SUCCESS
-assertion at file Test.java line 43 .* FAILURE
+assertion at file Test.java line 35 .* SUCCESS
+assertion at file Test.java line 37 .* SUCCESS
+assertion at file Test.java line 39 .* SUCCESS
+assertion at file Test.java line 41 .* SUCCESS
+assertion at file Test.java line 43 .* SUCCESS
+assertion at file Test.java line 45 .* SUCCESS
+assertion at file Test.java line 46 .* FAILURE
 ^VERIFICATION FAILED$
 --