From befbc76f89f3d8abc8da17caf91ea4a87ec96eeb Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 28 Mar 2012 13:32:21 +0000
Subject: checklink: first import of Valentin Robert's validator for asm and
 link cparser: renamed Errors to Cerrors; removed packing into Cparser.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Bitstring_utils.ml | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 checklink/Bitstring_utils.ml

(limited to 'checklink/Bitstring_utils.ml')

diff --git a/checklink/Bitstring_utils.ml b/checklink/Bitstring_utils.ml
new file mode 100644
index 0000000..2253b63
--- /dev/null
+++ b/checklink/Bitstring_utils.ml
@@ -0,0 +1,25 @@
+(** Note that a bitstring is a triple (string * int * int), where the string
+    contains the contents (the last char is filled up with zeros if necessary),
+    the firts int gives the first bit to consider, and the second int gives the
+    bit length of the considered bitstring.
+*)
+type bitstring = Bitstring.bitstring
+
+(** Checks whether a given number of bits of a bitstring are zeroed. The
+    bitstring may be longer.
+    @param size number of bits to check
+*)
+let rec is_zeros (bs: bitstring) (size: int): bool =
+  size = 0 ||
+  if size >= 64
+  then (
+    bitmatch bs with
+    | { 0L : 64 : int ; rest : -1 : bitstring } ->
+        is_zeros rest (size - 64)
+    | { _ } -> false
+  )
+  else (
+    bitmatch bs with
+    | { 0L : size : int } -> true
+    | { _ } -> false
+  )
-- 
cgit v1.2.3