Merge pull request diffblue#530 from lucasccordeiro/string-regression

added test cases to check the string-solver

Author: Daniel Kroening

regression/strings/RegexMatches01/RegexMatches01.class

@@ -0,0 +1,25 @@
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+public class RegexMatches01
+{
+   public static void main(String[] args)
+   {
+      Pattern expression =
+         Pattern.compile("W.*\\d[0-35-9]-\\d\\d-\\d\\d");
+
+      String string1 = "XXXX's Birthday is 05-12-75\n" +
+         "YYYY's Birthday is 11-04-68\n" +
+         "ZZZZ's Birthday is 04-28-73\n" +
+         "WWWW's Birthday is 12-17-77";
+
+      Matcher matcher = expression.matcher(string1);
+
+      while (matcher.find())
+      {
+         System.out.println(matcher.group());
+         String tmp=matcher.group();
+         assert tmp.equals("WWWW's Birthday is 12-17-77");
+      }
+   }
+}

regression/strings/RegexMatches01/RegexMatches01.java

@@ -0,0 +1,8 @@
+FUTURE
+RegexMatches01.class
+--string-refine --unwind 100
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/strings/RegexMatches01/test.desc

@@ -0,0 +1,25 @@
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+public class RegexMatches02
+{
+   public static void main(String[] args)
+   {
+      Pattern expression =
+         Pattern.compile("W.*\\d[0-35-9]-\\d\\d-\\d\\d");
+
+      String string1 = "XXXX's Birthday is 05-12-75\n" +
+         "YYYY's Birthday is 11-04-68\n" +
+         "ZZZZ's Birthday is 04-28-73\n" +
+         "WWWW's Birthday is 12-17-77";
+
+      Matcher matcher = expression.matcher(string1);
+
+      while (matcher.find())
+      {
+         System.out.println(matcher.group());
+         String tmp=matcher.group();
+         assert tmp.equals("WWWWW's Birthday is 12-17-77");
+      }
+   }
+}

regression/strings/RegexMatches02/RegexMatches02.class

@@ -0,0 +1,8 @@
+FUTURE
+RegexMatches02.class
+--string-refine --unwind 100
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/strings/RegexMatches02/RegexMatches02.java

@@ -0,0 +1,39 @@
+import java.util.Arrays;
+
+public class RegexSubstitution01
+{
+   public static void main(String[] args)
+   {
+      String firstString = "DiffBlue ***";
+      String secondString = "Automatic Test Case Generation";
+
+      firstString = firstString.replaceAll("\\*", "^");
+
+      assert firstString.equals("DiffBlue ^^^");
+
+      secondString = secondString.replaceAll("Automatic", "Automated");
+
+      System.out.printf(
+         "\"Automatic\" substituted for \"Automated\": %s\n", secondString);
+      secondString.equals("Automated Test Case Generation");
+
+      System.out.printf("Every word replaced by \"word\": %s\n\n",
+         firstString.replaceAll("\\w+", "word"));
+
+      System.out.printf("Original String 2: %s\n", secondString);
+      secondString.equals("Automated Test Case Generation");
+
+      for (int i = 0; i < 3; i++)
+         secondString = secondString.replaceFirst("\\A", "automated");
+
+      assert secondString.equals("automatedautomatedautomatedAutomated Test Case Generation");
+
+      System.out.print("String split at commas: ");
+      String[] results = secondString.split(" \\s*");
+      System.out.println(Arrays.toString(results));
+      assert results[0].equals("automatedautomatedautomatedAutomated");
+      assert results[1].equals("Test");
+      assert results[2].equals("Case");
+      assert results[3].equals("Generation");
+   }
+}

regression/strings/RegexMatches02/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+RegexSubstitution01.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/strings/RegexSubstitution01/RegexSubstitution01.class

