begin bitfields

1 files changed, 15 insertions, 0 deletions

diff --git a/common/Values.v b/common/Values.v
index a20dd567..ae8d31f3 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -766,6 +766,21 @@ Definition rolml (v: val) (amount: int) (mask: int64): val :=
   | _ => Vundef
   end.
 
+
+Definition extfz stop start v :=
+  if (Int.cmp Cle start stop)
+       && (Int.cmp Cge start Int.zero)
+       && (Int.cmp Clt stop Int.iwordsize)
+  then
+    let stop' := Int.add stop Int.one in
+    match v with
+    | Vint w =>
+      Vint (Int.shr (Int.shl w (Int.sub Int.iwordsize stop')) (Int.sub Int.iwordsize (Int.sub stop' start)))
+    | _ => Vundef
+    end
+  else Vundef.
+
+
 (** Comparisons *)
 
 Section COMPARISONS.