From 6b619e0928450f926af7f861b323c4b434516dca Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Sat, 2 Dec 2017 13:58:46 +0000
Subject: [PATCH 1/5] Deactivate preprocessing of charAt and substring

We provide functions CProverString.charAt and CProverString.substring.
The reason we deactivate these is that the internal modelling differs
from the real Java implementation because it lacks the ability to throw
exceptions, in particular for the out of bounds case.
---
 src/java_bytecode/java_string_library_preprocess.cpp | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 35ce5c63225..6cb6c6e5c96 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1890,8 +1890,10 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::java.lang.String.<init>:()V"]=
       ID_cprover_string_empty_string_func;
 
+  // CProverString.charAt differs from the Java String.charAt in that no
+  // exception is raised for the out of bounds case.
   cprover_equivalent_to_java_function
-    ["java::java.lang.String.charAt:(I)C"]=
+    ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
       ID_cprover_string_char_at_func;
   cprover_equivalent_to_java_function
     ["java::java.lang.String.codePointAt:(I)I"]=
@@ -1999,11 +2001,15 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]=
       ID_cprover_string_substring_func;
+  // CProverString.substring differs from the Java String.substring in that no
+  // exception is raised for the out of bounds case.
   cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.substring:(II)Ljava/lang/String;"]=
+    ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
+    "Ljava/lang/String;"]=
       ID_cprover_string_substring_func;
   cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.substring:(I)Ljava/lang/String;"]=
+    ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
+    "Ljava/lang/String;"]=
       ID_cprover_string_substring_func;
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=

From 5c716c13d8c77f071d602aa23f72a047bc976612 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 4 Dec 2017 15:19:23 +0000
Subject: [PATCH 2/5] Add a CProverString class for string-smoke-tests

This defines useful string functions replacing standard java functions
that cannot be directly supported in cbmc because of exception throwing.
---
 .../cprover/CProverString.class               | Bin 0 -> 790 bytes
 .../cprover/CProverString.java                |  29 ++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 regression/strings-smoke-tests/cprover/CProverString.class
 create mode 100644 regression/strings-smoke-tests/cprover/CProverString.java

diff --git a/regression/strings-smoke-tests/cprover/CProverString.class b/regression/strings-smoke-tests/cprover/CProverString.class
new file mode 100644
index 0000000000000000000000000000000000000000..c1cf5742e3955fa4c05a1d8df8a09fcc6d21d44c
GIT binary patch
literal 790
zcmZvaO;6iE5Qg9NIyN!RH*p9y(DLc{KvaoaE2Jt?B}?=}O4Yk#tY8QZG7i564zyPe
z;gVK8@B{jzs?II}TGg^NJ3Bk`%)7Jx_50^NfPL&3D8e$(!m=>!1+0kGHn0Fkc&j?r
zbgVOIZ{j4*4j8!G`NE*~#zzrD<uFd750kS&lzt8dBZ_F@age^v7%cbjB)AN^qaYb}
z`&k+%!`FVN$585LL3sK;IG<M(FD8QvdCst#Tl7DO!OhF`J9()_e>_RU=v^%I)q9`P
z@nw`gDB2SeO&D0z@xsJQY?vrxlL01b*b=58%r--NoDRF;xh(Gf17WB>-}K|)Bns*J
ze}x`e(P&0dGR%(U2z?r%E635KB~P{G`gsR<MNd<t#{*O_p`5HqyH#3AHwxZ&usd>S
z(quIm<Wy2dg?y2E0EIrF$?b2b+1?DwR}?*a27b$L=|GXCWpD{7K}UlCRoZbd;nq-}
zv-~-$WnWY4sf67?tE*GND@>ng77FB-NOhS+RmfH)Mo?8Kn)nlG+H-77G0}a`zJlR#
z=LfW@BZS_d;&I`qM<QlBkIkGJ^yhACq#3Y?(xM416Ss|ZtY8Z^cHzjo6u=i7IyGFP
HR0YjH3bl~e

literal 0
HcmV?d00001

diff --git a/regression/strings-smoke-tests/cprover/CProverString.java b/regression/strings-smoke-tests/cprover/CProverString.java
new file mode 100644
index 00000000000..572056b2100
--- /dev/null
+++ b/regression/strings-smoke-tests/cprover/CProverString.java
@@ -0,0 +1,29 @@
+package org.cprover;
+
+public final class CProverString {
+    public static char charAt(String s, int i) {
+        if (0 <= i && i < s.length())
+            return s.charAt(i);
+        else
+            return '\u0000';
+    }
+
+    public static String substring(String s, int i) {
+        if (i <= 0)
+            return s;
+        else if (i >= s.length())
+            return "";
+        else
+            return s.substring(i);
+    }
+
+    public static String substring(String s, int i, int j) {
+        if (i < 0)
+            return substring(s, 0, j);
+        if (j >= s.length())
+            return substring(s, 0, s.length() - 1);
+        if (i >= j)
+            return "";
+        return s.substring(i, j);
+    }
+}

