diff options
| author | Peter Sewell | 2018-07-27 18:16:52 +0100 |
|---|---|---|
| committer | Peter Sewell | 2018-07-27 18:16:52 +0100 |
| commit | 4c84c70eafbbf9bea475e3264f21eedc3555021f (patch) | |
| tree | 549c7898e945144e032c3c8e2f21ef943dfeddce /cheri/sail_latexcc/sailccfncapRegToCapStruct.tex | |
| parent | 6e80b938e5e72edebb1953602ba4d40f668e7426 (diff) | |
wib
Diffstat (limited to 'cheri/sail_latexcc/sailccfncapRegToCapStruct.tex')
| -rw-r--r-- | cheri/sail_latexcc/sailccfncapRegToCapStruct.tex | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex b/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex deleted file mode 100644 index 4af338b9..00000000 --- a/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex +++ /dev/null @@ -1,27 +0,0 @@ -function #\hyperref[zcapRegToCapStruct]{capRegToCapStruct}#(c) : CapReg -> CapStruct = - let s : bool = c[104] in - let Bc : #\hyperref[zbits]{bits}#(20) = if s then c[103..96] @ 0x000 else c[103..84] in - let Tc : #\hyperref[zbits]{bits}#(20) = if s then c[83..76] @ 0x000 else c[83..64] in - let otype : #\hyperref[zbits]{bits}#(24) = if s then c[95..84] @ c[75..64] else #\hyperref[zzzeros]{zeros}#() in - struct { - tag = c[128], - uperms = c[127..124], - access_system_regs = c[123], - permit_unseal = c[122], - permit_ccall = c[121], - permit_seal = c[120], - permit_store_local_cap = c[119], - permit_store_cap = c[118], - permit_load_cap = c[117], - permit_store = c[116], - permit_load = c[115], - permit_execute = c[114], - global = c[113], - reserved = c[112..111], - E = c[110..105], - sealed = s, - B = Bc, - T = Tc, - otype = otype, - address = c[63..0] - } |
