Strange behavior of __CPROVER_r_ok

[kenmcmil]

CBMC version: 5.15.0
Operating system:
Exact command line resulting in the issue: cbmc r_ok_unsound.c
What behaviour did you expect: verification failed
What happened instead: verification successful
r_ok_unsound.zip

The predicate __CPROVER_r_ok behaves strangely when the memory pointed to will be allocated in the future. Here is an example:

#include <stdbool.h>
#include <stdlib.h>


typedef struct node {
    struct node *next;
    int data;
} node_t;



int main() {
    node_t *p,*q;
    __CPROVER_assume(!__CPROVER_r_ok(p, 1));
    q = (node_t *)malloc(sizeof(node_t));
    __CPROVER_assert(p != q,"test");
}

CBMC proves this even though, obviously, p != q should not be provable, since p is uninitialized. It seems the reason is that __CPROVER_r_ok returns true when p happens to be equal to the address of the object that will be allocated at the next line. Is this the intended semantics? I guess you could argue that you shouldn't pass an invalid pointer to __CPROVER_r_ok, but it seems to me that for __CPROVER_r_ok to be useful in specifications, you should be able to pass it an invalid pointer and get the value false.

[tautschnig]

Hello Ken, Please see #5194 for an earlier discussion on this, and the documentation at http://cprover.diffblue.com/memory-primitives.html. In short, using __CPROVER_r_ok within __CPROVER_assume is only permissible when the pointer is guaranteed to be either null or valid (and running CBMC with --pointer-primitive-check will ensure this is the case).

This also implies that __CPROVER_r_ok is not to be used in preconditions.

[kenmcmil]

OK, thanks!

[hannes-steffenhagen-diffblue]

For some context, these primitives were never really meant for end users at all. They were mostly meant to be used by cbmcs own pointer and bounds checking. You can use them if you really want to, but you need to be very careful with them!

[hannes-steffenhagen-diffblue]

Seems like the question has been answered