generate assert(false) when calling undefined function

This changes the symbolic execution engine to emit an assert(false) when
processing a call to a function without body, instead of merely emitting a
warning.

The key benefit is that undefined function bodies are a threat to soundness,
especially when CBMC is run without a human operator (say in CI) who might
spot the warning.  A common scenario is a call to a function that was
renamed, or whose signature has changed.  This scenario now triggers a
verification failure.

Users who prefer the previous, or other alternative behaviors, can achieve
this via program instrumentation, say using goto-instrument.

doc/man/cbmc.1

@@ -347,10 +347,6 @@ run full slicer (experimental)
 .TP
 \fB\-\-drop\-unused\-functions\fR
 drop functions trivially unreachable from main function
-.TP
-\fB\-\-havoc\-undefined\-functions\fR
-for any function that has no body, assign non\-deterministic values to
-any parameters passed as non\-const pointers and the return value
 .SS "Semantic transformations:"
 .TP
 \fB\-\-nondet\-static\fR

regression/cbmc-cpp/Overloading_Functions4/main.cpp

@@ -1,7 +1,9 @@
 double pow(double _X, double _Y);
 double pow(double _X, int _Y);
 float pow(float _X, float _Y);
-float pow(float _X, int _Y);
+float pow(float _X, int _Y)
+{
+}
 long double pow(long double _X, long double _Y);
 long double pow(long double _X, int _Y);
 

regression/cbmc-library/fprintf-01/__fprintf_chk.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=0$
@@ -7,3 +7,5 @@ main.c
 --
 ^\*\*\*\* WARNING: no body for function __fprintf_chk
 ^warning: ignoring
+--
+We are missing __builtin_va_arg_pack

regression/cbmc-library/printf-01/__printf_chk.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=10$
@@ -8,3 +8,5 @@ main.c
 --
 ^\*\*\*\* WARNING: no body for function __printf_chk
 ^warning: ignoring
+--
+We are missing __builtin_va_arg_pack

regression/cbmc-library/syslog-01/__syslog_chk.desc

@@ -1,9 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-^\*\*\*\* WARNING: no body for function __syslog_chk
 ^warning: ignoring
+--
+We are missing __builtin_va_arg_pack

regression/cbmc/Array_UF17/main.c

@@ -31,7 +31,9 @@ int istrchr(const char *s, int c);
 int istrrchr(const char *s, int c);
 int istrncmp(const char *s1, int start, const char *s2, size_t n);
 int istrstr(const char *haystack, const char *needle);
-char *r_strncpy(char *dest, const char *src, size_t n);
+char *r_strncpy(char *dest, const char *src, size_t n)
+{
+}
 char *r_strcpy(char *dest, const char *src);
 char *r_strcat(char *dest, const char *src);
 char *r_strncat(char *dest, const char *src, size_t n);

regression/cbmc/Function_Pointer5/main.c

@@ -1,7 +1,13 @@
 // this is a pointer to a function that takes a function pointer as argument
 
