search

UQ-PAC / BASIL

Apache License 2.0
8 stars 0 forks source link

MMM region end clues #202

Open yousifpatti opened 5 months ago

yousifpatti commented 5 months ago

In case

S1:  R1 := R31 + 3
S2:  R2 := R1 + 5
S3:  R3 = MemLoad[R2]

Then we need to make the regions

Stack(3)
Stack(8)

Then exclusion offsets are Set(4, 5, 6, 7, 8) such that if we evaluate a direct access (without pointer arithmetic) ie. R31 + 4 then we need to say Stack(3) is not a proper region or that it's range(3, end) end value needs to be up to 4

Reference Nick, Kirsten

yousifpatti commented 5 months ago

May be good to add an assertion that boogie can verify (in case we are not sure we can split this memory region)

Reference Nick