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 /model/prelude.sail | |
| 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 'model/prelude.sail')
| -rw-r--r-- | model/prelude.sail | 8 |
1 files changed, 4 insertions, 4 deletions
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) |