New function __VERIFIER_base_pointer

[gernst]

It would be nice to include a new function into the benchmark rules

void *__VERIFIER_base_pointer(void *ptr);

that denotes the base pointer of an object, similarly to __CPROVER_POINTER_OBJECT as supported by CBMC.

Example:

int *a[N];
unsigned i;
__VERIFIER_assume(0 <= i && i < N);
assert(__VERIFIER_base_pointer(a + i) == a);

The exact semantics need to be discussed, e.g. in relation to structs.

Use case: Some benchmarks in #817 use this feature.

[feliperodri]

Is there any discussion to include __VERIFIER_base_pointer in the competition rules? ESBMC is currently reporting wrong verification results in some cases of AWS C Common benchmarks due to the lack of implementation for this function. @dbeyer @tautschnig

[dbeyer]

Wasn't this issue solved by some recent pull request?

[feliperodri]

Wasn't this issue solved by some recent pull request?

@dbeyer PR #993 simply removed all the __VERIFIER_base_pointer calls, but I believe this issue will only be solved once we settle whether or not to include __VERIFIER_base_pointer into the benchmark rules, which I'm in favor.