Add performance tests with negated asserts

Add a series of performance tests that check that the negation of the
assertions found in the smoke tests indeed fail.

Author: Joel Allred

regression/strings/performance_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/performance_tests/java_append_char/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_char.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 15.* FAILURE$
+--

regression/strings/performance_tests/java_append_char/test_append_char.class

@@ -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/performance_tests/java_append_char/test_append_char.java

@@ -0,0 +1,7 @@
+FUTURE
+test_append_int.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 9.* FAILURE$
+--

regression/strings/performance_tests/java_append_int/test.desc

@@ -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/performance_tests/java_append_int/test_append_int.class

@@ -0,0 +1,7 @@
+FUTURE
+test_append_object.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 15.* FAILURE$
+--

regression/strings/performance_tests/java_append_int/test_append_int.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/performance_tests/java_append_object/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_append_string.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 12.* FAILURE$
+--

regression/strings/performance_tests/java_append_object/test_append_object.class

@@ -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/performance_tests/java_append_object/test_append_object.java

@@ -0,0 +1,7 @@
+FUTURE
+test_case.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* FAILURE$
+--

regression/strings/performance_tests/java_append_string/test.desc

@@ -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") ||
+             !u.equals("AB") ||
+             !s.equalsIgnoreCase("aB"));
+   }
+}

regression/strings/performance_tests/java_append_string/test_append_string.class

@@ -0,0 +1,7 @@
+FUTURE
+test_char_array.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 9.* FAILURE$
+--

regression/strings/performance_tests/java_append_string/test_append_string.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 ||
+             a != 'a' ||
+             c != 'c');
+   }
+}

regression/strings/performance_tests/java_case/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_init.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 14.* FAILURE$
+--

regression/strings/performance_tests/java_case/test_case.class

@@ -0,0 +1,18 @@
+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);
+
+     assert(s.length() != 10 || 
+            !t.equals("el") ||
+            !s.startsWith("Hello"));
+   }
+}

regression/strings/performance_tests/java_case/test_case.java

@@ -0,0 +1,7 @@
+FUTURE
+test_char_at.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 5.* FAILURE$
+--

regression/strings/performance_tests/java_char_array/test.desc

@@ -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/performance_tests/java_char_array/test_char_array.class

@@ -0,0 +1,7 @@
+FUTURE
+test_code_point.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* FAILURE$
+--

regression/strings/performance_tests/java_char_array/test_char_array.java

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

regression/strings/performance_tests/java_char_array_init/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_compare.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 7.* FAILURE$
+--

regression/strings/performance_tests/java_char_array_init/test_init.class

@@ -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/performance_tests/java_char_array_init/test_init.java

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

regression/strings/performance_tests/java_char_at/test.desc

@@ -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 != 'p');
+   }
+}

regression/strings/performance_tests/java_char_at/test_char_at.class

@@ -0,0 +1,7 @@
+FUTURE
+test_contains.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 7.* FAILURE$
+--

regression/strings/performance_tests/java_char_at/test_char_at.java

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

regression/strings/performance_tests/java_code_point/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_delete.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* FAILURE$
+--

regression/strings/performance_tests/java_code_point/test_code_point.class

@@ -0,0 +1,10 @@
+public class test_delete
+{
+   public static void main(/*String[] argv*/)
+   {
+      StringBuilder s = new StringBuilder("Abc");
+      s.delete(1,2);
+      String str = s.toString();
+      assert(!str.equals("Ac"));
+   }
+}

regression/strings/performance_tests/java_code_point/test_code_point.java

@@ -0,0 +1,7 @@
+FUTURE
+test_delete_char_at.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 9.* FAILURE$
+--

regression/strings/performance_tests/java_compare/test.desc

@@ -0,0 +1,11 @@
+public class test_delete_char_at
+{
+   public static void main(/*String[] argv*/)
+   {
+      StringBuilder s = new StringBuilder();
+      s.append("Abc");
+      s.deleteCharAt(1);
+      String str = s.toString();
+      assert(!str.equals("Ac"));
+   }
+}

regression/strings/performance_tests/java_compare/test_compare.class

@@ -0,0 +1,7 @@
+FUTURE
+test_empty.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 6.* FAILURE$
+--

regression/strings/performance_tests/java_compare/test_compare.java

@@ -0,0 +1,8 @@
+public class test_empty
+{
+   public static void main(/*String[] argv*/)
+   {
+      String empty = "";
+      assert(!empty.isEmpty());
+   }
+}

regression/strings/performance_tests/java_concat/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_endswith.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 7.* FAILURE$
+--

regression/strings/performance_tests/java_concat/test_concat.class

@@ -0,0 +1,9 @@
+public class test_endswith
+{
+   public static void main(/*String[] argv*/)
+   {
+      String s = new String("Abcd");
+      String suff = "cd";
+      assert(!s.endsWith(suff));
+   }
+}

regression/strings/performance_tests/java_concat/test_concat.java

@@ -0,0 +1,7 @@
+FUTURE
+test_equal.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* FAILURE$
+--

regression/strings/performance_tests/java_contains/test.desc

@@ -0,0 +1,9 @@
+public class test_equal
+{
+   public static void main(String[] argv)
+   {
+      String s = new String("pi");
+      String t = new String("po");
+      assert(!s.equals(t));
+   }
+}

regression/strings/performance_tests/java_contains/test_contains.class

@@ -0,0 +1,7 @@
+FUTURE
+test_float.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 15.* FAILURE$
+--

regression/strings/performance_tests/java_contains/test_contains.java

@@ -0,0 +1,17 @@
+public class test_float
+{
+   public static void main(/*String[] arg*/)
+   {
+      float inf = 100.0f / 0.0f;
+      float minus_inf = -100.0f / 0.0f;
+      float nan = 0.0f / 0.0f;
+      String inf_string = Float.toString(inf);
+      String mininf_string = Float.toString(minus_inf);
+      String nan_string = Float.toString(nan);
+      System.out.println(nan_string);
+      System.out.println(inf_string);
+      System.out.println(mininf_string);
+      assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity")
+             || !mininf_string.equals("-Infinity"));
+   }
+}

regression/strings/performance_tests/java_delete/test.desc

@@ -0,0 +1,7 @@
+FUTURE
+test_hash_code.class
+--string-refine
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 7.* FAILURE$
+--