Merge pull request #5032 from yumibagge/yb/jbmc-regression-tidy

Rename constant evaluation regression folder names

Author: yumibagge

jbmc/regression/jbmc-strings/CharAtConstantEvaluation/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';
+  }
+}

jbmc/regression/jbmc-strings/CompareToConstantEvaluation/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;
+  }
+}

jbmc/regression/jbmc-strings/CharAtConstantEvaluation/Main.class renamed to jbmc/regression/jbmc-strings/ConstantEvaluationCharAt/Main.class

@@ -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);
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationCharAt/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();
+  }
+}