summaryrefslogtreecommitdiff
path: root/src/sail_lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/sail_lib.ml')
-rw-r--r--src/sail_lib.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 21d95e64..3812e4f7 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -106,6 +106,11 @@ let rec undefined_vector (len, item) =
then []
else item :: undefined_vector (Big_int.sub len (Big_int.of_int 1), item)
+let rec undefined_bitvector len =
+ if Big_int.equal len Big_int.zero
+ then []
+ else B0 :: undefined_vector (Big_int.sub len (Big_int.of_int 1), B0)
+
let undefined_string () = ""
let undefined_unit () = ()