diff options
| author | Robert Norton | 2017-04-27 16:17:16 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-04-27 16:17:16 +0100 |
| commit | 25852e6ee420be0de7791f865b40812ef9c96c5f (patch) | |
| tree | f1d235a16fee0fcdfad05c2828947b88bca77a8d | |
| parent | 334ce4ef4015b48f25e1ea9c13191a6c48230828 (diff) | |
remove undefined value from cheri 128 spec. The ocaml shallow embedding cannot handle undef structs and the value should not be used (could be option type but wanted a similar interface to incCapOffset and setCapOffset).
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index 8c76c744..96fdf480 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -173,7 +173,7 @@ function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) = if (((cap.T)[11..0] == 0) & ((cap.B)[11..0] == 0)) then (true, {cap with sealed=true; otype=otype}) else - (false, undefined) + (false, cap (* was undefined but ocaml shallow embedding can't handle it *) ) function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) = switch (a_mid <_u R, bound <_u R) { |