From 0f331e9eb5afde5d4b9f99bc55e93eabd70e3fa5 Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Fri, 15 Nov 2019 15:53:21 +0530
Subject: [PATCH] The assertion in the divbin program is violable hence changed
 the verdict of the program. Also adding the corrected program divbin2 with
 verifiable assertion.

---
 c/nla-digbench/divbin.yml  |  2 +-
 c/nla-digbench/divbin2.c   | 48 ++++++++++++++++++++++++++++++++++++++
 c/nla-digbench/divbin2.i   | 35 +++++++++++++++++++++++++++
 c/nla-digbench/divbin2.yml |  5 ++++
 4 files changed, 89 insertions(+), 1 deletion(-)
 create mode 100644 c/nla-digbench/divbin2.c
 create mode 100644 c/nla-digbench/divbin2.i
 create mode 100644 c/nla-digbench/divbin2.yml

diff --git a/c/nla-digbench/divbin.yml b/c/nla-digbench/divbin.yml
index 4bb1d3ccda5..005a4733286 100644
--- a/c/nla-digbench/divbin.yml
+++ b/c/nla-digbench/divbin.yml
@@ -2,4 +2,4 @@ format_version: '1.0'
 input_files: 'divbin.i'
 properties:
   - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+    expected_verdict: false
diff --git a/c/nla-digbench/divbin2.c b/c/nla-digbench/divbin2.c
new file mode 100644
index 00000000000..6d3a9aaa8c8
--- /dev/null
+++ b/c/nla-digbench/divbin2.c
@@ -0,0 +1,48 @@
+/*
+  A division algorithm, by Kaldewaij
+  returns A//B
+*/
+
+#include <limits.h>
+
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+  unsigned A, B;
+  unsigned q, r, b;
+    A = __VERIFIER_nondet_unsigned_int();
+    B = 1;
+
+    q = 0;
+    r = A;
+    b = B;
+
+    while (1) {
+        if (!(r >= b)) break;
+        b = 2 * b;
+    }
+
+    while (1) {
+        __VERIFIER_assert(A == q * b + r);
+        if (!(b != B)) break;
+
+        q = 2 * q;
+        b = b / 2;
+        if (r >= b) {
+            q = q + 1;
+            r = r - b;
+        }
+    }
+
+    __VERIFIER_assert(A == q * b + r);
+    return 0;
+}
diff --git a/c/nla-digbench/divbin2.i b/c/nla-digbench/divbin2.i
new file mode 100644
index 00000000000..d80c792c60a
--- /dev/null
+++ b/c/nla-digbench/divbin2.i
@@ -0,0 +1,35 @@
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+int main() {
+  unsigned A, B;
+  unsigned q, r, b;
+    A = __VERIFIER_nondet_unsigned_int();
+    B = 1;
+    q = 0;
+    r = A;
+    b = B;
+    while (1) {
+        if (!(r >= b)) break;
+        b = 2 * b;
+    }
+    while (1) {
+        __VERIFIER_assert(A == q * b + r);
+        if (!(b != B)) break;
+        q = 2 * q;
+        b = b / 2;
+        if (r >= b) {
+            q = q + 1;
+            r = r - b;
+        }
+    }
+    __VERIFIER_assert(A == q * b + r);
+    return 0;
+}
diff --git a/c/nla-digbench/divbin2.yml b/c/nla-digbench/divbin2.yml
new file mode 100644
index 00000000000..4f8d030079e
--- /dev/null
+++ b/c/nla-digbench/divbin2.yml
@@ -0,0 +1,5 @@
+format_version: '1.0'
+input_files: 'divbin2.i'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true