DFCC instrumentation: skip unused functions

Do not attempt to instrument functions that will never be used anyway.
As we eventually use `remove_unused_functions` there is no point in
trying to instrument them, and there is a scenario where the function
may not have been compiled (see included test).

Author: tautschnig

regression/contracts-dfcc/skip_unused_instrumentation/main.c

@@ -0,0 +1,10 @@
+// Using a forward declaration rather than including netdb.h to make sure we do
+// not have the compiled body of functions from header files available right
+// away.
+struct hostent;
+struct hostent *gethostbyname(const char *name);
+
+int main()
+{
+  (void)gethostbyname("x");
+}

regression/contracts-dfcc/skip_unused_instrumentation/test.desc

@@ -0,0 +1,31 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that functions brought in from header files when loading
+entries from the model library are not subject to instrumentation (when those
+functions are never used). Else we end up with invariant failures like:
+[...]
+Instrumenting '__bswap_16'
+--- begin invariant violation report ---
+Invariant check failed
+File: /src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp:329 function: instrument_function
+Condition: Precondition
+Reason: found != goto_model.goto_functions.function_map.end()
+Backtrace:
+build/bin/goto-instrument(+0xbfe182) [0x649c3d22b182]
+[...]
+/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x78dc2f029d90]
+/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x78dc2f029e40]
+build/bin/goto-instrument(+0x363cb5) [0x649c3c990cb5]
+
+Diagnostics:
+<< EXTRA DIAGNOSTICS >>
+Function '__bswap_16' must exist in the model.
+<< END EXTRA DIAGNOSTICS >>
+
+--- end invariant violation report ---

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -257,6 +257,12 @@ void dfcct::partition_function_symbols(
   std::set<irep_idt> &contract_symbols,
   std::set<irep_idt> &other_symbols)
 {
+  std::set<irep_idt> called_functions;
+  find_used_functions(
+    goto_functionst::entry_point(),
+    goto_model.goto_functions,
+    called_functions);
+
   // collect contract and other symbols
   for(auto &entry : goto_model.symbol_table)
   {
@@ -272,7 +278,7 @@ void dfcct::partition_function_symbols(
     {
       contract_symbols.insert(sym_name);
     }
-    else
+    else if(called_functions.find(sym_name) != called_functions.end())
     {
       // it is not a contract
       other_symbols.insert(sym_name);