diff options
| author | Jon French | 2019-05-13 16:27:31 +0100 |
|---|---|---|
| committer | Jon French | 2019-05-13 16:27:31 +0100 |
| commit | 719cb42ac0263d45b8d99eaf2845e28c79702863 (patch) | |
| tree | 64f19d546bf420dce69cacb425766f1b8907b44e /aarch64_small | |
| parent | cc90f4b8c1254f119aabc4bbf913f257b4205d25 (diff) | |
aarch64_small: move around Unreachable fns to sort dependency issue
Diffstat (limited to 'aarch64_small')
| -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 /*************************************************************************/ |
