summaryrefslogtreecommitdiff
path: root/riscv/riscv_extras.lem
diff options
context:
space:
mode:
Diffstat (limited to 'riscv/riscv_extras.lem')
-rw-r--r--riscv/riscv_extras.lem4
1 files changed, 4 insertions, 0 deletions
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 60d9852a..7c346688 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -72,6 +72,10 @@ val plat_enable_dirty_update : unit -> bool
let plat_enable_dirty_update () = false
declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`
+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_insns_per_tick : unit -> integer
let plat_insns_per_tick () = 1
declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`