diff options
| author | Jon French | 2019-04-12 14:44:30 +0100 |
|---|---|---|
| committer | Jon French | 2019-04-12 14:44:30 +0100 |
| commit | 566296e39a3f6cd472d86c13e075c3d8b8c1bf03 (patch) | |
| tree | bd93377137bfaf35e3e2d907df47c19afa66cbeb /lib | |
| parent | f2cdaab5fd7f648c1037c504e289e881ce8bbf47 (diff) | |
lib/regfp.sail: add explicit C binding for memory access functions
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/regfp.sail | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail index c191d654..90af9b44 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -115,19 +115,19 @@ union instruction_kind = { } val __read_mem - = { ocaml: "Platform.read_mem", _: "read_mem" } + = { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" } : forall 'n, 'n > 0. (read_kind, bits(64), int('n)) -> bits(8 * 'n) effect {rmem} val __write_mem_ea - = { ocaml: "Platform.write_mem_ea", _: "write_mem_ea" } + = { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" } : forall 'n, 'n > 0. (write_kind, bits(64), int('n)) -> unit effect {eamem} val __write_mem - = { ocaml: "Platform.write_mem", _: "write_mem" } + = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" } : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {wmv} val __excl_res - = { ocaml: "Platform.excl_res", _: "excl_res" } + = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_res" } : unit -> bool effect {exmem} val __barrier - = { ocaml: "Platform.barrier", _: "barrier" } + = { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" } : barrier_kind -> unit effect {barr} |