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

1 files changed, 25 insertions, 0 deletions

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
+  )