Closed zpzigi754 closed 5 months ago
This PR fixes a bug in granule_undelegate, found by model checking. Note that the previous page table-based GST didn't contain this bug.
granule_undelegate
[B.3.3.6.3 Success conditions in beta0 (B.4.3.6.3 in eac5)]
ID Condition ... gran_content Contents of target Granule are wiped.
This PR fixes a bug in
granule_undelegate, found by model checking. Note that the previous page table-based GST didn't contain this bug.[B.3.3.6.3 Success conditions in beta0 (B.4.3.6.3 in eac5)]