Merge pull request #5711 from peterschrammel/jbmc-book-examples

Add ASV book JBMC examples

Author: peterschrammel

jbmc/regression/book-examples/BinarySearch/BinarySearch.class

@@ -0,0 +1,12 @@
+public class BinarySearch {
+  public static int binarySearch(int[] array, int value) {
+    int lowerBound = 0;
+    int upperBound = array.length;
+    int i = array.length / 2;
+    while(array[i] != value && upperBound > lowerBound + 1) {
+      if(array[i] > value) upperBound = i; else lowerBound = i;
+      i = (upperBound + lowerBound) / 2;
+    }
+    return i;
+  }
+}

jbmc/regression/book-examples/BinarySearch/BinarySearch.java

@@ -0,0 +1,6 @@
+CORE
+BinarySearch.binarySearch
+ --throw-runtime-exceptions --unwind 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

jbmc/regression/book-examples/BinarySearch/runtime_exception.desc

@@ -0,0 +1,4 @@
+class IdLocator implements Locator {
+  IdLocator(String s) {
+  }
+}

jbmc/regression/book-examples/LocatorHandler/IdLocator.class

@@ -0,0 +1,2 @@
+public interface Locator {
+}