Test for String.equals with class identifier check

Author: romainbrenguier

regression/jbmc-strings/StringEquals/Test.class

@@ -0,0 +1,18 @@
+public class Test {
+    public static void check(int i, String s) {
+        String t = "Hello World";
+        Integer x = new Integer(2);
+        if (i==0)
+            assert("Hello World".equals(t));
+        else if (i==1)
+            assert(! "Hello World".equals(s));
+        else if (i==2)
+            assert(! "Hello World".equals(x));
+        else if (i==3)
+            assert("Hello World".equals(x));
+        else if (i==4)
+            assert(! s.equals(x));
+        else if (i==5)
+            assert(s.equals(x));
+    }
+}

regression/jbmc-strings/StringEquals/Test.java

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --function Test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 6 .* SUCCESS
+assertion at file Test.java line 8 .* FAILURE
+assertion at file Test.java line 10 .* SUCCESS
+assertion at file Test.java line 12 .* FAILURE
+assertion at file Test.java line 14 .* SUCCESS
+assertion at file Test.java line 16 .* FAILURE
+--