diff options
author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-04-03 11:38:47 +0100 |
---|---|---|
committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-04-03 11:44:49 +0100 |
commit | 12951120dc3d1dab5750d80ae8809943259198e3 (patch) | |
tree | 895bac5602e5c069a5f19f3d8b97cb2733e07235 /handwritten_support | |
parent | 9f30ffdb88b744c09370829ef73d1f293b62f76d (diff) | |
download | sail-riscv-12951120dc3d1dab5750d80ae8809943259198e3.zip sail-riscv-12951120dc3d1dab5750d80ae8809943259198e3.tar.gz sail-riscv-12951120dc3d1dab5750d80ae8809943259198e3.tar.bz2 |
Tweak print_* bindings for Lem
Map to a function that does not actuaylly output anything, in order to
not confuse rmem.
Diffstat (limited to 'handwritten_support')
-rw-r--r-- | handwritten_support/riscv_extras.lem | 3 | ||||
-rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 3 |
2 files changed, 6 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 738c9c6..d2cd03b 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -147,3 +147,6 @@ let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) + +val print_dbg : string -> unit +let print_dbg msg = () diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 5f147ee..604911a 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -143,3 +143,6 @@ let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) + +val print_dbg : string -> unit +let print_dbg msg = () |