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/sail_lib.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/sail_lib.ml')
| -rw-r--r-- | src/sail_lib.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 164bcefa..8251f9b4 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -274,9 +274,7 @@ let rec replicate_bits (bits, n) = let identity x = x - - -(* +(* Returns list of n bits of integer m starting from offset o >= 0 (bits numbered from least significant). Uses twos-complement representation for m<0 and pads most significant bits in sign-extended way. Most significant bit is head of returned list. @@ -529,7 +527,7 @@ let fast_read_ram (data_size, addr) = !vector let tag_ram = (ref Mem.empty : (bool Mem.t) ref);; - + let write_tag_bool (addr, tag) = let addri = uint addr in tag_ram := Mem.add addri tag !tag_ram @@ -551,7 +549,6 @@ let lor_int (n, m) = Big_int.bitwise_or n m let land_int (n, m) = Big_int.bitwise_and n m let lxor_int (n, m) = Big_int.bitwise_xor n m - let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2 ^ string_of_bits v) let eq_string (str1, str2) = String.compare str1 str2 == 0 |