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

[vmihalko]

CBMC version: 5.14.3
Operating system: Linux (Fedora rawhide)
Exact command line resulting in the issue: $ cbmc --malloc-may-fail --malloc-fail-null test.c
What behaviour did you expect: VERIFICATION SUCCESSFUL - the following code is correct:

#include <stdlib.h>

int main(void) {
    void* ptr = malloc(sizeof(char));
    if (ptr == NULL)
        return 0;

    void* ptr1 = realloc(ptr, 2 * sizeof(char));
    if (ptr1 == NULL) {
        free(ptr);
        return 0;
    }

    free(ptr1);
}

What happened instead:

CBMC version 5.14.3 (cbmc-5.14.3-13-g2bc93c24e) 64-bit x86_64 linux
Parsing testhis.c
Converting
Type-checking testhis
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: 252 steps
simple slicing removed 39 assignments
Generated 19 VCC(s), 12 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
1251 variables, 1635 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.0236582s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
1251 variables, 683 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 0.00160593s

** Results:
<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

<builtin-library-realloc> function realloc
[realloc.precondition_instance.1] line 20 free argument must be NULL or valid pointer: SUCCESS
[realloc.precondition_instance.2] line 20 free argument must be dynamic object: SUCCESS
[realloc.precondition_instance.3] line 20 free argument has offset zero: SUCCESS
[realloc.precondition_instance.4] line 20 double free: SUCCESS
[realloc.precondition_instance.5] line 20 free called for new[] object: SUCCESS
[realloc.precondition_instance.6] line 20 free called for stack-allocated object: SUCCESS
[realloc.precondition_instance.7] line 29 free argument must be NULL or valid pointer: SUCCESS
[realloc.precondition_instance.8] line 29 free argument must be dynamic object: SUCCESS
[realloc.precondition_instance.9] line 29 free argument has offset zero: SUCCESS
[realloc.precondition_instance.10] line 29 double free: SUCCESS
[realloc.precondition_instance.11] line 29 free called for new[] object: SUCCESS
[realloc.precondition_instance.12] line 29 free called for stack-allocated object: SUCCESS

testhis.c function main
[main.precondition_instance.1] line 8 realloc argument is dynamic object: SUCCESS
[main.precondition_instance.2] line 10 free argument must be NULL or valid pointer: FAILURE
[main.precondition_instance.3] line 10 free argument must be dynamic object: SUCCESS
[main.precondition_instance.4] line 10 free argument has offset zero: SUCCESS
[main.precondition_instance.5] line 10 double free: FAILURE
[main.precondition_instance.6] line 10 free called for new[] object: SUCCESS
[main.precondition_instance.7] line 10 free called for stack-allocated object: SUCCESS
[main.precondition_instance.8] line 14 free argument must be NULL or valid pointer: SUCCESS
[main.precondition_instance.9] line 14 free argument must be dynamic object: SUCCESS
[main.precondition_instance.10] line 14 free argument has offset zero: SUCCESS
[main.precondition_instance.11] line 14 double free: SUCCESS
[main.precondition_instance.12] line 14 free called for new[] object: SUCCESS
[main.precondition_instance.13] line 14 free called for stack-allocated object: SUCCESS

** 2 of 27 failed (2 iterations)
VERIFICATION FAILED

[martin-cs]

Thanks for reporting this. I am going to page @hannes-steffenhagen-diffblue and @danpoe as I know they have been working on this area.

[hannes-steffenhagen-diffblue]

Yes, this is basically a parenthesis error that snuck in when we added the --malloc-may-fail flag, I'll go fix it. Sorry about that one!