Considering a valid pointer and an invalid pointer, should they be `\separated()`?

[zilbuz]

In the following examples with a valid pointer and an invalid pointer, should they be \separated()?

Example 1:

#include <stdlib.h>
int main() {
    int * a = malloc(sizeof(int));
    int * b = malloc(sizeof(int));
    free(a);
    if (b) {
        //@ assert !\valid(a);
        //@ assert \valid(b);

        //@ assert \separated(a, b); // ?
    }
    free(b);
    return 0;
}       

Example 2:

int * f() {
    int a = 0;
    return &a;
}
int main() {
    int * a = f();
    int b = 0;
    //@ assert !\valid(a);
    //@ assert \valid(&b);

    //@ assert \separated(a, &b); // ?
    return 0;
}

[yakobowski]

There is a subtlety here. IMO, a is not invalid here. Instead, the bit pattern at location a is dangling, meaning that it is not even a pointer. In particular, I would have said that //@ assert !\valid(a); is not provable.

What you can prove instead is //@assert \dangling(&a);. But notice that we are not speaking about the location pointed to by a; only of its bit-pattern. As this bit-pattern is not a pointer, applying \separated on it is meaningless, and your last assertion has no definitive truth value.

(I noticed that Eva proves //@ assert !\valid(a);. This contradicts parts of what I said above, but I stand by my analysis. Also, saying that uninitialized/dangling bit patterns are invalid is certainly more convenient for the user.

[zilbuz]

Thanks for the explanation.

How would you build an invalid pointer? Do you have to for instance build a pointer that's not correctly aligned according to its type?

And if one of the pointer is effectively invalid, does my question still stand? I guess that if my examples are not pointers, then an invalid pointer should still represent a memory location and a size, possibly inside allocated memory. If that's the case then I guess \separated() should be computed as usual, even if some pointers are invalid. What do you think?

[yakobowski]

How would you build an invalid pointer? Do you have to for instance build a pointer that's not correctly aligned according to its type?

Actually, ACSL has never specified what it means for a pointer to be correctly aligned. So you won't get an invalid pointer this way. But there are actually simpler approaches. Just do

int x;
int *p = &x + 1;

p is invalid here.

And if one of the pointer is effectively invalid, does my question still stand?

IMO, the answer is no. Consider

int x;
int *p = (int *)((char*)(&x) + 1);

p is invalid too. But p and &x are not separated.

If you rephrase your question as "one valid pointer and one valid, both well-aligned (whatever that means for the invalid one)", then I would be inclined to say the answer is yes. But since ACSL does not define well-aligned pointers, it will be hard to prove this theory...

I guess that if my examples are not pointers, then an invalid pointer should still represent a memory location and a size, possibly inside allocated memory.

Sure. But only on a low-level view of the memory, and ACSL makes sure to stay quite abstract. Between other things, this allows to use a memory model more precise than the one defined by ACSL, meaning that you can assign truth value True or False to properties that cannot be determined from the ACSL specification itself. This is what Eva does on the initial //@ assert !\valid(a); example. This is fine as long as you do not start using two plugins that make contradictory assumptions!

[vprevosto]

@yakobowski, interesting example. You're right, an invalid pointer (at least when sizeof(*p) > 1) can indeed point partially to allocated memory, so that it is not possible to automatically assume that it is separated from any valid pointer.