From a3ddf7a3dbdfba5c5eee8797b9f32ab0b3a4a389 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 13 May 2019 09:57:16 +0100
Subject: [PATCH 1/2] Fix precision parsing in string_format

The 4th group in the regular expression matches `(\.\d+)?` so the dot
should be ignored before the string can be parsed to an int.
---
 src/solvers/strings/string_constraint_generator_format.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/strings/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp
index a8c67b4858b..a6a48a8c34f 100644
--- a/src/solvers/strings/string_constraint_generator_format.cpp
+++ b/src/solvers/strings/string_constraint_generator_format.cpp
@@ -198,7 +198,7 @@ static format_specifiert format_specifier_of_match(std::smatch &m)
   int index = m[1].str().empty() ? -1 : std::stoi(m[1].str());
   std::string flag = m[2].str();
   int width = m[3].str().empty() ? -1 : std::stoi(m[3].str());
-  int precision = m[4].str().empty() ? -1 : std::stoi(m[4].str());
+  int precision = m[4].str().empty() ? -1 : std::stoi(m[4].str().substr(1));
   std::string tT = m[5].str();
 
   bool dt = !tT.empty();

From efc59fd10e9bc9ec469ea8b9b213865c6696b490 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 17 May 2019 09:50:02 +0100
Subject: [PATCH 2/2] Add test for String.format with float

This checks that having a format flag with precision defined doesn't
crash the solver.
---
 .../jbmc-strings/StringFormat/Test.class      | Bin 1843 -> 2089 bytes
 .../jbmc-strings/StringFormat/Test.java       |  10 ++++++++++
 .../StringFormat/test-float1.desc             |   6 ++++++
 3 files changed, 16 insertions(+)
 create mode 100644 jbmc/regression/jbmc-strings/StringFormat/test-float1.desc

diff --git a/jbmc/regression/jbmc-strings/StringFormat/Test.class b/jbmc/regression/jbmc-strings/StringFormat/Test.class
index 4620e0f976fb37d65c49e7a91c0022597442f9de..2959bc9fa2961c5e3564a90adfcda1d646378411 100644
GIT binary patch
delta 763
zcmZvZ&u<b@5XZl7cVQpPY7j-+l0q$@P+G7Rs|BlAk@^Fb+EzuY1q5mhkwc-0r=Ij^
zLibkF^k}@PO(@Y+J^Md+GhV!VY8vMO)x@}mnb~=t_nq1AZtj0$Tlu>C;S+!e9&3<s
zieps8X$@yErXh+L$61lbEpXwSit`#Q0*Z^~1&#@hiyR4#OB_j#Nsh}LS2(V6T;oUy
z>beLwIBuHb7FToX=X1A)G^SMC(l8A+Q?D$u+4_%{y17)Y<f_9A4u7)##bH#LSMG<$
zc*WeF+dA&xu8LV58Qf#wg~d`SU#=B(+{c`bJ{&c^v3~gh9vYJLY-k=?9XaF~tm(zR
z#ic%9XrvTU@kr<t7?hdfQdI?AFJZx0m3{?mPjbt-a5?vMA)Khx^5vq~BN0gb+m0D8
z<Vey*UIEP3B_>nF!9crG^wL`|Wk%UFum$!`fbdZ?x0;L`Jci>`dsme#^BFnC)9t5Y
z@_z?@6@kP12pMQ2#(Im{{Vx;5ppY@5rUL0~n1Ve*#|lN=fp<@62%#4A-84zipxL=M
zj7#ltG%Va<vgSErw$09!&O(A2CnaJ|U|8tTfEs;?M0vvAqijRY$cNx;qIbFpQ|dkV
z8tlOay4GR+2uo%Q+UHi&5tJL~wxu`z_JeOpMQV9theGuz4q^;`MCTDlj0(`;&YDNa
r<dHuXM`#!E9I(3@aIZmCUPF;L!G+yz$vwM;iV2b)7eD1>>p1coIyian

delta 550
zcmZvYOK(k46vu!2y!PsGa8=@Quj=DoRO?Z7y|r4Z^{96#S_#s7lbZ<P)WFC$Xxf~a
zi5W34kS3ZK_y7_kMm`7wjad7*l}Jq1T6^u^{;&OCZwiZRo`3rF;UiGxPK?i9q0h1}
zrl0+>HV+5~T|U%8k;9fFF)a={>YB%d<HCS2D4Y<6gkj;Na7q{vP79-s8gt={<!sD3
z&KuTO?xkt%$!z1%!*ryvFkd(03qR(vSEk}`r9Jy>+RGObE^^5-o^Y8f2AOHp>-Qf#
zttDLLTEZ6EvbA29Kf(2^>OI?dgUN)O+%g0cwRF~UJ7J3H?3?#J`|0<O7S$P;!Y21p
zD~myAY3$Hbn`Waq>{-IR)56fHG0K}p{dQ5-x+6=2yQVYy8k9Fz^j_DsOt)p*hSkb!
zZ!(3@F^|LlF+1qab>4<E%CttkMW?fhz%El+5!y*l4oya53cZX<E5pS5Gfs!~HkmKc
zv@(6RG}Zi&V+K?SVb@=O)!YcIYc0N~^a2~aCh!*#=hgeitCI=wk|DQ|-TC#N-*>G|
Ax&QzG

diff --git a/jbmc/regression/jbmc-strings/StringFormat/Test.java b/jbmc/regression/jbmc-strings/StringFormat/Test.java
index 8dd33a0e98f..98b5d43ac97 100644
--- a/jbmc/regression/jbmc-strings/StringFormat/Test.java
+++ b/jbmc/regression/jbmc-strings/StringFormat/Test.java
@@ -49,4 +49,14 @@ public static String string3(String s, String t) {
     assert(s.length() != 1 || u.charAt(0) == u.charAt(u.length() - 1));
     return u;
   }
+
+  public static String float1(float f) {
+    String u = String.format("Pi is %.2f.", 3.14);
+    // We are not checking the exactness of the string produced, just that
+    // the solver will not crash.
+    assert(u.length() > 0);
+    assert(u.charAt(0) == 'P');
+    return u;
+  }
+
 }
diff --git a/jbmc/regression/jbmc-strings/StringFormat/test-float1.desc b/jbmc/regression/jbmc-strings/StringFormat/test-float1.desc
new file mode 100644
index 00000000000..0975e43d6a6
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/StringFormat/test-float1.desc
@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.float1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+