Print meaningful error message when trying to use undeclared uninterpreted functions

With 32715b4, the use of undeclared uninterpreted functions
resulted in an invariant failure. The commit introduced additional
sanity checking, but such failing such checks should still yield an
error message that is actionable by an end user.

Fixes: #5641

Author: tautschnig

regression/ansi-c/undeclared_function/undeclared_uninterpreted.desc

@@ -0,0 +1,11 @@
+CORE
+uninterpreted.c
+
+missing type information required to construct call to uninterpreted function
+^EXIT=70$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed$
+--
+Test to confirm that an actionable error message is provided.

regression/ansi-c/undeclared_function/uninterpreted.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main()
+{
+  int x;
+  assert(__CPROVER_uninterpreted_fn(x) == __CPROVER_uninterpreted_fn(x));
+  return 0;
+}
+
+int __CPROVER_uninterpreted_fn(int x);

src/goto-programs/builtin_functions.cpp

@@ -892,6 +892,15 @@ void goto_convertt::do_function_call_symbol(
     if(lhs.is_nil())
       return;
 
+    if(function.type().get_bool(ID_C_incomplete))
+    {
+      error().source_location = function.find_source_location();
+      error() << "'" << identifier << "' is not declared, "
+              << "missing type information required to construct call to "
+              << "uninterpreted function" << eom;
+      throw 0;
+    }
+
     const code_typet &function_call_type = to_code_type(function.type());
     mathematical_function_typet::domaint domain;
     for(const auto &parameter : function_call_type.parameters())