Test-gen support

.travis.yml

@@ -47,4 +47,4 @@ script:
     make -C src minisat2-download &&
     make -C src CXX=$COMPILER CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 &&
     env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test &&
-    make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 aa-symex.dir cegis.dir clobber.dir memory-models.dir musketeer.dir
+    make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir

regression/cbmc-java/assume1/Assume1.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume1
+{
+  static void foo(int x)
+  {
+    CProver.assume(x>3);
+    assert x>0;
+  }
+}

regression/cbmc-java/assume1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume1.class
+--function Assume1.foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/assume2/Assume2.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume2
+{
+  static void foo(int x)
+  {
+    CProver.assume(x>3);    
+    assert x>4;
+  }
+}

regression/cbmc-java/assume2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume2.class
+--function Assume2.foo
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/assume3/Assume3.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume3
+{
+  public static void main(String[] args)
+  {
+    CProver.assume(false);
+    assert false;
+  }
+}

regression/cbmc-java/assume3/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume3.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/covered1/covered1.java

@@ -0,0 +1,37 @@
+public class covered1
+{
+  // this is a variable
+  int x=1;
+  //these are two, one line off the first
+  int y=2;
+  int z=3;
+  //this is part of static init
+  static int z0=0;
+
+  //another non-static
+  int a;
+  int b;
+  static boolean odd;
+
+  static
+  {
+    odd=(z0+1)%2==0;
+  }
+
+  covered1(int a, int b)
+  {
+    this.a=a*b;
+    this.b=a+b;
+    if(this.a==a)
+      z0++;
+    else
+      odd=!odd;
+  }
+  // at the back
+  int z1=2;
+  int z2=3;
+  int z3=4;
+  //
+  static int z4=5;
+  int z5=5;
+}

regression/cbmc-java/covered1/test.desc

@@ -0,0 +1,19 @@
+CORE
+covered1.class
+--cover location --json-ui --show-properties
+^EXIT=0$
+^SIGNAL=0$
+.*\"coveredLines\": \"22\",$
+.*\"coveredLines\": \"4,6,7,23-25,31-33,36\",$
+.*\"coveredLines\": \"26\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"29\",$
+.*\"coveredLines\": \"9,18\",$
+.*\"coveredLines\": \"18\",$
+.*\"coveredLines\": \"18\",$
+.*\"coveredLines\": \"18,35\",$
+--
+^warning: ignoring

regression/cbmc-java/lazyloading1/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading1/test.java

@@ -0,0 +1,21 @@
+// The most basic lazy loading test: A::f is directly called, B::g should be unreachable
+
+public class test
+{
+  A a;
+  B b;
+  public static void main()
+  {
+    A.f();
+  }
+}
+
+class A
+{
+  public static void f() {}
+}
+
+class B
+{
+  public static void g() {}
+}

regression/cbmc-java/lazyloading2/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading2/test.java

@@ -0,0 +1,23 @@
+// This test checks that because A is instantiated in main and B is not,
+// A::f is reachable and B::g is not
+
+public class test
+{
+  A a;
+  B b;
+  public static void main()
+  {
+    A a = new A();
+    a.f();
+  }
+}
+
+class A
+{
+  public void f() {}
+}
+
+class B
+{
+  public void g() {}
+}

regression/cbmc-java/lazyloading3/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading3/test.java

@@ -0,0 +1,30 @@
+// This test checks that because `main` has a parameter of type C, which has a field of type A,
+// A::f is considered reachable, but B::g is not.
+
+public class test
+{
+  public static void main(C c)
+  {
+    c.a.f();
+  }
+}
+
+class A
+{
+  public void f() {}
+}
+
+class B
+{
+  public void g() {}
+}
+
+class C
+{
+  A a;
+}
+
+class D
+{
+  B b;
+}

regression/failed-tests-printer.pl

@@ -4,23 +4,25 @@
 
 open LOG,"<tests.log" or die "Failed to open tests.log\n";
 
-my $ignore = 1;
+my $printed_this_test = 1;
 my $current_test = "";
 
 while (<LOG>) {
   chomp;
   if (/^Test '(.+)'/) {
     $current_test = $1;
-    $ignore = 0;
-  } elsif (1 == $ignore) {
-    next;
+    $printed_this_test = 0;
   } elsif (/\[FAILED\]\s*$/) {
-    $ignore = 1;
-    print "Failed test: $current_test\n";
-    my $outf = `sed -n '2p' $current_test/test.desc`;
-    $outf =~ s/\..*$/.out/;
-    system("cat $current_test/$outf");
-    print "\n\n";
+    if(0 == $printed_this_test) {
+      $printed_this_test = 1;
+      print "\n\n";
+      print "Failed test: $current_test\n";
+      my $outf = `sed -n '2p' $current_test/test.desc`;
+      $outf =~ s/\..*$/.out/;
+      system("cat $current_test/$outf");
+      print "\n\nFailed test.desc lines:\n";
+    }
+    print "$_\n";
   }
 }
 

regression/strings/RegexMatches01/RegexMatches01.java

@@ -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/test.desc

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

regression/strings/RegexMatches02/RegexMatches02.java

@@ -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/test.desc

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

regression/strings/RegexSubstitution01/RegexSubstitution01.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/RegexSubstitution01/test.desc

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