An example I use for explaining CBMC.

martin · martin · commit e1c428cb6965 · 2017-04-05T17:46:07.000+01:00
diff --git a/main-module/src/main/java/com/diffblue/java_test/Search.java b/main-module/src/main/java/com/diffblue/java_test/Search.java
@@ -0,0 +1,18 @@
+package com.diffblue.java_test;
+
+public class Search
+{
+  public boolean search(int [] array, int target)
+  {
+    boolean found = false;
+    int i;
+    
+    for (i = 0 ; i < array.length; ++i) {
+	if (array[i] == target) {
+	    found = true;
+	}
+    }
+    
+    return found;
+  }
+}
