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.

Author: kroening

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?");