-void signal1(int, void (*)(int));
-void signal2(int, void (*h)(int));
+void signal1(int, void (*)(int))
+{
+}
+
+void signal2(int, void (*h)(int))
+{
+  h(123);
+}
 
 void handler(int x)
 {

regression/cbmc/Malloc2/main.c

@@ -1,4 +1,4 @@
-typedef unsigned int size_t;
+typedef __CPROVER_size_t size_t;
 typedef int ssize_t;
 typedef int atomic_t;
 typedef unsigned gfp_t;

regression/cbmc/Pointer28/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+KNOWNBUG no-new-smt
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/Promotion4/main.i

@@ -1,10 +1,12 @@
+unsigned nondet_unsigned();
+
 int main(int argc, char *argv[])
 {
   __CPROVER_assert(sizeof(unsigned int) == 2, "[--16] size of int is 16 bit");
   __CPROVER_assert(
     sizeof(unsigned long) == 4, "[--LP32] size of long is 32 bit");
 
-  unsigned int k = non_det_unsigned();
+  unsigned int k = nondet_unsigned();
   __CPROVER_assume(k < 1);
   __CPROVER_assert(k != 0xffff, "false counter example 16Bit?");
 

regression/cbmc/String_Abstraction11/anon-retval.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 char *foo()
 {

regression/cbmc/String_Abstraction19/structs.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 typedef struct str_struct
 {

regression/cbmc/Undefined_Function1/test.desc

@@ -1,9 +1,10 @@
 CORE
 main.c
 
+^\[main\.no-body\.f\] line 9 no body for callee f: FAILURE$
+^\[main\.assertion\.1] line 10 assertion i==1: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\*\*\*\* WARNING: no body for function f$
-^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/Undefined_Function2/test.desc

@@ -1,9 +1,10 @@
 CORE
 main.c
 
+^\[main\.no-body\.asd\] line 7 no body for callee asd: FAILURE$
+^\[main\.assertion\.1\] line 8 assertion v1==v2: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\*\*\*\* WARNING: no body for function asd$
-^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c

@@ -1,9 +1,11 @@
 #include <assert.h>
 #include <stdlib.h>
 
+_Bool nondet_bool();
+
 void main()
 {
   char *data;
-  data = nondet() ? malloc(1) : malloc(2);
+  data = nondet_bool() ? malloc(1) : malloc(2);
   assert(__CPROVER_OBJECT_SIZE(data) <= 2);
 }

regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc

@@ -4,9 +4,9 @@ short.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: SUCCESS
+^\[main\.assertion\.\d\] line \d+ assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: SUCCESS$
 --
-\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: FAILURE
+^\[main\.assertion\.\d\] line \d+ assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: FAILURE$
 --
 This is the reduced version of the issue described in
 https://github.com/diffblue/cbmc/issues/5952

regression/cbmc/memory_allocation2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$

regression/cbmc/pointer-overflow2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-overflow-check
 ^EXIT=0$

regression/cbmc/union12/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 
 ^EXIT=10$
@@ -15,3 +15,5 @@ possible. With 77236cc34 (Avoid nesting of ID_with/byte_update by rewriting
 byte_extract to use the root object) the test already is trivial, however.
 
 This test only fails when using SMT solvers as back-end on Windows.
+
+No body for __CPROVER_allocated_memory

regression/contracts/assigns_replace_02/main.c

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+void bar(int *)
+{
+}
+
 void foo(int *x, int *y) __CPROVER_assigns(*x)
 {
   *x = 7;

regression/contracts/cprover-assignable-pass/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 CALL __CPROVER_object_whole

regression/goto-instrument-wmm-core/CMakeLists.txt

@@ -4,6 +4,13 @@ else()
     set(is_windows false)
 endif()
 
+# These tests do not run with Visual Studio since they use
+# gcc's asm syntax.
+
+if(NOT WIN32)
+
 add_test_pl_tests(
     "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}" -X glpk
 )
+
+endif()

regression/goto-instrument-wmm-core/Makefile

@@ -1,15 +1,21 @@
+# These tests do not run with Visual Studio since they use
+# gcc's asm syntax.
+
 default: tests.log
 
 include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
-	exe=../../../src/goto-cc/goto-cl
-	is_windows=true
+
+test:
+
+tests.log: ../test.pl
+
 else
-	exe=../../../src/goto-cc/goto-cc
-	is_windows=false
-endif
+
+exe=../../../src/goto-cc/goto-cc
+is_windows=false
 
 testalpha:
 	@../test.pl -C -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
@@ -29,6 +35,8 @@ test:
 tests.log:
 	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
 
+endif
+
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
 	find . -name '*.gb' -execdir $(RM) '{}' \;

regression/goto-instrument/dump-vararg1/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --dump-c
 ^EXIT=0$
 ^SIGNAL=0$
 va_list
 --
 ^warning: ignoring
+--
+We are missing __CPROVER_va_start

regression/goto-instrument/inline_16/test.desc

@@ -1,12 +1,12 @@
 CORE
 main.c
 --inline
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 func1\(\)
 ret.*=.*func2\(\)
-no body for function.*func1
-no body for function.*func2
+^\[\.no-body\.func1\] file main.c line 3 no body for callee func1: FAILURE$
+^\[\.no-body\.func2\] file main.c line 3 no body for callee func2: FAILURE$
 --
 ^warning: ignoring

regression/goto-instrument/inline_17/test.desc

@@ -1,9 +1,10 @@
 CORE
 main.c
 --function-inline func1
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[func1\.no-body\.func2\] line 3 no body for callee func2: FAILURE$
+^VERIFICATION FAILED$
 func1\(\)
 func2\(\)
 --

regression/goto-instrument/remove-function-body1/test.desc

@@ -1,9 +1,11 @@
 CORE
 main.c
 --remove-function-body foo --remove-function-body bar
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[main\.no-body\.foo\] line 19 no body for callee foo: FAILURE$
+^\[main\.no-body\.bar\] line 20 no body for callee bar: FAILURE$
+^VERIFICATION FAILED$
 --
 ^warning: ignoring
 ^bar

src/ansi-c/library/syslog.c

@@ -21,6 +21,14 @@ void syslog(int priority, const char *format, ...)
   (void)*format;
 }
 
+/* FUNCTION: _syslog$DARWIN_EXTSN */
+
+void _syslog$DARWIN_EXTSN(int priority, const char *format, ...)
+{
+  (void)priority;
+  (void)*format;
+}
+
 /* FUNCTION: __syslog_chk */
 
 void __syslog_chk(int priority, int flag, const char *format, ...)

src/ansi-c/library_check.sh

@@ -15,6 +15,7 @@ for f in "$@"; do
     $CC -std=gnu11 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
     $CC -S -Wall -Werror -pedantic -Wextra -std=gnu11 __libcheck.i \
       -o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas \
+      -Wno-dollar-in-identifier-extension \
       -Wno-gnu-line-marker -Wno-unknown-warning-option -Wno-psabi
     ec="${?}"
     rm __libcheck.s __libcheck.i __libcheck.c
@@ -73,6 +74,7 @@ perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf-01/__fprintf_chk.desc
 perl -p -i -e 's/^__fread_chk\n//' __functions # fread-01/__fread_chk.desc
 perl -p -i -e 's/^__printf_chk\n//' __functions # printf-01/__printf_chk.desc
 perl -p -i -e 's/^__syslog_chk\n//' __functions # syslog-01/__syslog_chk.desc
+perl -p -i -e 's/^_syslog\$DARWIN_EXTSN\n//' __functions # syslog-01/test.desc
 perl -p -i -e 's/^__time64\n//' __functions # time
 perl -p -i -e 's/^__vfprintf_chk\n//' __functions # vfprintf-01/__vfprintf_chk.desc
 

src/cbmc/cbmc_parse_options.cpp

@@ -285,9 +285,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("drop-unused-functions"))
     options.set_option("drop-unused-functions", true);
 
-  if(cmdline.isset("havoc-undefined-functions"))
-    options.set_option("havoc-undefined-functions", true);
-
   if(cmdline.isset("string-abstraction"))
     options.set_option("string-abstraction", true);
 
@@ -1061,9 +1058,6 @@ void cbmc_parse_optionst::help()
     " {y--full-slice} \t run full slicer (experimental)\n"
     " {y--drop-unused-functions} \t drop functions trivially unreachable from"
     " main function\n"
-    " {y--havoc-undefined-functions} \t for any function that has no body,"
-    " assign non-deterministic values to any parameters passed as non-const"
-    " pointers and the return value\n"
     "\n"
     "Semantic transformations:\n"
     " {y--nondet-static} \t add nondeterministic initialization of variables"

src/cbmc/cbmc_parse_options.h

@@ -55,7 +55,6 @@ class optionst;
   OPT_SHOW_PROPERTIES \
   "(show-symbol-table)(show-parse-tree)" \
   "(drop-unused-functions)" \
-  "(havoc-undefined-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(verbosity):(no-library)" \
   "(nondet-static)" \