From ef610b3f50e0fd3648b5d4e1aed1a2dd97bf2381 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 4 Dec 2017 15:20:35 +0000
Subject: [PATCH 3/5] Use CProverString functions in strings-smoke-tests

We replace calls to charAt/substring by corresponding CProverString functions.
---
 .../test_append_string.class                  | Bin 1528 -> 1577 bytes
 .../test_append_string.java                   |   2 +-
 .../java_char_array/test_char_array.class     | Bin 1012 -> 1061 bytes
 .../java_char_array/test_char_array.java      |   4 ++--
 .../java_char_at/test_char_at.class           | Bin 628 -> 677 bytes
 .../java_char_at/test_char_at.java            |   2 +-
 .../java_code_point/test_code_point.class     | Bin 999 -> 1090 bytes
 .../java_code_point/test_code_point.java      |   2 +-
 .../java_concat/test_concat.class             | Bin 798 -> 847 bytes
 .../java_concat/test_concat.java              |   2 +-
 .../java_set_char_at/test_set_char_at.class   | Bin 874 -> 923 bytes
 .../java_set_char_at/test_set_char_at.java    |   4 ++--
 .../java_substring/test_substring.class       | Bin 740 -> 804 bytes
 .../java_substring/test_substring.java        |   8 ++++----
 14 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/regression/strings-smoke-tests/java_append_string/test_append_string.class b/regression/strings-smoke-tests/java_append_string/test_append_string.class
index a0880dfa7641d265fe9409f339282df2595887c1..3594e509e8700037ca37e4a6569574dad55021e5 100644
GIT binary patch
delta 269
zcmYL@y)pw)0ENH13Cp^LNg)iKCfznV1`&zBAQ6Q4n+<z+)|g#$catIojTgvluUDrr
z3J;+76kb4K48e@*e8u_BocECjX}x?tJp(hGb*;wOJPQ^Ei$mm1mMjV^n-sg9w{%I6
zO{%Hvtz?B&fuWSinq-{~ld@!!Ey*^OK9wYsObOB#zEYAZJA&~`r|sBRPT<-3C~|e|
zhe1*6P)lm;_DA<5`_xSiB!@I4N7MzwDh!*BR;`X86T4BIe2CG(W624py^L`q<|abz
r+2_|fY`fYnRDQA+Yd`S5?Wom^{y3K_|6lkm%=Ye6cS1ZS(*v(x#J5B?

delta 205
zcmZ3<^Mjk~)W2Q(7#J8#7-A=KMTs#n*l{s1G1zl3IIuG~axpkDII}ajOssm%;>yS%
zJ~@#|Jd=mPjlrFffhjGGoxy{L!IQy@oxz)j!H2<@hry4*AH;IyVUT8!VPs%Q$xKV*
zVF+LdWMq)YN-Rs%&q>Tn*LN%~PAw|Q%+GTzD#|b7VF+Rf1{oT{!w||4#={WK5W&L`
z$q+XA4Wlw!6c0l*L(FDTraDGG&f?Of;*z4wymUqeF^$Oq%p#i~GZ!#2Zkrs!dKCan
CKrTf9

diff --git a/regression/strings-smoke-tests/java_append_string/test_append_string.java b/regression/strings-smoke-tests/java_append_string/test_append_string.java
index 26de37e97d4..83a9ddf9b4c 100644
--- a/regression/strings-smoke-tests/java_append_string/test_append_string.java
+++ b/regression/strings-smoke-tests/java_append_string/test_append_string.java
@@ -20,7 +20,7 @@ public static void check(StringBuilder sb, String str)
             sb.append(str, 2, 4);
             String res = sb.toString();
             assert(res.startsWith(init));
-            assert(res.endsWith(str.substring(2, 4)));
+            assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4)));
             assert(res.length() == init.length() + 2);
             assert(!res.equals("foobarfuz"));
         }
diff --git a/regression/strings-smoke-tests/java_char_array/test_char_array.class b/regression/strings-smoke-tests/java_char_array/test_char_array.class
index 709157cf47064f77c34da49484e471ffe8de524d..bf4d9ea4993e18b736c981646c0b0e1837fa16b2 100644
GIT binary patch
delta 224
zcmeyuzLdlA)W2Q(7#J8#7>v0XxEW-)7-SjbI2kw@<k=Y%xENSKB8m)391O}_KtUCD
z230NwH3oHd291f9)k2z#3@o{cnR!4;!&5Viok45jF*7|a9tLd&9UcZA23|%6iLAu3
zME#t^ymWoX;^NezlFa-(*P^2QB6bE{9tJ%I{mJT#@@xh?42BFwlYJO%EG6@c()E)I
zit@`+i}alXz;tj)QD$B`BLiD<Mq-g;2_u7;h7ZDAh^+PG$&5P~cTDzS%4OWKc^8uv
FBLF`JH3t9y

delta 175
zcmZ3=@rB*;)W2Q(7#J8#7!0`>xEW-)7-SjbI2kw@<k=Y%xENR<B8nUgN?breWp)M?
zE(TQwHFgH|iI&wu8jK7qxrv#1KuW_?GmM=<bK)^GZA~5qEe35K1|9}pMh1zj#Ii*F
zoW#6zeaGVB)S{Bi{5;p9qWmHr1|0_7$y$u^Y<fHl`V0n>{TXez*^)C7iyTWp=1o4r
UxPx)q<XWa&#%-HlGg&bL0Its@Z~y=R

