Merge pull request #5642 from tautschnig/fix-error-message

Print meaningful error message when trying to use undeclared uninterpreted functions

Author: NlightNFotis

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())