From 2dd28164e40241a2117142fbb197c967740f196d Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 17 Jun 2019 14:25:01 +0100
Subject: Implement a count_leading_zeros builtin for ocaml and c. This may be
 a slight performance improvement and keeps compatibility with smt backend
 that already had a builtin for this because it can't handle the loop in the
 sail version. Will need implementations for prover backends.

---
 test/builtins/clz.sail | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test/builtins/clz.sail

(limited to 'test')

diff --git a/test/builtins/clz.sail b/test/builtins/clz.sail
new file mode 100644
index 00000000..5cf20068
--- /dev/null
+++ b/test/builtins/clz.sail
@@ -0,0 +1,9 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  assert(count_leading_zeros(0x0) == 4);
+  assert(count_leading_zeros(0x1) == 3);
+  assert(count_leading_zeros(0x4) == 1);
+  assert(count_leading_zeros(0xf) == 0);
+}
\ No newline at end of file
-- 
cgit v1.2.3