aboutsummaryrefslogtreecommitdiff
path: root/handwritten_support/riscv_extras.lem
diff options
context:
space:
mode:
Diffstat (limited to 'handwritten_support/riscv_extras.lem')
-rw-r--r--handwritten_support/riscv_extras.lem4
1 files changed, 0 insertions, 4 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index bc04c2d..27e8ee5 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -201,10 +201,6 @@ 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`