summaryrefslogtreecommitdiff
path: root/test/c
diff options
context:
space:
mode:
Diffstat (limited to 'test/c')
-rw-r--r--test/c/cheri_capstruct_order.expect1
-rw-r--r--test/c/cheri_capstruct_order.sail32
2 files changed, 33 insertions, 0 deletions
diff --git a/test/c/cheri_capstruct_order.expect b/test/c/cheri_capstruct_order.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/cheri_capstruct_order.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/cheri_capstruct_order.sail b/test/c/cheri_capstruct_order.sail
new file mode 100644
index 00000000..6eb774dd
--- /dev/null
+++ b/test/c/cheri_capstruct_order.sail
@@ -0,0 +1,32 @@
+default Order dec
+
+val SignalException : unit -> unit effect {rreg}
+
+val SignalExceptionBadAddr : unit -> unit effect {rreg}
+
+function SignalExceptionBadAddr() = {
+ SignalException();
+}
+
+struct CapStruct = {
+ base : bool,
+}
+
+type CapReg = CapStruct
+
+function getCapBase(c) : CapStruct -> bool = c.base
+
+register KCC : CapReg
+
+function SignalException () = {
+ base = getCapBase(KCC);
+ ();
+}
+
+val "print_endline" : string -> unit
+
+val main : unit -> unit
+
+function main() = {
+ print_endline("ok")
+} \ No newline at end of file