diff options
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 27e8ee5..4bc3300 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -169,6 +169,14 @@ val sys_enable_writable_fiom : unit -> bool let sys_enable_writable_fiom () = true declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom` +val sys_pmp_grain : unit -> integer +let sys_pmp_grain () = 0 +declare ocaml target_rep function sys_pmp_grain = `Platform.sys_pmp_grain` + +val sys_pmp_count : unit -> integer +let sys_pmp_count () = 0 +declare ocaml target_rep function sys_pmp_count = `Platform.sys_pmp_count` + val plat_ram_base : unit -> bitvector let plat_ram_base () = [] declare ocaml target_rep function plat_ram_base = `Platform.dram_base` |