@@ -0,0 +1,32 @@
+import java.util.Arrays;
+
+public class RegexSubstitution02
+{
+   public static void main(String[] args)
+   {
+      String firstString = "DiffBlue ***";
+      String secondString = "Automatic Test Case Generation";
+
+      firstString = firstString.replaceAll("\\*", "^");
+
+      secondString = secondString.replaceAll("Automatic", "Automated");
+
+      System.out.printf(
+         "\"Automatic\" substituted for \"Automated\": %s\n", secondString);
+      secondString.equals("Automated Test Case Generation");
+
+      System.out.printf("Every word replaced by \"word\": %s\n\n",
+         firstString.replaceAll("\\w+", "word"));
+
+      System.out.printf("Original String 2: %s\n", secondString);
+      secondString.equals("Automated Test Case Generation");
+
+      for (int i = 0; i < 3; i++)
+         secondString = secondString.replaceFirst("\\A", "automated");
+
+      System.out.print("String split at commas: ");
+      String[] results = secondString.split(" \\s*");
+      System.out.println(Arrays.toString(results));
+      assert results[0].equals("automatedautomatedautomatedaAutomated");
+   }
+}

regression/strings/RegexSubstitution01/RegexSubstitution01.java

@@ -0,0 +1,8 @@
+FUTURE
+RegexSubstitution02.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/strings/RegexSubstitution01/test.desc

@@ -0,0 +1,33 @@
+import java.util.Arrays;
+
+public class RegexSubstitution03
+{
+   public static void main(String[] args)
+   {
+      String firstString = "DiffBlue ***";
+      String secondString = "Automatic Test Case Generation";
+
+      firstString = firstString.replaceAll("\\*", "^");
+
+      assert firstString.equals("DiffBlue ^^^");
+
+      secondString = secondString.replaceAll("Automatic", "Automated");
+
+      System.out.printf(
+         "\"Automatic\" substituted for \"Automated\": %s\n", secondString);
+      secondString.equals("Automated Test Case Generation");
+
+      System.out.printf("Every word replaced by \"word\": %s\n\n",
+         firstString.replaceAll("\\w+", "word"));
+
+      System.out.printf("Original String 2: %s\n", secondString);
+      secondString.equals("Automated Test Case Generation");
+
+      for (int i = 0; i < 3; i++)
+         secondString = secondString.replaceFirst("\\A", "automated");
+
+      System.out.print("String split at commas: ");
+      String[] results = secondString.split(" \\s*");
+      System.out.println(Arrays.toString(results));
+   }
+}

regression/strings/RegexSubstitution02/RegexSubstitution02.class

@@ -0,0 +1,8 @@
+FUTURE
+RegexSubstitution03.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/strings/RegexSubstitution02/RegexSubstitution02.java

@@ -0,0 +1,16 @@
+public class StaticCharMethods01
+{
+   public static void main(String[] args)
+   {
+      char c = 0;
+      assert Character.isDefined(c)==true;
+      assert Character.isDigit(c)==false;
+      assert Character.isJavaIdentifierStart(c)==false;
+      assert Character.isJavaIdentifierPart(c)==true;
+      assert Character.isLetter(c)==false;
+      assert Character.isLetterOrDigit(c)==false;
+      assert Character.isLowerCase(c)==false;
+      assert Character.isUpperCase(c)==false;
+      assert Character.toUpperCase(c)==Character.toLowerCase(c);
+   }
+}

regression/strings/RegexSubstitution02/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+StaticCharMethods01.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/strings/RegexSubstitution03/RegexSubstitution03.class

@@ -0,0 +1,8 @@
+public class StaticCharMethods02
+{
+   public static void main(String[] args)
+   {
+      char c = 0;
+      assert Character.toUpperCase(c)!=Character.toLowerCase(c);
+   }
+}

regression/strings/RegexSubstitution03/RegexSubstitution03.java

@@ -0,0 +1,8 @@
+FUTURE
+StaticCharMethods02.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/strings/RegexSubstitution03/test.desc

