diff options
| author | Alasdair <alasdair.armstrong@cl.cam.ac.uk> | 2023-10-10 12:14:35 +0100 |
|---|---|---|
| committer | Bill McSpadden <bill@riscv.org> | 2023-10-10 19:17:34 -0500 |
| commit | 532714a6c71b47a91176eb90fef3b3b049c52fce (patch) | |
| tree | 7113f79e789525e40955ce33606b7dc16c66aad2 | |
| parent | 38658363547f5ec058feeea54bf028a317cf04fe (diff) | |
| download | sail-riscv-532714a6c71b47a91176eb90fef3b3b049c52fce.zip sail-riscv-532714a6c71b47a91176eb90fef3b3b049c52fce.tar.gz sail-riscv-532714a6c71b47a91176eb90fef3b3b049c52fce.tar.bz2 | |
Fix lem build error
The speculate_conditional should be marked monadic. It would seem like
the various _reservation functions should be also, but it seems like
perhaps they are not implemented in lem right now.
| -rw-r--r-- | model/riscv_sys_control.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index cf0a488..7746b6b 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -228,7 +228,7 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = * where cancellation can be performed. */ -val speculate_conditional = {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool +val speculate_conditional = monadic {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool |