JBMC tests should not use --cover

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java

@@ -18,7 +18,9 @@ public String det()
         builder.setCharAt(11, ':');
         builder.setCharAt(16, ':');
         builder.setCharAt(18, ':');
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String nonDet(String s, char c, int i)
@@ -42,7 +44,9 @@ public String nonDet(String s, char c, int i)
         builder.setCharAt(11, ':');
         builder.setCharAt(16, ':');
         builder.setCharAt(18, ':');
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String withDependency(boolean b)

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc

@@ -3,8 +3,8 @@ Test.class
 --function Test.withDependency --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 55 .*: SUCCESS
-assertion at file Test.java line 57 .*: FAILURE
+assertion at file Test.java line 59 .*: SUCCESS
+assertion at file Test.java line 61 .*: FAILURE
 --
 --
 Check that when a dependency is present, the correct constraints are added

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc

@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.det  --verbosity 10 --cover location
-^EXIT=0$
+--function Test.det --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 21 .*: SATISFIED
+assertion at file Test.java line 22 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc

@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
-^EXIT=0$
+--function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 45 .*: SATISFIED
+assertion at file Test.java line 48 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --

jbmc/regression/jbmc-strings/StringToLowerCase/Test.java

@@ -7,7 +7,9 @@ public String det()
         builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toLowerCase());
         builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toLowerCase());
         builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toLowerCase());
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String nonDet(String s)
@@ -25,7 +27,9 @@ public String nonDet(String s)
         builder.append(":");
         builder.append(s.toLowerCase());
         builder.append(s.toLowerCase());
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String withDependency(String s, boolean b)

jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc

@@ -3,8 +3,8 @@ Test.class
 --function Test.withDependency  --verbosity 10 --max-nondet-string-length 10000
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 44 .*: SUCCESS
-assertion at file Test.java line 46 .*: FAILURE
+assertion at file Test.java line 48 .*: SUCCESS
+assertion at file Test.java line 50 .*: FAILURE
 --
 --
 Check that when there are dependencies, axioms are adde correctly.

jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc

@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.det  --verbosity 10 --cover location
-^EXIT=0$
+--function Test.det  --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 9 .*: SATISFIED
+assertion at file Test.java line 11 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --

jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc

@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.nonDet  --verbosity 10 --cover location --max-nondet-string-length 1000
-^EXIT=0$
+--function Test.nonDet  --verbosity 10 --max-nondet-string-length 1000
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 27 .*: SATISFIED
+assertion at file Test.java line 31 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --

jbmc/regression/jbmc-strings/StringToUpperCase/Test.java

@@ -7,7 +7,9 @@ public String det()
         builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toUpperCase());
         builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toUpperCase());
         builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toUpperCase());
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String nonDet(String s)
@@ -25,7 +27,9 @@ public String nonDet(String s)
         builder.append(":");
         builder.append(s.toUpperCase());
         builder.append(s.toUpperCase());
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String withDependency(String s, boolean b)

jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc

@@ -3,8 +3,8 @@ Test.class
 --function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 44 .*: SUCCESS
-assertion at file Test.java line 46 .*: FAILURE
+assertion at file Test.java line 48 .*: SUCCESS
+assertion at file Test.java line 50 .*: FAILURE
 --
 --
 Check that when there are dependencies, axioms are added correctly.

jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc

@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.det  --verbosity 10 --cover location
-^EXIT=0$
+--function Test.det  --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 9 .*: SATISFIED
+assertion at file Test.java line 11 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --

jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc

@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.nonDet  --verbosity 10 --cover location --max-nondet-string-length 1000
-^EXIT=0$
+--function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 27 .*: SATISFIED
+assertion at file Test.java line 31 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --

jbmc/regression/jbmc-strings/StringValueOfInt/Test.java

@@ -23,6 +23,7 @@ public static String checkDet()
         tmp = String.valueOf(-1000003);
         tmp = String.valueOf(1000004);
         tmp = String.valueOf(1000005);
+        assert tmp.length() < 5;
         return tmp;
     }
 
@@ -51,6 +52,7 @@ public static String checkNonDet(int i)
         tmp += String.valueOf(-i + 1);
         tmp += " ";
         tmp += String.valueOf(-i - 2);
+        assert tmp.length() < 5;
         return tmp;
     }
 

jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc

@@ -3,8 +3,8 @@ Test.class
 --function Test.checkWithDependency --depth 10000
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 61 .*: SUCCESS
-assertion at file Test.java line 64 .*: FAILURE
+assertion at file Test.java line 63 .*: SUCCESS
+assertion at file Test.java line 66 .*: FAILURE
 --
 --
 Check that when a dependency is present, the correct constraints are added

jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc

@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.checkDet --verbosity 10 --cover location
-^EXIT=0$
+--function Test.checkDet --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 25 .*: SATISFIED
+assertion at file Test.java line 26 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --

jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc

