diff options
| author | Alasdair Armstrong | 2019-04-15 14:15:09 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-15 17:22:55 +0100 |
| commit | fb88a51fbfd74482a4e5bcbada7c4c749db4d5ba (patch) | |
| tree | 6908de3f59734247d7ffe946f6ab6247b001f650 /src/value.ml | |
| parent | 7cfbabc2bfba4f7d2ba0d3f91c7068ac3b1a84d1 (diff) | |
SMT: Allow partial specializations
Change specialisation so we only specialize integer parameters when
they are constant. This makes ensures that the integer-specialised
code is always type-correct.
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/value.ml b/src/value.ml index 82647860..6f5148e4 100644 --- a/src/value.ml +++ b/src/value.ml @@ -100,7 +100,7 @@ let coerce_bit = function let is_bit = function | V_bit _ -> true | _ -> false - + let rec string_of_value = function | V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs) | V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]" |