From c08a090d255f5ac17da89f02bf2228478dc47986 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 27 May 2019 17:03:55 +0000
Subject: [PATCH] User-provided function definitions take precedence over
 built-ins

We should not replace calls to functions that have a body provided by
the user by our built-in definitions. While function names starting with
"_" are reserved in C and thus users shouldn't be using them, it is
certainly not true that anything named "nondet_*" is exclusively to be
captured by our built-ins.
---
 regression/cbmc/Function14/main.c       | 10 ++++++++++
 regression/cbmc/Function14/test.desc    |  8 ++++++++
 src/goto-programs/builtin_functions.cpp | 18 +++++++++++++++++-
 3 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/Function14/main.c
 create mode 100644 regression/cbmc/Function14/test.desc

diff --git a/regression/cbmc/Function14/main.c b/regression/cbmc/Function14/main.c
new file mode 100644
index 00000000000..cfcf14124cb
--- /dev/null
+++ b/regression/cbmc/Function14/main.c
@@ -0,0 +1,10 @@
+int nondet_foo()
+{
+  return 42;
+}
+
+int main()
+{
+  int x = nondet_foo();
+  __CPROVER_assert(x == 42, "nondet_foo returns a constant");
+}
diff --git a/regression/cbmc/Function14/test.desc b/regression/cbmc/Function14/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/Function14/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 3288690ab53..52ec4b497c6 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -647,6 +647,22 @@ void goto_convertt::do_function_call_symbol(
     throw 0;
   }
 
+  // User-provided function definitions always take precedence over built-ins.
+  // Front-ends do not (yet) consistently set ID_C_incomplete, thus also test
+  // whether the symbol actually has some non-nil value (which might be
+  // "compiled").
+  if(!symbol->type.get_bool(ID_C_incomplete) && symbol->value.is_not_nil())
+  {
+    do_function_call_symbol(*symbol);
+
+    code_function_callt function_call(lhs, function, arguments);
+    function_call.add_source_location() = function.source_location();
+
+    copy(function_call, FUNCTION_CALL, dest);
+
+    return;
+  }
+
   if(identifier==CPROVER_PREFIX "assume" ||
      identifier=="__VERIFIER_assume")
   {
@@ -702,7 +718,7 @@ void goto_convertt::do_function_call_symbol(
     a->source_location.set("user-provided", true);
   }
   else if(
-    identifier == "assert" && symbol->type.get_bool(ID_C_incomplete) &&
+    identifier == "assert" &&
     to_code_type(symbol->type).return_type() == signed_int_type())
   {
     if(arguments.size()!=1)