Re-add division files

src/example-archive/c-testsuite/working/00064.working.c

@@ -0,0 +1,7 @@
+#define X 6 / 2
+
+int
+main()
+{
+	return X - 3;
+}

src/example-archive/dafny-tutorial/working/binary_search.c

@@ -0,0 +1,49 @@
+// Binary search algorithm. The functional correctness of this algorithm depends
+// on the array being sorted
+
+int binary_search(int *a, int length, int value)
+/*@ requires 
+      let MAXi32 = (i64) 2147483647i64; // TODO: lift to library 
+
+      0i32 <= length; 
+      (2i64 * (i64) length) <= MAXi32; 
+      take IndexPre = each (i32 j; 0i32 <= j && j < length)
+                           {Owned<int>(a + j)}; @*/
+/*@ ensures 
+      take IndexPost = each (i32 j; 0i32 <= j && j < length)
+                            {Owned<int>(a + j)}; 
+      IndexPost == IndexPre; 
+      (return < 0i32) || (IndexPost[return] == value); @*/
+{
+  int low = 0;
+  int high = length;
+
+  while (low < high)
+  /*@ inv 
+        {a}unchanged; {length}unchanged; {value}unchanged;  
+        0i32 <= low; 
+        low <= high; 
+        high <= length; 
+        ((i64) low + (i64) high) <= MAXi32; 
+        take IndexInv = each (i32 j; 0i32 <= j && j < length)
+                             {Owned<int>(a + j)}; 
+        IndexInv == IndexPre; @*/
+  {
+    int mid = (low + high) / 2;
+    /*@ extract Owned<int>, mid; @*/
+    /*@ instantiate good<int>, mid;  @*/
+    if (a[mid] < value)
+    {
+      low = mid + 1;
+    }
+    else if (value < a[mid])
+    {
+      high = mid;
+    }
+    else if (value == a[mid])
+    {
+      return mid;
+    }
+  };
+  return -1;
+}

src/example-archive/java_program_verification_challenges/working/00004_exceptions.c

@@ -0,0 +1,71 @@
+// Tags: main, java
+
+/** Source
+Examples translated to C from their original Java source in
+
+Jacobs, Bart, Joseph Kiniry, and Martijn Warnier. "Java program
+verification challenges." Formal Methods for Components and Objects:
+First International Symposium, FMCO 2002, Leiden, The Netherlands,
+November 5-8, 2002, Revised Lectures 1. Springer Berlin Heidelberg,
+2003.
+
+ */
+
+/** Description
+  
+  Typical of Java is its systematic use of exceptions, via its statements for throwing
+and catching. They require a suitable control flow semantics. Special care is
+needed for the ‘finally’ part of a try-catch-finally construction. Figure 4 contains
+a simple example (adapted from [17]) that combines many aspects. The subtle
+point is that the assignment m+=10 in the finally block will still be executed,
+despite the earlier return statements, but has no effect on the value that is
+returned. The reason is that this value is bound earlier.
+
+NOTE: C doesn't handle exceptions. In the translation below, we use an
+if statement to discriminate the input, making the example rather
+trivial.
+
+*/
+
+//#include <stdio.h>
+
+int m; // Global variable m
+
+/* Normal-behavior
+ * @ requires true;
+ * @ assignable m;
+ * @ ensures \result == ((d == 0) ? \old(m) : \old(m) / d)
+ *           && m == \old(m) + 10;
+ */
+int returnfinally(int d)
+  /*@ requires take vp0 = Owned<int>(&m);
+               let m10 = (i64)vp0 + 10i64;
+               m10 <= 2147483647i64; 
+      ensures take vp1 = Owned<int>(&m); 
+  @*/
+  {
+    int result;
+
+    if (d == 0) {
+        result = m; // Handle division by zero case
+    } else {
+        result = m / d; // Normal division
+    }
+
+    m += 10; // This corresponds to the 'finally' block in Java, executed regardless of exception
+
+    return result;
+}
+
+int main()
+  /*@ requires take vp0 = Owned<int>(&m); 
+      ensures take vp1 = Block<int>(&m);
+	      return == 0i32; 
+  @*/
+{
+    m = 20; // Initialize m
+    int d = 0; // Example divisor, change this value to test different paths
+    //printf("Result: %d\n", returnfinally(d));
+    //printf("Updated m: %d\n", m);
+    return 0;
+}

src/example-archive/simple-examples/working/division.c

@@ -0,0 +1 @@
+void a() { 1 / 1; }