summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_interface.lem
diff options
context:
space:
mode:
authorPeter Sewell2014-11-22 23:12:51 +0000
committerPeter Sewell2014-11-22 23:12:51 +0000
commit13293f193bafef81ab90575a9bdfd536396f914b (patch)
tree96b218c6e13de5c63e37ebcec4a8c1a6fb954097 /src/lem_interp/interp_interface.lem
parent48ab677924ce1392447a4a57f37d2065a4113c20 (diff)
sorry, interp_interface didn't build. now it does
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
-rw-r--r--src/lem_interp/interp_interface.lem4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index b05c6303..ab369a03 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -169,12 +169,14 @@ type direction =
| D_increasing
| D_decreasing
-type register_value = <| rv_bits: list bit_lifted; rv_dir: direction; rv_start: integer |>
+type register_value = <| rv_bits: list bit_lifted; rv_dir: direction; rv_start: int |> (* beter for this to be int, not integer *)
type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *)
type instruction_field_value = list bit
+type byte = Byte of list bit (* of length 8 *)
+
type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*)
type memory_byte = byte_lifted