goto-harness results in `no body for function 'free'`

[archigup]

We get an error from goto-instrument when using a harness generated by goto-harness.

For example:

Take the following C file as test.c:

#include <assert.h>

void test_fn(int *a)
__CPROVER_requires((a == nullptr) || __CPROVER_is_fresh(a, sizeof(*a)))
__CPROVER_requires((a != nullptr) ==> (*a != 5))
__CPROVER_ensures((a != nullptr) ==> (*a == 5))
__CPROVER_assigns(*a)
{
    assert((a == nullptr) || (*a != 5));
    if (a != nullptr) {
        *a = 5;
    }
}

This contract should pass validation.

When trying to generate the harness and instrument the goto, we get:

$ goto-cc -std=c23 -o test.goto test.c
$ goto-harness --harness-function-name main --harness-type call-function --function test_fn test.goto test.goto
$ goto-instrument --dfcc main --enforce-contract test_fn test.goto test.goto
Reading GOTO program from 'test.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
file <builtin-library-__CPROVER_contracts_library> line 1077 function __CPROVER_contracts_write_set_deallocate_freeable: no body for function 'free'
No body for 'free' during inlining
Numeric exception : 0
6$ 

We are able to prove the contract passes if using the following manual harness:

int main(void) {
  int * a;
  test_fn(a);
}

[tautschnig]

Thank you for the detailed report and test case. Please see #8684 for the candidate fix.

[archigup]

I built commit f06afc4 and tried again but still get an error (though a new one):

$ cat test.c 
#include <assert.h>
#include <stddef.h>

void test_fn(int *a)
__CPROVER_requires((a == NULL) || __CPROVER_is_fresh(a, sizeof(*a)))
__CPROVER_requires((a != NULL) ==> (*a != 5))
__CPROVER_ensures((a != NULL) ==> (*a == 5))
__CPROVER_assigns(*a)
{
    assert((a == NULL) || (*a != 5));
    if (a != NULL) {
        *a = 5;
    }
}

$ goto-cc -o test.goto test.c
$ goto-harness --harness-function-name main --harness-type call-function --function test_fn test.goto test.goto
$ goto-instrument --dfcc main --enforce-contract test_fn test.goto test.goto
Reading GOTO program from 'test.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'main'
Wrapping 'test_fn' with contract 'test_fn' in CHECK mode
no body for function '__CPROVER_assignable'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 1 targets
Removing unused functions
generate function bodies: No function name matched regex
Updating init function
--- begin invariant violation report ---
Invariant check failed
File: /build/source/src/goto-instrument/nondet_static.cpp:90 function: nondet_static
Condition: fct_entry != goto_model.goto_functions.function_map.end()
Reason: Check return value
Backtrace:
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xe78073]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xe79189]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x5642cd]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x5cecc5]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x5cff2a]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x684cfb]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x6858e1]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x685cb1]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x685f83]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x56ec87]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x56fa14]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x56299a]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x558a44]
/nix/store/q4wq65gl3r8fy746v9bbwgx4gzn0r2kl-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x726681e2a4d8]
/nix/store/q4wq65gl3r8fy746v9bbwgx4gzn0r2kl-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x726681e2a59b]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x563955]


--- end invariant violation report ---
aborted
6$ 

[tautschnig]

To fix the additional error that you saw you need to make sure you do a linking step after running goto-harness: run goto-cc --function main test.goto -o test.goto.