search

swtv-kaist / cs458-fall22

1 stars 0 forks source link

Question regarding memory model of CBMC #42

Open A-Mehdi opened 1 year ago

A-Mehdi commented 1 year ago

I have a question regarding this slide, why does the first assert is not violated? Even though the allocated memory regions do not overlap, m1 + 30 is outside the allocated region of m1, so why there can't be a collision with m1 + 30 and allocated memory for m2? (Similarly for the second assert, m1 + a case)

image

moonzoo commented 1 year ago

why there can't be a collision with m1 + 30 and allocated memory for m2?

This is because CBMC's memory model is not a linear sequence of bytes unlike physical memory. You can simply assume that dynamically allocated memory regions are completely separated (i.e., they cannot reach each other even through pointer arithmetic).