valid-memtrack analysis doesn't check sizes, only checks at end & doesn't consider locals

[sim642]

I started looking into allowing our SV-COMP valid-memtrack analysis to still consider one-past-end pointers to track memory for the rule change: https://gitlab.com/sosy-lab/sv-comp/bench-defs/-/merge_requests/471. However, I am really confused because the memLeak analysis we use for that doesn't seem to check sizes anywhere.

It looks like our valid-memtrack analysis is unsound. For example:

//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
#include <stdlib.h>

int main(int argc, char const *argv[]) {
    int *p = malloc(sizeof(int));
    p += 1; // NOWARN (valid-memtrack not yet violated because one-past-end)
    p -= 1;
    p += 2; // WARN (valid-memtrack violated)
    p -= 2;
    free(p);

    return 0; //NOWARN
}

We don't warn about anything on this program, but there is a point where the allocated memory has no pointer to it (or one past the end).