diff options
| -rw-r--r-- | aarch64_small/armV8_common_lib.sail | 27 | ||||
| -rw-r--r-- | aarch64_small/armV8_lib.h.sail | 1 |
2 files changed, 14 insertions, 14 deletions
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail index c2ed72ee..4ba36dc5 100644 --- a/aarch64_small/armV8_common_lib.sail +++ b/aarch64_small/armV8_common_lib.sail @@ -32,6 +32,20 @@ /* SUCH DAMAGE. */ /*========================================================================*/ + +/** FUNCTION:shared/functions/system/Unreachable */ + +/* CP: adding two variants, one that takes a string argument, the other one doesn't */ +val Unreachable_no_message : forall ('a : Type) . unit -> 'a effect{escape} +function Unreachable_no_message() = + error("Unreachable reached") + +val Unreachable_message : forall ('a : Type) . string -> 'a effect{escape} +function Unreachable_message(message) = + error(message) + +overload Unreachable = {Unreachable_no_message, Unreachable_message} + /** FUNCTION:shared/debug/DoubleLockStatus/DoubleLockStatus */ function DoubleLockStatus() -> boolean= { @@ -996,19 +1010,6 @@ function SendEvent() -> unit = /* TODO: ??? */ } -/** FUNCTION:shared/functions/system/Unreachable */ - -/* CP: adding two variants, one that takes a string argument, the other one doesn't */ -val Unreachable_no_message : forall ('a : Type) . unit -> 'a effect{escape} -function Unreachable_no_message() = - error("Unreachable reached") - -val Unreachable_message : forall ('a : Type) . string -> 'a effect{escape} -function Unreachable_message(message) = - error(message) - -overload Unreachable = {Unreachable_no_message, Unreachable_message} - /** FUNCTION:shared/functions/system/UsingAArch32 */ diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail index 332ad18c..5ace3f01 100644 --- a/aarch64_small/armV8_lib.h.sail +++ b/aarch64_small/armV8_lib.h.sail @@ -179,7 +179,6 @@ val Halted : unit -> boolean effect {rreg} val HaveEL : bits(2) -> boolean effect {escape} val HaveAnyAArch32 : unit -> boolean effect pure val HighestELUsingAArch32 : unit -> boolean effect pure -val Unreachable : unit -> unit effect {escape} val Hint_Branch : BranchType -> unit effect pure /*************************************************************************/ |