introduces --havoc-undefined-function

If function body does not exist, we assume that any pointers passed to function may be written to
with a non-deterministic value, but only with something the size of the pointer type.

regression test for havoc_undefined_functions

Author: polgreen

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;
+}

regression/cbmc/havoc_undefined_functions/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--havoc-undefined-functions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

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"

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)" \

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;
   }
 }

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;
   }