diff --git a/regression/cbmc/havoc_undefined_functions/main.c b/regression/cbmc/havoc_undefined_functions/main.c
new file mode 100644
index 00000000000..b9ca953a211
--- /dev/null
+++ b/regression/cbmc/havoc_undefined_functions/main.c
@@ -0,0 +1,9 @@
+void function(int *a);
+
+int main()
+{
+  int a=0;
+  function(&a);
+  __CPROVER_assert(a==0,"");
+  return 0;
+}
\ No newline at end of file
diff --git a/regression/cbmc/havoc_undefined_functions/test.desc b/regression/cbmc/havoc_undefined_functions/test.desc
new file mode 100644
index 00000000000..914f6d7b486
--- /dev/null
+++ b/regression/cbmc/havoc_undefined_functions/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--havoc-undefined-functions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
\ No newline at end of file
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index cccea229ada..576154c3554 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -165,6 +165,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       cmdline.get_value("localize-faults-method"));
   }
 
+  if(cmdline.isset("havoc-undefined-functions"))
+    options.set_option("havoc-undefined-functions", true);
+
   if(cmdline.isset("unwind"))
     options.set_option("unwind", cmdline.get_value("unwind"));
 
@@ -995,6 +998,9 @@ void cbmc_parse_optionst::help()
     " --partial-loops              permit paths with partial loops\n"
     " --no-pretty-names            do not simplify identifiers\n"
     " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
+    " --havoc-undefined-functions\n"
+    "                              for any function that has no body, assign non-deterministic values to\n" // NOLINT(*)
+    "                              any parameters passed as non-const pointers and the return value\n" // NOLINT(*)
     "\n"
     "Backend options:\n"
     " --object-bits n              number of bits used for object addresses\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 4fd131422c6..da23991550a 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -52,6 +52,7 @@ class optionst;
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
   "(show-claims)(claim):(show-properties)" \
   "(drop-unused-functions)" \
+  "(havoc-undefined-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index 4a1c59096b5..861cffe925b 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -194,7 +194,13 @@ void symex_bmct::no_body(const irep_idt &identifier)
 {
   if(body_warnings.insert(identifier).second)
   {
-    warning() <<
-      "**** WARNING: no body for function " << identifier << eom;
+    warning() << "**** WARNING: no body for function " << identifier;
+
+    if(options.get_bool_option("havoc-undefined-functions"))
+    {
+      warning()
+          << "; assigning non-deterministic values to any pointer arguments";
+    }
+    warning() << eom;
   }
 }
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 0243f1487c2..1aefe901787 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -24,6 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/c_types.h>
 
+#include <pointer-analysis/dereference.h>
+
 #include <analyses/dirty.h>
 
 bool goto_symext::get_unwind_recursion(
@@ -276,6 +278,22 @@ void goto_symext::symex_function_call_code(
       symex_assign_rec(state, code);
     }
 
+    if(options.get_bool_option("havoc-undefined-functions"))
+    {
+      // assign non det to function arguments if pointers
+      // are not const
+      for(const auto &arg : call.arguments())
+      {
+        if(arg.type().id() == ID_pointer &&
+            !arg.type().subtype().get_bool(ID_C_constant))
+        {
+          exprt object = dereference_exprt(arg, arg.type().subtype());
+          clean_expr(object, state, true);
+          havoc_rec(state, guardt(), object);
+        }
+      }
+    }
+
     symex_transition(state);
     return;
   }