diffblue · yumibagge · Aug 16, 2019 · Jul 26, 2019 · Jul 26, 2019
diff --git a/jbmc/regression/jbmc-strings/CharAtConstantEvaluation/Main.java b/jbmc/regression/jbmc-strings/CharAtConstantEvaluation/Main.java
diff --git a/jbmc/regression/jbmc-strings/CompareToConstantEvaluation/Main.java b/jbmc/regression/jbmc-strings/CompareToConstantEvaluation/Main.java
diff --git a/...rings/CharAtConstantEvaluation/Main.class → ...rings/ConstantEvaluationCharAt/Main.class b/...rings/CharAtConstantEvaluation/Main.class → ...rings/ConstantEvaluationCharAt/Main.class
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCharAt/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationCharAt/Main.java
@@ -0,0 +1,7 @@
+public class Main {
+  public void constantCharAt() {
+    StringBuilder sb = new StringBuilder("abc");
+    char c = sb.charAt(1);
+    assert c == 'b';
+  }
+}
diff --git a/...trings/CharAtConstantEvaluation/test.desc → ...trings/ConstantEvaluationCharAt/test.desc b/...trings/CharAtConstantEvaluation/test.desc → ...trings/ConstantEvaluationCharAt/test.desc
diff --git a/...gs/CompareToConstantEvaluation/Main.class → ...gs/ConstantEvaluationCompareTo/Main.class b/...gs/CompareToConstantEvaluation/Main.class → ...gs/ConstantEvaluationCompareTo/Main.class
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/Main.java
@@ -0,0 +1,38 @@
+public class Main {
+  public void constantCompareToPass() {
+    String s1 = "ab";
+    String s2 = "abc";
+    assert s1.compareTo(s2) == -1;
+    assert s2.compareTo(s1) == 1;
+    s1 = "abc";
+    s2 = "abc";
+    assert s1.compareTo(s2) == 0;
+    s1 = "abyz";
+    s2 = "adyz";
+    assert s1.compareTo(s2) == -2;
+  }
+
+  public void constantCompareToFail1() {
+    String s1 = "ab";
+    String s2 = "abc";
+    assert s1.compareTo(s2) != -1;
+  }
+
+  public void constantCompareToFail2() {
+    String s1 = "ab";
+    String s2 = "abc";
+    assert s2.compareTo(s1) != 1;
+  }
+
+  public void constantCompareToFail3() {
+    String s1 = "abc";
+    String s2 = "abc";
+    assert s1.compareTo(s2) != 0;
+  }
+
+  public void constantCompareToFail4() {
+    String s1 = "abyz";
+    String s2 = "adyz";
+    assert s1.compareTo(s2) != -2;
+  }
+}
diff --git a/...ngs/CompareToConstantEvaluation/test.desc → ...ngs/ConstantEvaluationCompareTo/test.desc b/...ngs/CompareToConstantEvaluation/test.desc → ...ngs/ConstantEvaluationCompareTo/test.desc
diff --git a/...mpareToConstantEvaluation/test_fail1.desc → ...nstantEvaluationCompareTo/test_fail1.desc b/...mpareToConstantEvaluation/test_fail1.desc → ...nstantEvaluationCompareTo/test_fail1.desc
diff --git a/...eToConstantEvaluation/test_fail1_vcc.desc → ...ntEvaluationCompareTo/test_fail1_vcc.desc b/...eToConstantEvaluation/test_fail1_vcc.desc → ...ntEvaluationCompareTo/test_fail1_vcc.desc
diff --git a/...mpareToConstantEvaluation/test_fail2.desc → ...nstantEvaluationCompareTo/test_fail2.desc b/...mpareToConstantEvaluation/test_fail2.desc → ...nstantEvaluationCompareTo/test_fail2.desc
diff --git a/...eToConstantEvaluation/test_fail2_vcc.desc → ...ntEvaluationCompareTo/test_fail2_vcc.desc b/...eToConstantEvaluation/test_fail2_vcc.desc → ...ntEvaluationCompareTo/test_fail2_vcc.desc
diff --git a/...mpareToConstantEvaluation/test_fail3.desc → ...nstantEvaluationCompareTo/test_fail3.desc b/...mpareToConstantEvaluation/test_fail3.desc → ...nstantEvaluationCompareTo/test_fail3.desc
diff --git a/...eToConstantEvaluation/test_fail3_vcc.desc → ...ntEvaluationCompareTo/test_fail3_vcc.desc b/...eToConstantEvaluation/test_fail3_vcc.desc → ...ntEvaluationCompareTo/test_fail3_vcc.desc
diff --git a/...mpareToConstantEvaluation/test_fail4.desc → ...nstantEvaluationCompareTo/test_fail4.desc b/...mpareToConstantEvaluation/test_fail4.desc → ...nstantEvaluationCompareTo/test_fail4.desc
diff --git a/...eToConstantEvaluation/test_fail4_vcc.desc → ...ntEvaluationCompareTo/test_fail4_vcc.desc b/...eToConstantEvaluation/test_fail4_vcc.desc → ...ntEvaluationCompareTo/test_fail4_vcc.desc
diff --git a/...ngs/EndsWithConstantEvaluation/Main.class → ...ngs/ConstantEvaluationEndsWith/Main.class b/...ngs/EndsWithConstantEvaluation/Main.class → ...ngs/ConstantEvaluationEndsWith/Main.class
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/Main.java
@@ -0,0 +1,13 @@
+public class Main {
+  public void constantEndsWithPass() {
+    String s1 = "abc";
+    String s2 = "bc";
+    assert s1.endsWith(s2);
+  }
+
+  public void constantEndsWithFail() {
+    String s1 = "abc";
+    String s2 = "d";
+    assert s1.endsWith(s2);
+  }
+}
diff --git a/...EndsWithConstantEvaluation/test_fail.desc → ...ConstantEvaluationEndsWith/test_fail.desc b/...EndsWithConstantEvaluation/test_fail.desc → ...ConstantEvaluationEndsWith/test_fail.desc
diff --git a/...WithConstantEvaluation/test_fail_vcc.desc → ...tantEvaluationEndsWith/test_fail_vcc.desc b/...WithConstantEvaluation/test_fail_vcc.desc → ...tantEvaluationEndsWith/test_fail_vcc.desc
diff --git a/...EndsWithConstantEvaluation/test_pass.desc → ...ConstantEvaluationEndsWith/test_pass.desc b/...EndsWithConstantEvaluation/test_pass.desc → ...ConstantEvaluationEndsWith/test_pass.desc
diff --git a/...ings/IsEmptyConstantEvaluation/Main.class → ...ings/ConstantEvaluationIsEmpty/Main.class b/...ings/IsEmptyConstantEvaluation/Main.class → ...ings/ConstantEvaluationIsEmpty/Main.class
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/Main.java
@@ -0,0 +1,11 @@
+public class Main {
+  public void constantIsEmptyPass() {
+    String s = "";
+    assert s.isEmpty();
+  }
+
+  public void constantIsEmptyFail() {
+    String s = "abc";
+    assert s.isEmpty();
+  }
+}
diff --git a/.../IsEmptyConstantEvaluation/test_fail.desc → .../ConstantEvaluationIsEmpty/test_fail.desc b/.../IsEmptyConstantEvaluation/test_fail.desc → .../ConstantEvaluationIsEmpty/test_fail.desc
diff --git a/...mptyConstantEvaluation/test_fail_vcc.desc → ...stantEvaluationIsEmpty/test_fail_vcc.desc b/...mptyConstantEvaluation/test_fail_vcc.desc → ...stantEvaluationIsEmpty/test_fail_vcc.desc
diff --git a/.../IsEmptyConstantEvaluation/test_pass.desc → .../ConstantEvaluationIsEmpty/test_pass.desc b/.../IsEmptyConstantEvaluation/test_pass.desc → .../ConstantEvaluationIsEmpty/test_pass.desc
diff --git a/...ilderAppendConstantEvaluation1/Main.class → ...valuationStringBuilderAppend01/Main.class b/...ilderAppendConstantEvaluation1/Main.class → ...valuationStringBuilderAppend01/Main.class
diff --git a/...uilderAppendConstantEvaluation1/Main.java → ...EvaluationStringBuilderAppend01/Main.java b/...uilderAppendConstantEvaluation1/Main.java → ...EvaluationStringBuilderAppend01/Main.java
diff --git a/...uilderAppendConstantEvaluation1/test.desc → ...EvaluationStringBuilderAppend01/test.desc b/...uilderAppendConstantEvaluation1/test.desc → ...EvaluationStringBuilderAppend01/test.desc
diff --git a/...ilderAppendConstantEvaluation2/Main.class → ...uilderAppend02-WithEmptyString/Main.class b/...ilderAppendConstantEvaluation2/Main.class → ...uilderAppend02-WithEmptyString/Main.class
diff --git a/...uilderAppendConstantEvaluation2/Main.java → ...BuilderAppend02-WithEmptyString/Main.java b/...uilderAppendConstantEvaluation2/Main.java → ...BuilderAppend02-WithEmptyString/Main.java
diff --git a/...ilderAppendConstantEvaluation2/test1.desc → ...uilderAppend02-WithEmptyString/test1.desc b/...ilderAppendConstantEvaluation2/test1.desc → ...uilderAppend02-WithEmptyString/test1.desc
diff --git a/...ilderAppendConstantEvaluation2/test2.desc → ...uilderAppend02-WithEmptyString/test2.desc b/...ilderAppendConstantEvaluation2/test2.desc → ...uilderAppend02-WithEmptyString/test2.desc
diff --git a/...ilderAppendConstantEvaluation2/test3.desc → ...uilderAppend02-WithEmptyString/test3.desc b/...ilderAppendConstantEvaluation2/test3.desc → ...uilderAppend02-WithEmptyString/test3.desc
diff --git a/...tConstructorConstantEvaluation/Main.class → ...tringBuilderDefaultConstructor/Main.class b/...tConstructorConstantEvaluation/Main.class → ...tringBuilderDefaultConstructor/Main.class
diff --git a/...ltConstructorConstantEvaluation/Main.java → ...StringBuilderDefaultConstructor/Main.java b/...ltConstructorConstantEvaluation/Main.java → ...StringBuilderDefaultConstructor/Main.java
diff --git a/...ltConstructorConstantEvaluation/test.desc → ...StringBuilderDefaultConstructor/test.desc b/...ltConstructorConstantEvaluation/test.desc → ...StringBuilderDefaultConstructor/test.desc
diff --git a/...ncatenationConstantEvaluation1/Main.class → ...valuationStringConcatenation01/Main.class b/...ncatenationConstantEvaluation1/Main.class → ...valuationStringConcatenation01/Main.class
diff --git a/...oncatenationConstantEvaluation1/Main.java → ...EvaluationStringConcatenation01/Main.java b/...oncatenationConstantEvaluation1/Main.java → ...EvaluationStringConcatenation01/Main.java
diff --git a/...oncatenationConstantEvaluation1/test.desc → ...EvaluationStringConcatenation01/test.desc b/...oncatenationConstantEvaluation1/test.desc → ...EvaluationStringConcatenation01/test.desc
diff --git a/...ncatenationConstantEvaluation2/Main.class → ...oncatenation02-WithEmptyString/Main.class b/...ncatenationConstantEvaluation2/Main.class → ...oncatenation02-WithEmptyString/Main.class
diff --git a/...oncatenationConstantEvaluation2/Main.java → ...Concatenation02-WithEmptyString/Main.java b/...oncatenationConstantEvaluation2/Main.java → ...Concatenation02-WithEmptyString/Main.java
diff --git a/...ncatenationConstantEvaluation2/test1.desc → ...oncatenation02-WithEmptyString/test1.desc b/...ncatenationConstantEvaluation2/test1.desc → ...oncatenation02-WithEmptyString/test1.desc
diff --git a/...ncatenationConstantEvaluation2/test2.desc → ...oncatenation02-WithEmptyString/test2.desc b/...ncatenationConstantEvaluation2/test2.desc → ...oncatenation02-WithEmptyString/test2.desc
diff --git a/...ncatenationConstantEvaluation2/test3.desc → ...oncatenation02-WithEmptyString/test3.desc b/...ncatenationConstantEvaluation2/test3.desc → ...oncatenation02-WithEmptyString/test3.desc
diff --git a/...ncatenationConstantEvaluation3/Main.class → ...catenation03-NegativeScenarios/Main.class b/...ncatenationConstantEvaluation3/Main.class → ...catenation03-NegativeScenarios/Main.class
diff --git a/...oncatenationConstantEvaluation3/Main.java → ...ncatenation03-NegativeScenarios/Main.java b/...oncatenationConstantEvaluation3/Main.java → ...ncatenation03-NegativeScenarios/Main.java
diff --git a/...ncatenationConstantEvaluation3/test1.desc → ...catenation03-NegativeScenarios/test1.desc b/...ncatenationConstantEvaluation3/test1.desc → ...catenation03-NegativeScenarios/test1.desc
diff --git a/...ncatenationConstantEvaluation3/test2.desc → ...catenation03-NegativeScenarios/test2.desc b/...ncatenationConstantEvaluation3/test2.desc → ...catenation03-NegativeScenarios/test2.desc
diff --git a/...ncatenationConstantEvaluation3/test3.desc → ...catenation03-NegativeScenarios/test3.desc b/...ncatenationConstantEvaluation3/test3.desc → ...catenation03-NegativeScenarios/test3.desc
diff --git a/jbmc/regression/jbmc-strings/EndsWithConstantEvaluation/Main.java b/jbmc/regression/jbmc-strings/EndsWithConstantEvaluation/Main.java
diff --git a/jbmc/regression/jbmc-strings/IsEmptyConstantEvaluation/Main.java b/jbmc/regression/jbmc-strings/IsEmptyConstantEvaluation/Main.java