Cheri-research/cheri-cap-lib
1
0
Fork 0
Code Issues 1 Pull Requests Actions Packages Projects Releases Wiki Activity

fix property following getLength return type change in b3896e4e50

Browse Source
This commit is contained in:
Alexandre Joannou
2025-02-10 17:44:09 +00:00
parent 2295c3b8c0
commit 595447fd62
1 changed files with 4 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
CHERICapProps.bsv
View File

@@ -52,7 +52,7 @@ function Bool forallBaseAndLen(CapAddr base, CapAddr len,
Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
return baseCap.exact && implies
( boundedCap.exact
( boundedCap.exact
, prop(boundedCap.value)
);
endfunction
@@ -107,10 +107,10 @@ function Bool prop_exact(CapAddr base, CapAddr len);
Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
Exact#(CapPipe) baseCap2 = setAddr(almightyCap, getBase(boundedCap.value));
CapAddrPlus1 length = getLength(boundedCap.value);
Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, truncate(length));
CapAddr length = getLength(boundedCap.value);
Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, length);
return baseCap.exact && baseCap2.exact && implies
( truncateLSB(length) == 1'b0
( ~length != 0
, boundedCap2.exact
);
endfunction