MPS issue job004009

TitleCan't split a segment if buffer is above the split point
Assigned userGareth Rees
Descriptiondesign.mps.seg.split.inv.buffer says, "If seg is attached to a buffer, the buffered region must not include [the split address]". (Note that this condition is overly strict: it should be fine for the buffer to include the split address if that address is the base of the buffer. I guess this is just imprecise wording.)

But the condition that SegSplit checks is more stringent:

    /* Can only split a buffered segment if the entire buffer is below
     * the split point. */
    AVER(SegBuffer(seg) == NULL || BufferLimit(SegBuffer(seg)) <= at);

For symmetry, it should also be possible to split a buffered segment if the entire buffer is above the split point.
AnalysisNone as yet.
How foundinspection
EvidenceNone as yet.
Created byGareth Rees
Created on2016-04-19 12:40:22
Last modified byGareth Rees
Last modified on2016-04-22 10:12:12
History2016-04-19 GDR Created.