SMACK does not catch freeing of stack locations as an invalid-free error

[zvonimir]

Here is a simple regression for this:

#include "smack.h"

int main(void) {
  int x = __VERIFIER_nondet_int();
  int *y = &x;
  free(y);
  return 0;
}

This regression should fail, and yet it passes. This is due to both stack variable allocation (alloc) and malloc being modeled the same way, mainly setting the Alloc array entry to allocated. Stack variable allocation should probably not do that.

[zvonimir]

My proposed fix is to keep track of stack allocation in a separate map. So instead of having just $Alloc we should probably have $HeapAlloc and $StackAlloc maps. Thoughts @michael-emmi and @shaobo-he?

[michael-emmi]

Would DSA-region merging be a problem in that proposal, e.g., when some variable may alias both with some local and some heap location?

[zvonimir]

Bumping this up since I would like to fix it since I think it might simplify some of our memory models.

@michael-emmi I thought about your comment above. I am not sure if what you said is true since we will still end up using the same memory map for aliasing pointers. So I think it'll still work. Could you maybe come up with a counterexample if you disagree? That would be helpful. Thx!