From 82acf052d4392f0662fa62cccea2353d57b4145a Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 3 Apr 2024 16:12:24 +0100 Subject: lem: Add PMP related stubs for Isabelle build These stub functions are required for building the Riscv.thy file from the generated lem file. --- handwritten_support/riscv_extras.lem | 8 ++++++++ 1 file changed, 8 insertions(+) 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` -- cgit v1.1