@@ -0,0 +1,8 @@
+public class StaticCharMethods03
+{
+   public static void main(String[] args)
+   {
+      char c = 0;
+      assert Character.isDefined(c)==false;
+   }
+}

regression/strings/StaticCharMethods01/StaticCharMethods01.class

@@ -0,0 +1,8 @@
+FUTURE
+StaticCharMethods03.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/strings/StaticCharMethods01/StaticCharMethods01.java

@@ -0,0 +1,8 @@
+public class StaticCharMethods04
+{
+   public static void main(String[] args)
+   {
+      char c = 0;
+      assert Character.isLetter(c)==true;
+   }
+}

regression/strings/StaticCharMethods01/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+StaticCharMethods04.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/strings/StaticCharMethods02/StaticCharMethods02.class

@@ -0,0 +1,33 @@
+import java.util.Scanner;
+
+public class StaticCharMethods05
+{
+   public static void main(String[] args)
+   {
+      Scanner scanner = new Scanner(System.in);
+
+      int radix = scanner.nextInt();
+
+      int choice = scanner.nextInt() % 3;
+      assert choice>=0 && choice<3;
+
+      switch (choice)
+      {
+         case 1: // convert digit to character
+            System.out.println("Enter a digit:");
+            int digit = scanner.nextInt();
+            System.out.printf("Convert digit to character: %s\n",
+               Character.forDigit(digit, radix));
+	    char tmp=Character.forDigit(digit, radix);
+            assert tmp=='t';
+            break;
+
+         case 2: // convert character to digit
+            System.out.println("Enter a character:");
+            char character = scanner.next().charAt(0);
+            System.out.printf("Convert character to digit: %s\n",
+               Character.digit(character, radix));
+            break;
+      }
+   }
+}

regression/strings/StaticCharMethods02/StaticCharMethods02.java

@@ -0,0 +1,8 @@
+FUTURE
+StaticCharMethods05.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/strings/StaticCharMethods02/test.desc

@@ -0,0 +1,19 @@
+public class StaticCharMethods06
+{
+   public static void main(String[] args)
+   {
+      Character c1 = 'A';
+      Character c2 = 'A';
+
+      if (c1.equals(c2))
+      {
+         System.out.println("c1 and c2 are equal\n");
+         assert true;
+      }
+      else
+      {
+         System.out.println("c1 and c2 are not equal\n");
+         assert false;
+      }
+   }
+}

regression/strings/StaticCharMethods03/StaticCharMethods03.class

@@ -0,0 +1,8 @@
+FUTURE
+StaticCharMethods06.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/strings/StaticCharMethods03/StaticCharMethods03.java

@@ -0,0 +1,43 @@
+public class StringBuilderAppend01
+{
+   public static void main(String[] args)
+   {
+      Object objectRef = "diffblue";
+      String string = "test";
+      char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'};
+      boolean booleanValue = true;
+      char characterValue = 'Z';
+      int integerValue = 7;
+      long longValue = 10000000000L;
+      float floatValue = 2.5f;
+      double doubleValue = 33.333;
+
+      StringBuilder lastBuffer = new StringBuilder("last buffer");
+      StringBuilder buffer = new StringBuilder();
+
+      buffer.append(objectRef)
+            .append("%n")
+            .append(string)
+            .append("%n")
+            .append(charArray)
+            .append("%n")
+            .append(charArray, 0, 3)
+            .append("%n")
+            .append(booleanValue)
+            .append("%n")
+            .append(characterValue)
+            .append("%n")
+            .append(integerValue)
+            .append("%n")
+            .append(longValue)
+            .append("%n")
+            .append(floatValue)
+            .append("%n")
+            .append(doubleValue)
+            .append("%n")
+            .append(lastBuffer);
+
+      String tmp=buffer.toString();
+      assert tmp.equals("diffblue%ntest%nverification%nver%ntrue%nZ%n7%n10000000000%n2.5%n33.333%nlast buffer");
+   }
+}