diff options
| author | Alasdair Armstrong | 2018-11-05 17:05:58 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-11-05 17:05:58 +0000 |
| commit | a3de0c3913d9dec549ebf96496dbf340fa7b124e (patch) | |
| tree | ff8a9d7a7eb5a3c17acbb691a73f16ad1d21d1c2 | |
| parent | 21e94e35b56b86d56b720ac2a38d22020f41fc19 (diff) | |
Add a regression test for issue #22
| -rw-r--r-- | test/c/cheri_capstruct_order.expect | 1 | ||||
| -rw-r--r-- | test/c/cheri_capstruct_order.sail | 32 |
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 |
