Test harnesses should mock unused functions

[sallaigy]

Consider the following code:

#include <assert.h>

int nondet1();
int nondet2();

int nevercalled() {
    return nondet2();
}

int main(void) {
    int x = nondet1();
    assert(x != 0);

    return 0;
}

The analysis produces a test harness which is incomplete and cannot be linked against the original program. This is due to the way the analysis works: as main is the entry point, nevercalled will never be executed and thus the nondeterministic call to nondet2 is not part of the counterexample, so it is not part of the trace. However, it should be part of the generated test harness, otherwise we will not be able to compile it and link it against the original program.