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 | |
| 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.
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 3 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 3 | ||||
| -rw-r--r-- | model/prelude.sail | 8 |
3 files changed, 10 insertions, 4 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 = () diff --git a/model/prelude.sail b/model/prelude.sail index fc4e38c..59289ed 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -104,10 +104,10 @@ val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) val print = "print_endline" : string -> unit val print_string = "print_string" : (string, string) -> unit -val print_instr = {ocaml: "Platform.print_instr", c: "print_instr", _: "print_endline"} : string -> unit -val print_reg = {ocaml: "Platform.print_reg", c: "print_reg", _: "print_endline"} : string -> unit -val print_mem = {ocaml: "Platform.print_mem_access", c: "print_mem_access", _: "print_endline"} : string -> unit -val print_platform = {ocaml: "Platform.print_platform", c: "print_platform", _: "print_endline"} : string -> unit +val print_instr = {ocaml: "Platform.print_instr", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_reg = {ocaml: "Platform.print_reg", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_mem = {ocaml: "Platform.print_mem_access", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_platform = {ocaml: "Platform.print_platform", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit $ifndef FEATURE_IMPLICITS val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) |