`goto-instrument` fails if code unrelated to harness contains `free`

[hanno-becker]

Example:

#include <stdlib.h>
void foo(void *p) { free(p); }
void harness(void) { int x = 42; }

Instructions:

goto-cc test.c --function harness -o a.out
goto-instrument --dfcc harness a.out b.out

Fails with:

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

[tautschnig]

It seems the problem is that on the one side we only consider reachable functions when loading library functions, but then still need the library function for contracts instrumentation. I'll work on a fix.

[hanno-becker]

@tautschnig Thank you 🙏 Can you elaborate a bit more, I don't yet follow: We don't have a contract here that involves (directly or indirectly) malloc/free?