smack icon indicating copy to clipboard operation
smack copied to clipboard

Published 20 hours ago • verified publisher icon smackers

Model realloc

Open shaobo-he opened this issue 8 years ago • 8 comments

Memory reallocation is used by rust libraries (e.g., vec). We need to model it properly.

shaobo-he avatar Mar 31 '16 05:03 shaobo-he

Is it possible to write a C-language test case for this?

michael-emmi avatar Apr 03 '16 14:04 michael-emmi

@Guoanshisb (Shaobo): Please write a simple C program that uses realloc, which we can use to debug this. @michael-emmi : To model realloc, we most likely need $Size to be present in all memory models. The pull request related to memory safety is supposed to do that. I just provided feedback to that pull request. I will stay on top of it this time around and try to merge it soon. Then we can take care of realloc.

zvonimir avatar Apr 04 '16 02:04 zvonimir

Simple tests for correct realloc behavior. Attached as a .txt file since github rejects .c files. realloc_simple.txt

keram88 avatar Apr 06 '16 00:04 keram88

This issue has been resolved: we model realloc as free-then-malloc.

shaobo-he avatar Feb 04 '20 22:02 shaobo-he

Has Mark's program been added to our regressions?

zvonimir avatar Feb 04 '20 22:02 zvonimir

Has Mark's program been added to our regressions?

No, SMACK reports an error for Mark's program as we don't model copying in realloc.

shaobo-he avatar Feb 04 '20 22:02 shaobo-he

Could we update the model to include copying as well?

zvonimir avatar Feb 06 '20 17:02 zvonimir

Could we update the model to include copying as well?

This might be very tricky since we have to keep track of the memory associated with the base pointer.

@keram88 thoughts?

shaobo-he avatar Feb 06 '20 18:02 shaobo-he