diff options
| author | Alasdair Armstrong | 2019-11-04 20:36:17 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-11-04 20:38:35 +0000 |
| commit | f42e1a8adbf220bd03862bb08ca5103b6e1cde09 (patch) | |
| tree | e7a4a45e34dcd8508522c15bba4dd1548fb5a071 /src/value.ml | |
| parent | 6adffb527511e1cec333b292d93e6ae6748b2c47 (diff) | |
Allow overriding the interpreter effects
This allows read_mem and read_reg effects to be handled by GDB
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/value.ml b/src/value.ml index 751c10d7..69023bc3 100644 --- a/src/value.ml +++ b/src/value.ml @@ -486,7 +486,7 @@ let value_undefined_vector = function 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" @@ -751,5 +751,3 @@ let primops = ref let add_primop name impl = primops := StringMap.add name impl !primops - - |