Port of changes to test-gen-support to master (7)

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/strings-smoke-tests/Makefile

@@ -0,0 +1,9 @@
+
+test:
+	@../test.pl -c ../../../src/cbmc/cbmc
+
+testfuture:
+	@../test.pl -c ../../../src/cbmc/cbmc -CF
+
+testall:
+	@../test.pl -c ../../../src/cbmc/cbmc -CFTK

regression/strings-smoke-tests/java_append_char/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_char.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_append_char/test_append_char.java

@@ -0,0 +1,17 @@
+public class test_append_char
+{
+   public static void main(/*String[] args*/)
+   {
+      char[] diff = {'d', 'i', 'f', 'f'};
+      char[] blue = {'b', 'l', 'u', 'e'};
+
+      StringBuilder buffer = new StringBuilder();
+
+      buffer.append(diff)
+            .append(blue);
+
+      String tmp=buffer.toString();
+      System.out.println(tmp);
+      assert tmp.equals("diffblue");
+   }
+}

regression/strings-smoke-tests/java_append_int/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_int.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_append_int/test_append_int.java

@@ -0,0 +1,11 @@
+public class test_append_int
+{
+   public static void main(/*String[] args*/)
+   {
+      StringBuilder diffblue = new StringBuilder();
+      diffblue.append("d");
+      diffblue.append(4);
+      String s = diffblue.toString();
+      assert s.equals("d4");
+   }
+}

regression/strings-smoke-tests/java_append_object/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_object.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_append_object/test_append_object.java

@@ -0,0 +1,17 @@
+public class test_append_object
+{
+   public static void main(/*String[] args*/)
+   {
+      Object diff = "diff";
+      Object blue = "blue";
+
+      StringBuilder buffer = new StringBuilder();
+
+      buffer.append(diff)
+            .append(blue);
+
+      String tmp=buffer.toString();
+      System.out.println(tmp);
+      assert tmp.equals("diffblue");
+   }
+}

regression/strings-smoke-tests/java_append_string/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_string.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_append_string/test_append_string.java

@@ -0,0 +1,14 @@
+public class test_append_string
+{
+   public static void main(/*String[] args*/)
+   {
+      String di = new String("di");
+      StringBuilder diff = new StringBuilder();
+      diff.append(di);
+      diff.append("ff");
+      System.out.println(diff);
+      String s = diff.toString();
+      System.out.println(s);
+      assert s.equals("diff");
+   }
+}

regression/strings-smoke-tests/java_case/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_case.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_case/test_case.java

@@ -0,0 +1,12 @@
+public class test_case
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = new String("Ab");
+      String l = s.toLowerCase();
+      String u = s.toUpperCase();
+      assert(l.equals("ab"));
+      assert(u.equals("AB"));
+      assert(s.equalsIgnoreCase("aB"));
+   }
+}

regression/strings-smoke-tests/java_char_array/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_char_array.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_char_array/test_char_array.java

@@ -0,0 +1,13 @@
+public class test_char_array
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = "abc";
+      char [] str = s.toCharArray();
+      char c = str[2];
+      char a = s.charAt(0);
+      assert(str.length == 3);
+      assert(a == 'a');
+      assert(c == 'c');
+   }
+}

regression/strings-smoke-tests/java_char_array_init/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_init.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_char_array_init/test_init.java

@@ -0,0 +1,21 @@
+public class test_init {
+
+  public static void main(/*String[] argv*/)
+  {
+     char [] str = new char[10];
+     str[0] = 'H';
+     str[1] = 'e';
+     str[2] = 'l';
+     str[3] = 'l';
+     str[4] = 'o';
+     String s = new String(str);
+     String t = new String(str,1,2);
+
+     System.out.println(s.length());
+     assert(s.length() == 10);
+     System.out.println(s);
+     System.out.println(t);
+     assert(t.equals("el"));
+     assert(s.startsWith("Hello"));
+   }
+}

regression/strings-smoke-tests/java_char_at/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_char_at.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_char_at/test_char_at.java

@@ -0,0 +1,7 @@
+public class test_char_at {
+
+  public static void main(/*String[] argv*/) {
+    String s = new String("abc");
+    assert(s.charAt(2)=='c');
+  }
+}

regression/strings-smoke-tests/java_code_point/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_code_point.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_code_point/test_code_point.java

@@ -0,0 +1,14 @@
+public class test_code_point
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = "!𐤇𐤄𐤋𐤋𐤅";
+      assert(s.codePointAt(1) == 67847);
+      assert(s.codePointBefore(3) == 67847);
+      assert(s.codePointCount(1,5) >= 2);
+      assert(s.offsetByCodePoints(1,2) >= 3);
+      StringBuilder sb = new StringBuilder();
+      sb.appendCodePoint(0x10907);
+      assert(s.charAt(1) == sb.charAt(0));
+   }
+}

regression/strings-smoke-tests/java_compare/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_compare.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/strings-smoke-tests/java_compare/test_compare.java

@@ -0,0 +1,9 @@
+public class test_compare
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s1 = "ab";
+      String s2 = "aa";
+      assert(s1.compareTo(s2) == 1);
+   }
+}

regression/strings-smoke-tests/java_concat/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+test_concat.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 10.* SUCCESS$
+^\[.*assertion.2\].* line 11.* FAILURE$
+--

regression/strings-smoke-tests/java_concat/test_concat.java

@@ -0,0 +1,13 @@
+public class test_concat
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = new String("pi");
+      int i = s.length();
+      String t = new String("ppo");
+      String u = s.concat(t);
+      char c = u.charAt(i);
+      assert(c == 'p');
+      assert(c == 'o');
+   }
+}

regression/strings-smoke-tests/java_contains/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+test_contains.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+--

regression/strings-smoke-tests/java_contains/test_contains.java

@@ -0,0 +1,11 @@
+public class test_contains
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = new String("Abc");
+      String u = "bc";
+      String t = "ab";
+      assert(s.contains(u));
+      assert(s.contains(t));
+   }
+}