diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-22 18:25:53 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-22 18:25:53 -0800 |
| commit | 0c19e38b8ea0c3dac1a684c59e6956097bf58dc8 (patch) | |
| tree | c0ee68fabd76534c60f840a9c8bb3179bd1d2efc | |
| parent | eaa9c30a44e6eedbe54e62994caedbb114924be8 (diff) | |
| download | sail-riscv-0c19e38b8ea0c3dac1a684c59e6956097bf58dc8.zip sail-riscv-0c19e38b8ea0c3dac1a684c59e6956097bf58dc8.tar.gz sail-riscv-0c19e38b8ea0c3dac1a684c59e6956097bf58dc8.tar.bz2 | |
Some fixes for lem build.
| -rw-r--r-- | handwritten_support/0.11/riscv_extras.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/handwritten_support/0.11/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem index f4ade26..cc48761 100644 --- a/handwritten_support/0.11/riscv_extras.lem +++ b/handwritten_support/0.11/riscv_extras.lem @@ -79,6 +79,10 @@ val sys_enable_rvc : unit -> bool let sys_enable_rvc () = true declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc` +val sys_enable_fdext : unit -> bool +let sys_enable_fdext () = true +declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext` + val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 declare ocaml target_rep function plat_ram_base = `Platform.dram_base` diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index da6106d..d8dec88 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -79,6 +79,10 @@ val sys_enable_rvc : unit -> bool let sys_enable_rvc () = true declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc` +val sys_enable_fdext : unit -> bool +let sys_enable_fdext () = true +declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext` + val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 declare ocaml target_rep function plat_ram_base = `Platform.dram_base` |