diff --git a/regression/strings-smoke-tests/java_char_array/test_char_array.java b/regression/strings-smoke-tests/java_char_array/test_char_array.java
index 34d6f009e55..7a9351d0afb 100644
--- a/regression/strings-smoke-tests/java_char_array/test_char_array.java
+++ b/regression/strings-smoke-tests/java_char_array/test_char_array.java
@@ -8,7 +8,7 @@ public static char[] toCharArray(String s)
         char arr[] = new char[s.length()];
         // We limit arbitrarly the loop unfolding to 5
         for(int i = 0; i < length && i < 5; i++)
-        arr[i] = s.charAt(i);
+            arr[i] = org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
@@ -17,7 +17,7 @@ public static void main(int i)
         String s = "abc";
         char [] str = toCharArray(s);
         char c = str[2];
-        char a = s.charAt(0);
+        char a = org.cprover.CProverString.charAt(s, 0);
         assert(str.length == 3);
         assert(a == 'a');
         assert(c == 'c');
diff --git a/regression/strings-smoke-tests/java_char_at/test_char_at.class b/regression/strings-smoke-tests/java_char_at/test_char_at.class
index de5fe888245402b54400942a31c1deaea5296cfc..84d68a19c5e94f2a13fc5c43b1816bc511af8048 100644
GIT binary patch
delta 160
zcmeyuvXs^Q)W2Q(7#J8#7__+<xEUna86-Ivq_`NE7^FEFI2mNP7-Sjb*cs%x7}!CQ
z3S10|3`*<_$`j33@u~1I@G$VQGpO<~s4=Kde51pr!NZ`*pfy>JQP)y3zbIWlxu7V&
zEVW4AIRH!tmlS2@r86?HC1)fSIhHUoh-vs_C6*=X=OpH(>qBI%Cx<c4X52CP6Jrwq
DA`~Qo

delta 111
zcmZ3=`h~^()W2Q(7#J8#7&N&UxEUna86-Ivq_`NE7^FEFI2mL>ELnC2IW7ivkfb~p
zg93vhJA=|h^Hto+JPbSxygUpl45|~~>#(WuFsL(VOjcyn<z`FHNGx(JVPs&@nB2}d
Ln{nG@Wu_(o%b^mp

diff --git a/regression/strings-smoke-tests/java_char_at/test_char_at.java b/regression/strings-smoke-tests/java_char_at/test_char_at.java
index 3b8663d62ae..c91fc7d1cff 100644
--- a/regression/strings-smoke-tests/java_char_at/test_char_at.java
+++ b/regression/strings-smoke-tests/java_char_at/test_char_at.java
@@ -2,6 +2,6 @@ public class test_char_at {
 
   public static void main(/*String[] argv*/) {
     String s = new String("abc");
-    assert(s.charAt(2)=='c');
+    assert(org.cprover.CProverString.charAt(s, 2)=='c');
   }
 }
diff --git a/regression/strings-smoke-tests/java_code_point/test_code_point.class b/regression/strings-smoke-tests/java_code_point/test_code_point.class
index 1d5d2269325d6c4baed8f6c6f44326db9fc57985..df523be365ba4f6037c25c04e198b74e673bd336 100644
GIT binary patch
delta 305
zcmaFPeu#tX)W2Q(7#J8#7@Q|^*$Qhj=x{M`Gw8B2=y5UVGZ?Tl7*33eW;B|(ErHF5
zhryV^WU>sSY_KVV2@iuAgE<d_1%o*wgLqbAS)zVUVqUs_a7j^SUb<6hW==|K5f6hU
zgB3f2H4lRggDnq(9fLh11Aj?saY=k~eoAV5L4Ial2|I%W4}&9v)8rP$b#apUMd|v<
z1x5K~sYUwE0bm+pA|nG^az<j2V+kXJn1&C!eb%0u&WsEkCHXMLA{v^QiY7ZS)p9;y
zU}j(fdU)dGV@&0I(poG#82GfeG4L}3>B%0<mf{l_cp0RC3IrKg|1e0iGf0bzi~nKJ
JnLLBp9{}~BP8I+F

delta 196
zcmX@a@tmFO)W2Q(7#J8#80;o;*$OK&Xmc@eGib9j=x{OUGU%~0=ueD_W;B?%ErHE|
zhry7+XtE5Wtbj3t5f4y{DG!4ggDE3}_+$kpaTOj0a|R0@21^DjMh5<p)Z&u(<ouM>
z_=5b*yb^W>YaRw02HVL!jO+N=k~0#E97`A(STsB}ohQ#=s^z@Pz|6n|bVlD~Ip%V1
v2`!dw41C(m+ZgyKFJ`tB?`7a+kOImIGO+$(kY;C)78e))!=O3&GqXPcsjevm

diff --git a/regression/strings-smoke-tests/java_code_point/test_code_point.java b/regression/strings-smoke-tests/java_code_point/test_code_point.java
index faf9a2051d5..afc21c44fed 100644
--- a/regression/strings-smoke-tests/java_code_point/test_code_point.java
+++ b/regression/strings-smoke-tests/java_code_point/test_code_point.java
@@ -9,6 +9,6 @@ public static void main(/*String[] argv*/)
       assert(s.offsetByCodePoints(1,2) >= 3);
       StringBuilder sb = new StringBuilder();
       sb.appendCodePoint(0x10907);
-      assert(s.charAt(1) == sb.charAt(0));
+      assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0));
    }
 }
diff --git a/regression/strings-smoke-tests/java_concat/test_concat.class b/regression/strings-smoke-tests/java_concat/test_concat.class
index e4143c157737bffffa1af323a7918a12ba9a88e1..8802b3957d256ad0dd0290b78212e49734f7f807 100644
GIT binary patch
delta 158
zcmbQocAkyv)W2Q(7#J8#7)&Q}$xACSD04FKFsQIIsB$rIF-WsBsBtl<Gib0gXijul
zA*sc~pv|De$iQ4skk7-Q%b>^3pwGi#z+gC;iP3<~h=;+L!DO-pW1gjCeo?x9azRmk
zS!$8Ka{!nQE-A{)OJ`(YOU_6vax7tF5YzC<N-Rs%&q>Tn*N4bjPu|G5igCx}7^Xu2
D{+K3#

delta 109
zcmV-z0FwXD2A&2A%Ko~(0000q05g#a9~%MyA_)Kt03!zgBnkiu02>DYB?<s004E0k
zD3L^{7AXt>DgY}100VGvZwvq|04)pvE&wl+1pzPyFbn`O05X$10d5NhV`yP=L39BC
P1Spf@0jdGElZ^txMu-)i

diff --git a/regression/strings-smoke-tests/java_concat/test_concat.java b/regression/strings-smoke-tests/java_concat/test_concat.java
index b9909c723d4..9e861e722bf 100644
--- a/regression/strings-smoke-tests/java_concat/test_concat.java
+++ b/regression/strings-smoke-tests/java_concat/test_concat.java
@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
       int i = s.length();
       String t = new String("ppo");
       String u = s.concat(t);
-      char c = u.charAt(i);
+      char c = org.cprover.CProverString.charAt(u, i);
       assert(c == 'p');
       assert(c == 'o');
    }
