Merge pull request #4939 from yumibagge/yb/jbmc-regression-tg-8284

Add regression tests for [TG-8284]

Author: danpoe

jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.class renamed to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/Main.class

@@ -0,0 +1,14 @@
+public class Main {
+
+  public void constantIndexOf() {
+    String s1 = "abcabc";
+    String s2 = "bc";
+    assert s1.indexOf(s2) == 1;
+    assert s1.indexOf(s2, -10) == 1;
+    assert s1.indexOf("") == 0;
+    assert s1.indexOf(s2, 3) == 4;
+    assert s1.indexOf("cd") == -1;
+    assert s1.indexOf(s2, 10) == -1;
+    assert s1.indexOf("", 10) == -1;
+  }
+}

jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/Main.java

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/test-models-library.desc

@@ -0,0 +1,11 @@
+public class Main {
+
+  public void constantIndexOf() {
+    String s1 = "abcabc";
+    assert s1.indexOf('b') == 1;
+    assert s1.indexOf('b', -10) == 1;
+    assert s1.indexOf('b', 3) == 4;
+    assert s1.indexOf('d') == -1;
+    assert s1.indexOf('b', 10) == -1;
+  }
+}

jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/test.desc renamed to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/test.desc

@@ -0,0 +1,7 @@
+public class Main {
+
+  public void constantIndexOf(String arg) {
+    String s1 = "abcabc";
+    assert s1.indexOf(arg, 10) == -1;
+  }
+}