false positives when --malloc-may-fail and --malloc-fail-null are used

[vmihalko]

CBMC version: 5.13.1
Operating system: Linux (Fedora rawhide)
Exact command line resulting in the issue: $ cbmc --pointer-check --malloc-may-fail --malloc-fail-null 0005-test.c
What behaviour did you expect: Detection of possible NULL dereference failure in following code and nothing else:

#include <stdlib.h>
 
int main(void)
{
    char *ptr = malloc(sizeof(char));
    *ptr = 'A'; /* error */
    free(ptr);
}

What happened instead:
CBMC also found some false positives: deallocated dynamic object, pointer outside object bounds, dead object. This false positives occurs also when calloc and realloc are used instead of malloc.

CBMC version 5.13.0 (cbmc-5.13.1) 64-bit x86_64 linux
Parsing 0005-test.c
Converting
Type-checking 0005-test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 129 steps
simple slicing removed 32 assignments
Generated 13 VCC(s), 10 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
933 variables, 1060 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.0113545s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
933 variables, 610 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.00145552s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
933 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime decision procedure: 0.000101401s
 
** Results:
0005-test.c function main
[main.pointer_dereference.1] line 6 dereference failure: pointer invalid in *ptr: SUCCESS
[main.pointer_dereference.2] line 6 dereference failure: pointer NULL in *ptr: FAILURE
[main.pointer_dereference.3] line 6 dereference failure: deallocated dynamic object in *ptr: FAILURE
[main.pointer_dereference.4] line 6 dereference failure: dead object in *ptr: FAILURE
[main.pointer_dereference.5] line 6 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[main.pointer_dereference.6] line 6 dereference failure: pointer outside object bounds in *ptr: FAILURE
[main.pointer_dereference.7] line 6 dereference failure: invalid integer address in *ptr: SUCCESS
[main.precondition_instance.1] line 7 free argument must be NULL or valid pointer: SUCCESS
[main.precondition_instance.2] line 7 free argument must be dynamic object: SUCCESS
[main.precondition_instance.3] line 7 free argument has offset zero: SUCCESS
[main.precondition_instance.4] line 7 double free: SUCCESS
[main.precondition_instance.5] line 7 free called for new[] object: SUCCESS
[main.precondition_instance.6] line 7 free called for stack-allocated object: SUCCESS
 
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS
 
** 4 of 15 failed (3 iterations)
VERIFICATION FAILED

[martin-cs]

@danpoe was working on this area in #5401 , maybe he has some insight into this?

[hannes-steffenhagen-diffblue]

This isn’t really a bug with malloc-may-fail, just a quirk of how these pointer checks are defined; Some cases for these just overlap.

Dereferencing a null pointer will always fail the deallocated check (i.e. null pointers are always considered deallocated), same with dead object, and it’s outside dynamic bounds (because the dynamic bounds for a null pointer are empty).

It’d be possible to make these checks not trigger for null pointers but I’m not sure how valuable that’d be?

[hannes-steffenhagen-diffblue]

Closing as this looks like expected behaviour to me.