summaryrefslogtreecommitdiff
path: root/aarch64
diff options
context:
space:
mode:
authorAlastair Reid2018-06-29 01:22:18 +0100
committerAlastair Reid2018-06-29 01:22:18 +0100
commitac7a3d0b508f9a055a85f2aa8842a5e7d9b2ff3f (patch)
tree6150ea3e2b2d125c63632325bffdc3cc43be5486 /aarch64
parent3a91534b233ab63fb5ac91ffd92a4d75cc533180 (diff)
Prelude: drop escape effect from sleep/verbosity primops
It appears that primops that have the escape effect are required to write to the have_exception flag so I am dropping the effect from primops that don't actually escape.
Diffstat (limited to 'aarch64')
-rwxr-xr-xaarch64/prelude.sail8
1 files changed, 4 insertions, 4 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 74298e00..73a084c4 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -350,11 +350,11 @@ union option ('a : Type) = {
}
*/
-val __SleepRequest = {ocaml: "sleep_request", lem: "sleep_request", smt: "sleep_request", interpreter: "sleep_request", c: "sleep_request"}: unit -> unit effect {escape, rreg, undef}
+val __SleepRequest = {ocaml: "sleep_request", lem: "sleep_request", smt: "sleep_request", interpreter: "sleep_request", c: "sleep_request"}: unit -> unit effect {rreg, undef}
-val __WakeupRequest = {ocaml: "wakeup_request", lem: "wakeup_request", smt: "wakeup_request", interpreter: "wakeup_request", c: "wakeup_request"}: unit -> unit effect {escape, rreg, undef}
+val __WakeupRequest = {ocaml: "wakeup_request", lem: "wakeup_request", smt: "wakeup_request", interpreter: "wakeup_request", c: "wakeup_request"}: unit -> unit effect {rreg, undef}
-val __Sleeping = {ocaml: "sleeping", lem: "sleeping", smt: "sleeping", interpreter: "sleeping", c: "sleeping"}: unit -> bool effect {escape, rreg, undef}
+val __Sleeping = {ocaml: "sleeping", lem: "sleeping", smt: "sleeping", interpreter: "sleeping", c: "sleeping"}: unit -> bool effect {rreg, undef}
-val __GetVerbosity = {c: "sail_get_verbosity"}: unit -> bits(64) effect {escape, rreg, undef}
+val __GetVerbosity = {c: "sail_get_verbosity"}: unit -> bits(64) effect {rreg, undef}