Skip to content

Commit

Permalink
Fix lem build error
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Alasdair committed Oct 10, 2023
1 parent dbea780 commit 12a549c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 12a549c

Please sign in to comment.