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.

---
 lib/sail.h | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/sail.h')

diff --git a/lib/sail.h b/lib/sail.h
index 1a123cf4..eddf6e41 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -262,6 +262,7 @@ fbits fast_sign_extend(const fbits op, const uint64_t n, const uint64_t m);
 fbits fast_sign_extend2(const sbits op, const uint64_t m);
 
 void length_lbits(sail_int *rop, const lbits op);
+void count_leading_zeros(sail_int *rop, const lbits op);
 
 bool eq_bits(const lbits op1, const lbits op2);
 bool EQUAL(lbits)(const lbits op1, const lbits op2);
-- 
cgit v1.2.3