diff options
| author | Robert Norton <rmn30@cam.ac.uk> | 2019-03-07 17:31:10 +0000 |
|---|---|---|
| committer | Robert Norton <rmn30@cam.ac.uk> | 2019-03-07 17:31:10 +0000 |
| commit | ad44eb77aa89a5e87d7454dec70f1655bc061ef3 (patch) | |
| tree | 2f5878de296523fee0a6d701576588bc5a7216eb | |
| parent | 215c2b31d2c1649a40bfebb1e060e7095001813f (diff) | |
| download | sail-riscv-ad44eb77aa89a5e87d7454dec70f1655bc061ef3.zip sail-riscv-ad44eb77aa89a5e87d7454dec70f1655bc061ef3.tar.gz sail-riscv-ad44eb77aa89a5e87d7454dec70f1655bc061ef3.tar.bz2 | |
Prohibit modifying sealed capabilities by setting mepc etc. Similar to cheri-mips issue.
| -rw-r--r-- | model/cheri_prelude_128.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/model/cheri_prelude_128.sail b/model/cheri_prelude_128.sail index 382ac4f..4d43f7e 100644 --- a/model/cheri_prelude_128.sail +++ b/model/cheri_prelude_128.sail @@ -377,7 +377,7 @@ function setCapOffset(c, offset) : (Capability, bits(64)) -> (bool, Capability) function setCapOffsetOrNull (cap, offset) : (Capability, bits(64)) -> Capability = let (representable, newCap) = setCapOffset(cap, offset) in - if representable then newCap else int_to_cap(newCap.address) + if representable & not(cap.sealed) then newCap else int_to_cap(newCap.address) function incCapOffset(c, delta) : (Capability, bits(64)) -> (bool, Capability) = let newAddress : bits(64) = c.address + delta in |