VerCors optimistically assumes malloc always succeeds in C

[wandernauta]

The following C program verifies:

#include <assert.h>
#include <stdlib.h>

int main() {
    int* ptr = (int*) malloc(sizeof(int)*1000000);
    assert(ptr != NULL);
    free(ptr);
}

However, malloc can fail, see e.g. section 7.22.3.4 in ref:

The malloc function returns either a null pointer or a pointer to the allocated space.

So the assertion doesn't necessarily hold (here on Linux, glibc):

$ ( ulimit -v 5000 ; ./malloc_optimism )
malloc_optimism: malloc_optimism.c:6: main: Assertion `ptr != NULL' failed.
Aborted (core dumped)

In #973, the @ensures clause was given as only promising a pointer to some memory if the result is non-NULL, but it appears that LangCToCol and the concepts/c/malloc_free.c example currently assume that allocation always succeeds.

---

This may be a known limitation, but it was surprising to me so I thought I'd report it here.

[superaxander]

True I'd been meaning to open an issue/document this somewhere since other verifiers such as frama-c and verifast don't make this assumption

[wandernauta]

Yeah. On desktop Linux, malloc really tries very hard not to hand you a NULL pointer (overcommit and such) but it will still do it.

It looks like something like the following could potentially work. If the AST stores whether the new pointer array is potentially NULL (fallible), either by...

• smuggling a boolean flag fallible into NewPointerArray, similar to the initialize flag on NewArray, or
• introducing a NewPointerArrayPerhapsMaybeNot expression or similiar, or
• some neater way

Then, in EncodeArrayValues, two variants of the make_pointer_array_ function could be emitted as needed, one with the current contract that has @ensures \result != NULL ** … and one with a more cautious contract that has @ensures \result != NULL ==> ….

The NewPointerArray node is only used by the C and C++ front-ends so PVL, Java etc would be unaffected. The malloc_free.c test case would need to be updated, of course.