diff options
| author | Alasdair Armstrong | 2020-02-20 17:21:42 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2020-02-20 17:21:42 +0000 |
| commit | a04a740a3b564f2a9b09ca0a2366043eac3e8bc0 (patch) | |
| tree | 20bc2e3d495ecd317f7580378a58c906599675c5 /src/value.ml | |
| parent | 742eee392609a01b8565f4e64806ba0a14997844 (diff) | |
More list C codegen fixes for issue #59
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 5 |
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); |