@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.checkNonDet --verbosity 10 --cover location
-^EXIT=0$
+--function Test.checkNonDet --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 53 .*: SATISFIED
+assertion at file Test.java line 55 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --

jbmc/regression/jbmc-strings/char_escape/Test.java

@@ -10,10 +10,15 @@ public static boolean test(char c1, char c2, char c3, char c4, char c5, char c6,
         sb.append(c6);
         sb.append(c7);
         sb.append(c8);
-        if (sb.toString().equals("\b\t\n\f\r\"\'\\"))
+        if (sb.toString().equals("\b\t\n\f\r\"\'\\")) {
+            assert false;
             return true;
-        if (!sb.toString().equals("\b\t\n\f\r\"\'\\"))
+        }
+        if (!sb.toString().equals("\b\t\n\f\r\"\'\\")) {
+            assert false;
             return false;
+        }
+        assert false;
         return true;
     }
 }

jbmc/regression/jbmc-strings/char_escape/test.desc

@@ -1,6 +1,9 @@
 CORE
 Test.class
---function Test.test --cover location --trace --json-ui
-^EXIT=0$
+--function Test.test --trace --json-ui
+^EXIT=10$
 ^SIGNAL=0$
-20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\)
+"reason": "assertion at file Test.java line 14
+"reason": "assertion at file Test.java line 18
+--
+"reason": "assertion at file Test.java line 21

jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java

@@ -4,15 +4,23 @@ public static Boolean testMyGenSet(Integer key) {
         if (key == null) return null;
         MyGenSet<Integer> ms = new MyGenSet<>();
         ms.array[0] = 101;
-        if (ms.contains(key)) return true;
+        if (ms.contains(key)) {
+          assert false;
+          return true;
+        }
+        assert false;
         return false;
     }
 
     public static Boolean testMySet(Integer key) {
         if (key == null) return null;
         MySet ms = new MySet();
         ms.array[0] = 101;
-        if (ms.contains(key)) return true;
+        if (ms.contains(key)) {
+          assert false;
+          return true;
+        }
+        assert false;
         return false;
     }
 

jbmc/regression/jbmc-strings/max-length-generic-array/test.desc

@@ -1,19 +1,7 @@
 CORE
 IntegerTests.class
---max-nondet-string-length 100 --function IntegerTests.testMySet --cover location
-^EXIT=0$
+--max-nondet-string-length 100 --function IntegerTests.testMySet
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED
-coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 3 .* SATISFIED
-coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 4 .* SATISFIED
-coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 6 .* SATISFIED
-coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 7 .* SATISFIED
-coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 12 .* SATISFIED
-coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 13 .* SATISFIED
-coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 16 .* SATISFIED
-coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 17 .* SATISFIED
-coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 21 .* SATISFIED
-coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 19 .* SATISFIED
-coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 20 .* SATISFIED
-coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 22 .* SATISFIED
-coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 23 .* SATISFIED
+assertion at file IntegerTests.java line 20 .*: FAILURE
+assertion at file IntegerTests.java line 23 .*: FAILURE

jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc

@@ -1,20 +1,7 @@
 CORE
 IntegerTests.class
---max-nondet-string-length 100 --function IntegerTests.testMyGenSet --cover location
-^EXIT=0$
+--max-nondet-string-length 100 --function IntegerTests.testMyGenSet
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED
-coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 3 .* SATISFIED
-coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 4 .* SATISFIED
-coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 6 .* SATISFIED
-coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 7 .* SATISFIED
-coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 10 .* SATISFIED
-coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 13 .* SATISFIED
-coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 14 .* SATISFIED
-coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 17 .* SATISFIED
-coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 18 .* SATISFIED
-coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 22 .* SATISFIED
-coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 20 .* SATISFIED
-coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 21 .* SATISFIED
-coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 23 .* SATISFIED
-coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 24 .* SATISFIED
+assertion at file IntegerTests.java line 8 .*: FAILURE
+assertion at file IntegerTests.java line 11 .*: FAILURE

jbmc/regression/jbmc/array2/test.desc

@@ -1,7 +1,6 @@
 CORE
 test.class
---function test.f --cover location
-\d+ of \d+ covered
+--function test.f
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/array2/test.java

@@ -11,6 +11,10 @@ public void f(int unknown) {
     if(unknown > 0)
       arr[0]=1;
 
+    if(unknown > 0)
+      assert arr[0] == 1;
+    else
+      assert arr.length == 0;
   }
 
 }

jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java

@@ -1,17 +1,17 @@
 public class FloatMultidim1 {
   public float[][] f(int y) {
+    float[][] a1 = null;
     if (y > 0 && y < 5) {
-      float[][] a1 = new float[y][2];
+      a1 = new float[y][2];
       int j;
       if (y > 1) {
         j = 1;
       } else {
         j = 0;
       }
       a1[j][1] = 1.0f;
-      return a1;
-    } else {
-      return null;
     }
+    assert a1 == null;
+    return a1;
   }
 }