From 746e337d219c0cca495074abed4ec1d792ab7816 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 27 Apr 2018 08:34:28 +0100 Subject: [PATCH 1/2] Set mode of if_exprt introduced in preprocessing A temporary variable is introduced later for this if_exprt and the mode needs to be known for the variable, other an invariant may fail. --- src/java_bytecode/java_string_library_preprocess.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 3c73c3e8ae6..655c696f659 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -902,10 +902,11 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr( // Although we should not reach this code if rhs is null, the association // `pointer -> length` is added to the solver anyway, so we have to make sure // the length is set to something reasonable. - const auto rhs_length = if_exprt( + auto rhs_length = if_exprt( equal_exprt(rhs, null_pointer_exprt(to_pointer_type(rhs.type()))), from_integer(0, lhs.length().type()), get_length(deref, symbol_table)); + rhs_length.set(ID_mode, ID_java); // Assignments code.add(code_assignt(lhs.length(), rhs_length), loc); From 3c697da1c4ff481f5d97b474839af9e2b00668e6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 27 Apr 2018 10:58:57 +0100 Subject: [PATCH 2/2] Add test where tmp_if_expr is introduced This checks the ID_mode fix for if_expr in preprocessing works correctly. --- .../jbmc-strings/char_escape/Test.class | Bin 0 -> 672 bytes regression/jbmc-strings/char_escape/Test.java | 19 ++++++++++++++++++ regression/jbmc-strings/char_escape/test.desc | 6 ++++++ 3 files changed, 25 insertions(+) create mode 100644 regression/jbmc-strings/char_escape/Test.class create mode 100644 regression/jbmc-strings/char_escape/Test.java create mode 100644 regression/jbmc-strings/char_escape/test.desc diff --git a/regression/jbmc-strings/char_escape/Test.class b/regression/jbmc-strings/char_escape/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..5ffa97543e07f6203d0805cd7d65dc7b0f94a79c GIT binary patch literal 672 zcmZWmO>fgc6r6SZv2oq6(6n`%Kq-YdJ&+3$QiEElk>FC`kSK_Xi<7J(m*9ld>3@OW zkPDYq0;va%{3e8$wOtj_we;rg^Xz*wyTAT?zXtFOfeRO92kR0WE(~ny;Onp@vF)OQ zs)PFu9thYkqBu$p1qwmED`2+910}G062{CxoJ7I6cikYbML|`Fk<*R-wu-Hz* z{>RthBqed4fZHC=rhWA?(uay29(sBfUW6VN;0bK#yfF&nVWXW)qj-2ci$()A6@X^! zczB3i509`XAZ5|@7I$kO96a{$1T~7#{RCESyS(k4sXj~P;N-TLwQg!Zb~u@+cpy*- zTJ<}We0r0^l5uuQU@f>yB;%in)Oq9De@ikGQg{&MP3=IM?1(rGY<<0ghtis%!bCi*aIY^^P)fP&W=EK1bBx;n?psVNnb3{k4D6>Ou Zm!kWWt+2`uWEsEFbx>NOlY42~wZDqcerEsx literal 0 HcmV?d00001 diff --git a/regression/jbmc-strings/char_escape/Test.java b/regression/jbmc-strings/char_escape/Test.java new file mode 100644 index 00000000000..791563bbbc0 --- /dev/null +++ b/regression/jbmc-strings/char_escape/Test.java @@ -0,0 +1,19 @@ +public class Test { + + public static boolean test(char c1, char c2, char c3, char c4, char c5, char c6, char c7, char c8) { + StringBuilder sb = new StringBuilder(""); + sb.append(c1); + sb.append(c2); + sb.append(c3); + sb.append(c4); + sb.append(c5); + sb.append(c6); + sb.append(c7); + sb.append(c8); + if (sb.toString().equals("\b\t\n\f\r\"\'\\")) + return true; + if (!sb.toString().equals("\b\t\n\f\r\"\'\\")) + return false; + return true; + } +} diff --git a/regression/jbmc-strings/char_escape/test.desc b/regression/jbmc-strings/char_escape/test.desc new file mode 100644 index 00000000000..53ab05408c9 --- /dev/null +++ b/regression/jbmc-strings/char_escape/test.desc @@ -0,0 +1,6 @@ +CORE +Test.class +--refine-strings --function Test.test --cover location --trace --json-ui +^EXIT=0$ +^SIGNAL=0$ +20 of 23 covered \(87.0%\)|30 of 44 covered \(68.2%\)