test/c/cheri_capstruct_order.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
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")
}