diff options
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 66b5d94..da6106d 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -111,6 +111,10 @@ val plat_enable_misaligned_access : unit -> bool let plat_enable_misaligned_access () = false declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` +val plat_enable_pmp : unit -> bool +let plat_enable_pmp () = false +declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` + val plat_mtval_has_illegal_inst_bits : unit -> bool let plat_mtval_has_illegal_inst_bits () = false declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 604911a..7715614 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -107,6 +107,10 @@ val plat_enable_misaligned_access : unit -> bool let plat_enable_misaligned_access () = false declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` +val plat_enable_pmp : unit -> bool +let plat_enable_pmp () = false +declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` + val plat_mtval_has_illegal_inst_bits : unit -> bool let plat_mtval_has_illegal_inst_bits () = false declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` |