Motivation for context-sensitive DSA/memory model

[shaobo-he]

I found a strong motivation for context-senstive DSA or memory model: when malloc is wrapped. Consider the following program,

#include <stdlib.h>

void* my_malloc(size_t size) {
  return malloc(size);
}

int main() {
  int* a = my_malloc(sizeof(int));
  int* b = my_malloc(sizeof(int));
  return *a != *b;
}

a and b points to disjoint objects while SMACK assigns the same memory region for them. This is because we use a context-insensitive DSA. In SV-COMP benchmarks, such a pattern is very common in the software system category.

[zvonimir]

There were pull requests and issues in the SeaDSA project that made me think that you can manually provide malloc wrappers to DSA. So we could potentially try to do that since there would be only a few.

[shaobo-he]

This issue also shows up in our implementation of rust box.

[shaobo-he]

Another example is strlen.