Skip to content

Commit

Permalink
lem: Add PMP related stubs for Isabelle build
Browse files Browse the repository at this point in the history
These stub functions are required for building the Riscv.thy file
from the generated lem file.
  • Loading branch information
Alasdair authored and billmcspadden-riscv committed May 10, 2024
1 parent 440ac2c commit 82acf05
Showing 1 changed file with 8 additions and 0 deletions.
8 changes: 8 additions & 0 deletions handwritten_support/riscv_extras.lem
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down

0 comments on commit 82acf05

Please sign in to comment.