Merge pull request #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