summaryrefslogtreecommitdiff
path: root/src/value.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2020-02-20 17:21:42 +0000
committerAlasdair Armstrong2020-02-20 17:21:42 +0000
commita04a740a3b564f2a9b09ca0a2366043eac3e8bc0 (patch)
tree20bc2e3d495ecd317f7580378a58c906599675c5 /src/value.ml
parent742eee392609a01b8565f4e64806ba0a14997844 (diff)
More list C codegen fixes for issue #59
Diffstat (limited to 'src/value.ml')
-rw-r--r--src/value.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml
index b166e99b..3e7782ed 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -491,6 +491,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_list = function
+ | [_] -> V_list []
+ | _ -> failwith "value undefined_list"
+
let value_undefined_bitvector = function
| [v] -> V_vector (Sail_lib.undefined_vector (coerce_int v, V_bit (Sail_lib.B0)))
| _ -> failwith "value undefined_bitvector"
@@ -747,6 +751,7 @@ let primops = ref
("undefined_bool", fun _ -> V_bool false);
("undefined_bitvector", value_undefined_bitvector);
("undefined_vector", value_undefined_vector);
+ ("undefined_list", value_undefined_list);
("undefined_string", fun _ -> V_string "");
("internal_pick", value_internal_pick);
("replicate_bits", value_replicate_bits);