From 92f50f2564834fcbeda250337c3acce571f7d6f0 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 16 Jul 2019 22:12:42 +0100
Subject: Fix all remaining tests for this branch

---
 src/value.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/value.ml')

diff --git a/src/value.ml b/src/value.ml
index c509c81f..71d9ffe6 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -483,6 +483,10 @@ let value_undefined_vector = function
   | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2))
   | _ -> failwith "value undefined_vector"
 
+let value_undefined_bitvector = function
+  | [v] -> V_vector (Sail_lib.undefined_vector (coerce_int v, V_bit (Sail_lib.B0)))
+  | _ -> failwith "value undefined_bitvector"
+       
 let value_read_ram = function
   | [v1; v2; v3; v4] -> mk_vector (Sail_lib.read_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4))
   | _ -> failwith "value read_ram"
@@ -731,6 +735,7 @@ let primops =
       ("undefined_int", fun _ -> V_int Big_int.zero);
       ("undefined_nat", fun _ -> V_int Big_int.zero);
       ("undefined_bool", fun _ -> V_bool false);
+      ("undefined_bitvector", value_undefined_bitvector);
       ("undefined_vector", value_undefined_vector);
       ("undefined_string", fun _ -> V_string "");
       ("internal_pick", value_internal_pick);
-- 
cgit v1.2.3