#include #include int main() { int *a = (int*)malloc(sizeof(int) * 10); $mem m = &a[1 .. 5]; for (int i = 0; i < 10; i++) a[i] = i; $mem_havoc(m); $assert(a[1] == 1); free(a); }