From ac7a3d0b508f9a055a85f2aa8842a5e7d9b2ff3f Mon Sep 17 00:00:00 2001
From: Alastair Reid
Date: Fri, 29 Jun 2018 01:22:18 +0100
Subject: 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.
---
 aarch64/prelude.sail | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'aarch64')

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}
 
-- 
cgit v1.2.3