overspecificity in state view giving false negatives

[akiarie]

#include <stdlib.h>

void
f() ~ [ return malloc(1); ]
{
    void *p;

    p = malloc(1);
    free(p);
    p = malloc(1);
    return p;
}

This is currently rejected on account of the second-allocation appearing as heap:1, whereas the one in the abstract is heap:0. There are many other ways to trigger this kind of issue. More succinctly:

#include <stdlib.h>

void
f() ~ [ return malloc(1); ]
{
    free(malloc(1));
    return malloc(1);
}

[akiarie]

Possible solutions:

• non string-based state comparisons (seems like a bad idea)
• deterministic renumbering that would reassign locations in a way that eliminates the variance

[claude-betz]

Agree with not going with the first.

The second makes sense. So an update that runs on the axiomatic free and goes through every value in every object and block.. seems a bit involved.