summaryrefslogtreecommitdiff
path: root/aarch64_small
diff options
context:
space:
mode:
authorJon French2019-05-13 16:27:31 +0100
committerJon French2019-05-13 16:27:31 +0100
commit719cb42ac0263d45b8d99eaf2845e28c79702863 (patch)
tree64f19d546bf420dce69cacb425766f1b8907b44e /aarch64_small
parentcc90f4b8c1254f119aabc4bbf913f257b4205d25 (diff)
aarch64_small: move around Unreachable fns to sort dependency issue
Diffstat (limited to 'aarch64_small')
-rw-r--r--aarch64_small/armV8_common_lib.sail27
-rw-r--r--aarch64_small/armV8_lib.h.sail1
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
/*************************************************************************/