Incorrect region generation for ptrtoint/inttoptr arguments

[shaobo-he]

Consider this program,

#include "smack.h"
#include <stdint.h>

void foo(uint64_t p) {
    int* x = (int*)p;
    *x = 1;
}
int main(void) {
    int y = 0;
    foo((uint64_t)&y);
    assert(y == 1);
    return 0;
}

SMACK reports a spurious error. This is because x points to a different region than &y.

[shaobo-he]

Follow-up: this is because RemovePtrToIntPass eliminates the ptrtoint operation but not inttoptr as well. So we have only one complicated node.

[shaobo-he]

One solution is to inline foo manually.