diff options
| author | Robert Norton | 2017-04-27 10:43:38 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-04-27 10:43:38 +0100 |
| commit | bbed94896ab872d7b3d1939c8ad21d1c7fe04665 (patch) | |
| tree | be866bbc981ca1d38dd5b6228707e773d1f0a9d4 /src | |
| parent | 0a4963271c28cea3aa3eabf2115f4a22a4c2fa23 (diff) | |
add command line argument for setting undef values to all zero or all one. Some tests intentionally produce undefined values (e.g. divide by zero) and this might be required for them to work.
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 1516c503..7e6f0ae7 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -11,6 +11,8 @@ type _bool = vbit type _string = string type _nat = number +let undef_val = ref Vundef + type value = | Vvector of vbit array * int * bool | VvectorR of value array * int * bool @@ -25,6 +27,12 @@ let string_of_bit = function | Vzero -> "0" | Vundef -> "u" +let bit_of_string = function + | "1" -> Vone + | "0" -> Vzero + | "u" -> Vundef + | _ -> failwith "invalid bit value" + let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a) let string_of_value = function @@ -509,13 +517,13 @@ let to_vec_inc = to_vec_inc_big let to_vec_dec = to_vec_dec_big let to_vec_undef_int ord len = - let array = Array.make len Vundef in + let array = Array.make len !undef_val in let start = if ord then 0 else len-1 in Vvector(array, start, ord) let to_vec_undef_big ord len = let len = int_of_big_int len in - let array = Array.make len Vundef in + let array = Array.make len !undef_val in let start = if ord then 0 else len-1 in Vvector(array, start, ord) |
