From 532714a6c71b47a91176eb90fef3b3b049c52fce Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 10 Oct 2023 12:14:35 +0100 Subject: [PATCH] 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. --- model/riscv_sys_control.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index cf0a488cc..7746b6bcb 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