diff --git a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.class
index 6e843afbe2a4b7cfb6c15ccbbbc95c7bc11bcbd0..e83ac01dcaf52d96bb387d3ef45507ac7e227d2f 100644
GIT binary patch
delta 222
zcmaFGHk&>0)W2Q(7#J8#7;L#11R3Pn85B4e6uB6f7?ijelo?dm8C1C#*gzaM1~m|&
z&dI>fpuxeQ2~wlQ&Y;c3zzfo*!^NP>pvTUjKQS<lQFY>mAWj2z216bOBL?Hi9E>s&
zCJd%L3}y`GJPbk%!i)^ej^)Wb3>FNQlWiCc*sORMtQl-37cuHuO6C`(>n9f!<(H)v
z={pC2>EM#0%)E3)2Dapk#3IKMMg}nrpRB~PME#t^ymWntto7tojBglsOrFkU4kXVr
G%?1E8r!D>f

delta 172
zcmbQu{)#Q|)W2Q(7#J8#7_7M%1R3Pn85B4e6uB6f7?ePSGCP9`7XurJ!^WTrBGfn;
z_!-nW7&JiAn(Pc(TnxM*ZQ5K6It;q(40;m-;}}&YZU|!2=V35lFr3WIC?jFSV9W!w
z!jy+Wh(VZ<f!VP<nTNrQ!F;kkqXC-*4}&Fx)#Oq}U2eAIjKm_x5=I6Vjmfte-!N{Q
Ne1gfGaoZ&3*#HBY96JC2

diff --git a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
index fd1d1fbf9e2..9e67eba0de7 100644
--- a/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
+++ b/regression/strings-smoke-tests/java_set_char_at/test_set_char_at.java
@@ -3,11 +3,11 @@ public class test_set_char_at
    public static void main(/*String[] argv*/)
    {
       String s = new String("Abc");
-      char c = s.charAt(1);
+      char c = org.cprover.CProverString.charAt(s, 1);
       StringBuilder sb = new StringBuilder(s);
       sb.setCharAt(1,'w');
       s = sb.toString();
       assert(s.equals("Awc"));
-      assert(s.charAt(2)=='c');
+      assert(org.cprover.CProverString.charAt(s, 2)=='c');
    }
 }
diff --git a/regression/strings-smoke-tests/java_substring/test_substring.class b/regression/strings-smoke-tests/java_substring/test_substring.class
index 3ba0b60e7f2f7faf54110943d367cc5063d9aaf7..086aff06ab9c3eecbb30fd8cda16b30908a4279e 100644
GIT binary patch
delta 158
zcmaFDx`d7E)W2Q(7#J8#7_=vH9pP5yVNhXE<zY}`P@j0ym`#I+L6bpivJj(&jbwgN
zx_)v&QGQu!k-l>Pm<}!}%FIh=WZ*0=O)7@6H8gy(63Y_xa}x8?^&twZCwnj|h=^g6
f$YSgl-oe1^qs_d7fyGvv1xVUyv+kJ8!*l}xSXeH`

delta 94
zcmZ3&_Joz|)W2Q(7#J8#7_=sG9pP5uVNhmJ;bBl^P@8zum`$CBL4!eavJj&NA7^oC
yQgKO9W?niYgP6wTGDZa^7LCcP82g2{F);gRGjC&HvDIb)l6Kmx+a~)k-2ec5P8Y@i

diff --git a/regression/strings-smoke-tests/java_substring/test_substring.java b/regression/strings-smoke-tests/java_substring/test_substring.java
index 03a33fdbebd..e94ee9c51cb 100644
--- a/regression/strings-smoke-tests/java_substring/test_substring.java
+++ b/regression/strings-smoke-tests/java_substring/test_substring.java
@@ -3,10 +3,10 @@ public class test_substring
    public static void main(/*String[] argv*/)
    {
       String abcdef = "AbcDef";
-      String cde = abcdef.substring(2,5);
-      char c = cde.charAt(0);
-      char d = cde.charAt(1);
-      char e = cde.charAt(2);
+      String cde = org.cprover.CProverString.substring(abcdef, 2,5);
+      char c = org.cprover.CProverString.charAt(cde, 0);
+      char d = org.cprover.CProverString.charAt(cde, 1);
+      char e = org.cprover.CProverString.charAt(cde, 2);
       assert(c == 'c');
       assert(d == 'D');
       assert(e == 'e');

From 22dc353520e6932788d6ba3673baa1c971017784 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 4 Dec 2017 15:35:06 +0000
Subject: [PATCH 4/5] Add CProverString class for jbmc-strings tests

This defines string function to replace standard Java string functions
that cannot be supported internally by CBMC because of exception throwing.
---
 .../jbmc-strings/cprover/CProverString.class  | Bin 0 -> 790 bytes
 .../jbmc-strings/cprover/CProverString.java   |  29 ++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 regression/jbmc-strings/cprover/CProverString.class
 create mode 100644 regression/jbmc-strings/cprover/CProverString.java

diff --git a/regression/jbmc-strings/cprover/CProverString.class b/regression/jbmc-strings/cprover/CProverString.class
new file mode 100644
index 0000000000000000000000000000000000000000..c1cf5742e3955fa4c05a1d8df8a09fcc6d21d44c
GIT binary patch
literal 790
zcmZvaO;6iE5Qg9NIyN!RH*p9y(DLc{KvaoaE2Jt?B}?=}O4Yk#tY8QZG7i564zyPe
z;gVK8@B{jzs?II}TGg^NJ3Bk`%)7Jx_50^NfPL&3D8e$(!m=>!1+0kGHn0Fkc&j?r
zbgVOIZ{j4*4j8!G`NE*~#zzrD<uFd750kS&lzt8dBZ_F@age^v7%cbjB)AN^qaYb}
z`&k+%!`FVN$585LL3sK;IG<M(FD8QvdCst#Tl7DO!OhF`J9()_e>_RU=v^%I)q9`P
z@nw`gDB2SeO&D0z@xsJQY?vrxlL01b*b=58%r--NoDRF;xh(Gf17WB>-}K|)Bns*J
ze}x`e(P&0dGR%(U2z?r%E635KB~P{G`gsR<MNd<t#{*O_p`5HqyH#3AHwxZ&usd>S
z(quIm<Wy2dg?y2E0EIrF$?b2b+1?DwR}?*a27b$L=|GXCWpD{7K}UlCRoZbd;nq-}
zv-~-$WnWY4sf67?tE*GND@>ng77FB-NOhS+RmfH)Mo?8Kn)nlG+H-77G0}a`zJlR#
z=LfW@BZS_d;&I`qM<QlBkIkGJ^yhACq#3Y?(xM416Ss|ZtY8Z^cHzjo6u=i7IyGFP
HR0YjH3bl~e

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/cprover/CProverString.java b/regression/jbmc-strings/cprover/CProverString.java
new file mode 100644
index 00000000000..572056b2100
--- /dev/null
+++ b/regression/jbmc-strings/cprover/CProverString.java
@@ -0,0 +1,29 @@
+package org.cprover;
+
+public final class CProverString {
+    public static char charAt(String s, int i) {
+        if (0 <= i && i < s.length())
+            return s.charAt(i);
+        else
+            return '\u0000';
+    }
+
+    public static String substring(String s, int i) {
+        if (i <= 0)
+            return s;
+        else if (i >= s.length())
+            return "";
+        else
+            return s.substring(i);
+    }
+
+    public static String substring(String s, int i, int j) {
+        if (i < 0)
+            return substring(s, 0, j);
+        if (j >= s.length())
+            return substring(s, 0, s.length() - 1);
+        if (i >= j)
+            return "";
+        return s.substring(i, j);
+    }
+}

From ac7e6490eb1a57164084a6a14c00cd0bde9ceb0f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Sat, 2 Dec 2017 14:32:00 +0000
Subject: [PATCH 5/5] Use CProverString function in jbmc tests

charAt and substring are replaced by CProver functions
---
 .../jbmc-strings/StringLastIndexOf/Test.class | Bin 968 -> 1017 bytes
 .../jbmc-strings/StringLastIndexOf/Test.java  |   2 +-
 .../StringMiscellaneous04.class               | Bin 1921 -> 1970 bytes
 .../StringMiscellaneous04.java                |   8 ++++----
 .../SubString01/SubString01.class             | Bin 829 -> 896 bytes
 .../jbmc-strings/SubString01/SubString01.java |  17 ++++++++---------
 .../java_char_array_init/test_init.class      | Bin 1348 -> 1397 bytes
 .../java_char_array_init/test_init.java       |   2 +-
 .../java_concat/test_concat.class             | Bin 798 -> 847 bytes
 .../jbmc-strings/java_concat/test_concat.java |   2 +-
 10 files changed, 15 insertions(+), 16 deletions(-)

diff --git a/regression/jbmc-strings/StringLastIndexOf/Test.class b/regression/jbmc-strings/StringLastIndexOf/Test.class
index 609cc4f33481416a6f1774684d1197b0a3874146..6f4767b8b338b840a6f2c270145789dff3d76c7a 100644
GIT binary patch
delta 179
zcmX@X{*#^S)W2Q(7#J8#7;GkTsmQ7^sB<##GH7ry$TMhy2rYI7Z7v2K23>Xry@}oj
zxb=A$3>XY~7>pQ<CyOy^s<AVe@GzJ%nDH<OFbIO=%t3?&BLhoFYH<lWgC!4x6@&HU
zB*s`v$^4>p{p5n8{Ib*{edho$9b8hBnU~JUz?PhmSmap3$RMWSla*MOsGpOVm#z<y
RwcdP+QJ9f&$K-oVuK+l?DV_iT

delta 130
zcmey#euACr)W2Q(7#J8#7_268smRJRsBtpzGN^Mg$TMhw2u*edEiMLa1|4<=-HF}@
zxb=7#^cf6z7z`PVCW|p@D)TTHGnnu&2rvkOBuqhs86yKrNNRBjJA*k7g9U@-<W$C3
bZnor%#3IKMpp?eu-;BbHjN2yjGrs}==@S>l

diff --git a/regression/jbmc-strings/StringLastIndexOf/Test.java b/regression/jbmc-strings/StringLastIndexOf/Test.java
index 38436b885bf..b86ce51169d 100644
--- a/regression/jbmc-strings/StringLastIndexOf/Test.java
+++ b/regression/jbmc-strings/StringLastIndexOf/Test.java
@@ -13,7 +13,7 @@ public void check(String input_String1, String input_String2, int i) {
                 // Contradiction with the previous condition (should fail).
                 assert "foo".lastIndexOf("") != 3;
             } else if (i == 2 && input_String2.length() > 0) {
-                int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex);
+                int lio = input_String1.lastIndexOf(org.cprover.CProverString.charAt(input_String2, 0), fromIndex);
                 if (input_String2.length() == 0)
                     assert lio == fromIndex;
             } else if (i == 3) {
diff --git a/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class
index 96733a2b713ee52903e7951bd735b827c2e8d84a..156f2f2d791f1759a63b0e04935e1c725966de44 100644
GIT binary patch
delta 366
zcmW-ZyG{a86h-$XWactnr862IG1@bzs30iv8bMJ|#P@4}aTr2CFC#HF#LAk?pGadY
zEG#Yb3;YOM3nSO&tgL;`*$>_)Z|D8@<rP2xH3ft4DNy0}U<|V|<`lR^GLHbo0>vW5
zlGq152w|BbEF&U(MZqef6l+3a6mh`>MN%+Dp(*{ob&9mO%ZRZdV^cvETcq2$C)?eh
zX?IRW-kBm1Uyfl1y9^VUBp9jbZC$PF4O5M^S_ZeRW+TOUlglVD?4js9692$H4rClM
z9O2k`Bf;1SPGy`ioa2IkRxC{`)o%@kOXz)1W;89HEv6Vs!iQ|5Wt&FB;JRpMC_{I`
zF27Vk|K-ZLag9qRLlu_exS}(oO>U~?Yu;=dTutQvS+Kd)FbSk`Rp&9g`!U@6a(xr>
N-1~Ij38bYE`2%*CQ4;_F

delta 358
zcmXAjO-lk%6o%hx=3K{{u7V&6X(a?Xm6euhV>)H2eVBchjXI5nj4(4swUM^%WS}3S
z(4s}VHvOBnEuy)!d0(D$4i9G#dJgrze&0U;#LyHmhB*;YNPbLWUciC~@Bd_xB1W-9
zvCQ`?e#DWWSQW6wIVoZtDT*|Q4GNiehGLU<mLey*K80e7-)-~A3)m5{ivsEQo=CC(
zGvh4@*mJ@pIa^}b#{t6>rU@qQ)O$7BRt-HWTb5?pt&Wj1&5p@%h_drSq`(m>0*)C@
zaO!-LxO|3l0T&FHxFVp9mZH?!U5()yRhP4QMadK@Iffg~L0hwIT{ARO<!S~MRVU?<
zA~n<*8VD1Nmu<6U=*5;**V^tUTBmDCF#)df7P|B5Ne6uOrfSMIfj2S?j(ijHHW+<y
JbNJ{>kUzk-O9ub|

diff --git a/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java
index c06e96a5ced..ce8d3a2e06c 100644
--- a/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java
+++ b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java
@@ -8,7 +8,7 @@ public static char[] toCharArray(String s)
         char arr[]=new char[s.length()];
         // We limit arbitrarly the loop unfolding to 10
         for(int i=0; i<length && i<10; i++)
-            arr[i]=s.charAt(i);
+            arr[i]=org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
@@ -16,11 +16,11 @@ public static void main(String[] args)
     {
         String s1 = "diffblue";
         String s2 = "TESTGENERATION";
-        String s3 = "	automated   ";
+        String s3 = "   automated   ";
 
         assert s1.equals("diffblue");
         assert s2.equals("TESTGENERATION");
-        assert s3.equals("   automated	 ");
+        assert s3.equals("   automated   ");
 
         System.out.printf(
           "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
@@ -43,7 +43,7 @@ public static void main(String[] args)
         int i=0;
         for (char character : charArray)
         {
-            assert character=="diffblue".charAt(i);
+            assert character==org.cprover.CProverString.charAt("diffblue", i);
             ++i;
         }
 
diff --git a/regression/jbmc-strings/SubString01/SubString01.class b/regression/jbmc-strings/SubString01/SubString01.class
index 861bf6905d377ed4734838615a71b208ff4870df..c6c9c4d4ceced75f983628dbfcc65b74265c3415 100644
GIT binary patch
delta 301
zcmZvVO-jR19K`1z#FxB8MG#S{*80^LKVGZFjY28n&V|sO3n8(uA*Cep^3rv$P;vpi
zg9}mg03O2LL^SQfjhmUp{AT8TcF3Ba->)A48fb9Lp=4r>V;vh7Y?MuGa#XOzu+70x
zDv})&y9|3ARk#fMqoyWr^nBYnaBzqt2lH4UEK23;D2aXDiMrjOpGgMK!7&73rRNWP
z(f8v}w9-_ng1b^GQN=)wFr#Iv33fXR+FC_%SgSMC9h~4aPsqJkO;jlEA5=1sN?hJd
zd<qh*Gz-#6iBNT~|DLA6c|NA){EaG0?tkGIJ<&@(G|IpFXq;IVJaDvN=VRmU2mV7$
A_y7O^

delta 286
zcmYL@%SyvQ07dVlwUbQJ8bw8@uhds+t7%1aS-Nm3F1pf%km$6eloTctxB3Z|*>&eH
zh(u7-y&vEY_#a~9LYL=q4%}P%T4;TIKfeJuz&=9}WgSZl%UCgBVpYdl1`b7qfufwj
zx{eKsO@=LOQ@Ep+B-PR5`AyZr4r&%km?oIv!k6JN^5s?7?FNH{Tc~4~V6pFC``*Bh
zdR{w@xyYnrA%-HW_XzTm$CAM8Btb`tFzPj$6rP0!ngsTLd>Zum<wX3O)E!|ZBTj<&
zHzSyL)h9X97F^|M_fCr3$pi9Z%++V7QWVB8UqH{Epug8_!!D-kOFJ~!<b;VfELF)}
F`~ZxVK>Gjy

diff --git a/regression/jbmc-strings/SubString01/SubString01.java b/regression/jbmc-strings/SubString01/SubString01.java
index c99db9b7308..8e211318613 100644
--- a/regression/jbmc-strings/SubString01/SubString01.java
+++ b/regression/jbmc-strings/SubString01/SubString01.java
@@ -1,13 +1,12 @@
 public class SubString01
 {
-   public static void main(String[] args)
-   {
-      String letters = "automatictestcasegenerationatdiffblue";
+    public static void main(String[] args)
+    {
+        String letters = "automatictestcasegenerationatdiffblue";
 
-      String tmp=letters.substring(20);
-      assert tmp.equals("erationatdiffblue");
-
-      tmp=letters.substring(9, 13);
-      assert tmp.equals("test");
-   }
+        String tmp=org.cprover.CProverString.substring(letters, 20);
+        assert tmp.equals("erationatdiffblue");
+        tmp=org.cprover.CProverString.substring(letters, 9, 13);
+        assert tmp.equals("test");
+    }
 }
diff --git a/regression/jbmc-strings/java_char_array_init/test_init.class b/regression/jbmc-strings/java_char_array_init/test_init.class
index f10bdeb92563349587ea273e1063a992dcf9c9e1..294c48eba4cc774131f18b84f9cd4968d0285632 100644
GIT binary patch
delta 191
zcmX@Y^_7e3)W2Q(7#J8#7<?vjS&JDnm~b$daxoY)n6WdMb1_&jSh6!%O^ja4V$IHA
zGnt1m-`kdl!H&V6hrxltk%vKwL7JVxiHE_N!3D&TV`O0UNX^N~2P)=aaAj~~WME3o
z;bCxR@L*)%EJ-aciO<Z-EMaHx<YDk)@Sc2_v0qa%zbIWlxu7V&EVW4AIRH!tmlS2@
fr31ATmnIcM*&35SG74`_U@Bu|+_CvOb1owQ1cNQY

delta 157
zcmWm2y9$C}7zW_?6XVyPk4A@r<~E1yXy>DK3k^XaA(%q`bsHgGN0ZRd&=d{bPis`;
z^StFl%Gc+12jF0pO4qVcGvG+rs0%bCnrI2M)AdE~2)G$j>~$GE^ce#T86}i|&lq9+
zM}<)E{4k6e6HE!3A2Mc`6HMhNY7<0(5?C-iEVCz_i)M1%Ch8DGJAzfsQ|&}_%?*7|
EU#@o{82|tP

diff --git a/regression/jbmc-strings/java_char_array_init/test_init.java b/regression/jbmc-strings/java_char_array_init/test_init.java
index 55f61983018..43b7c52ffdd 100644
--- a/regression/jbmc-strings/java_char_array_init/test_init.java
+++ b/regression/jbmc-strings/java_char_array_init/test_init.java
@@ -13,7 +13,7 @@ public static String stringOfCharArray(char arr[])
 
     public static String stringOfCharArray(char arr[], int i, int j)
     {
-        return stringOfCharArray(arr).substring(i, i+j);
+        return org.cprover.CProverString.substring(stringOfCharArray(arr), i, i+j);
     }
 
     public static void main(int i)
diff --git a/regression/jbmc-strings/java_concat/test_concat.class b/regression/jbmc-strings/java_concat/test_concat.class
index a69c05921f673cc68295af7dbb43ccd41e10f1a8..df929981f5268975d0a85b00cc5c556efb399b96 100644
GIT binary patch
delta 158
zcmbQocAkyv)W2Q(7#J8#7)&Q}$xACSD04FKFsQIIsB$rIF-WsBsBtl<Gib0gXijul
zA*sc~pv|De$iQ4skk7-Q%b>^3pwGi#z+gC;iP3<~h=;+L!DO-pW1gjCeo?x9azRmk
zS!$8Ka{!nQE-A{)OJ`(YOU_6vax7tF5YzC<N-Rs%&q>Tn*N4bjPu|G5igCx}7^Xu2
D{+K3#

delta 109
zcmV-z0FwXD2A&2A%Ko~(0000q05g#a9~%MyA_)Kt03!zgBnkiu02>DYB?<s004E0k
zD3L^{7AXt>DgY}100VGvZwvq|04)pvE&wl+1pzPyFbn`O05X$10d5NhV`yP=L39BC
P1Spf@0jdGElZ^txMu-)i

diff --git a/regression/jbmc-strings/java_concat/test_concat.java b/regression/jbmc-strings/java_concat/test_concat.java
index 6bbe753b2e4..9f4d3f5e371 100644
--- a/regression/jbmc-strings/java_concat/test_concat.java
+++ b/regression/jbmc-strings/java_concat/test_concat.java
@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
       int i = s.length();
       String t = new String("ppo");
       String u = s.concat(t);
-      char c = u.charAt(i);
+      char c = org.cprover.CProverString.charAt(u, i);
       assert(c == 'p');
       assert(c != 'p');
    }