C front-end: permit taking the address of built-in functions

regression/ansi-c/gcc_builtins_address_of/main.c

@@ -0,0 +1,22 @@
+#ifdef __GNUC__
+
+int main()
+{
+  void (*f)(int) = __builtin_exit;
+  int (*g)(float) = __builtin_isnanf;
+  int (*h)(int) = __builtin_ffs;
+  void *(*m)(__SIZE_TYPE__) = __builtin_malloc;
+  void *(*c)(void *, const void *, __SIZE_TYPE__) = __builtin_memcpy;
+  (void)g(3.14f);
+  (void)h(42);
+  f(1);
+  return 0;
+}
+
+#else
+
+int main()
+{
+}
+
+#endif

regression/ansi-c/gcc_builtins_address_of/test.desc

@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc-library/__builtin_exit/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  __builtin_exit(0);
+  assert(0);
+  return 0;
+}

regression/cbmc-library/__builtin_exit/test.desc

@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/gcc_builtins_address_of/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  void (*f)(int) = __builtin_exit;
+  int (*g)(float) = __builtin_isnanf;
+  assert(!g(3.14f));
+  f(1);
+  assert(0);
+  return 0;
+}

regression/cbmc/gcc_builtins_address_of/test.desc

@@ -0,0 +1,9 @@
+CORE gcc-only
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/c_typecheck_expr.cpp

@@ -884,9 +884,15 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
   const symbolt *symbol_ptr;
   if(lookup(identifier, symbol_ptr))
   {
-    error().source_location = expr.source_location();
-    error() << "failed to find symbol '" << identifier << "'" << eom;
-    throw 0;
+    // If this is a built-in, try to add it to the symbol table on the fly,
+    // just like we do for function calls (see
+    // typecheck_side_effect_function_call).
+    if(builtin_factory(identifier) || lookup(identifier, symbol_ptr))
+    {
+      error().source_location = expr.source_location();
+      error() << "failed to find symbol '" << identifier << "'" << eom;
+      throw 0;
+    }
   }
 
   const symbolt &symbol=*symbol_ptr;

src/ansi-c/library/stdlib.c

@@ -108,6 +108,14 @@ void exit(int status)
 #endif
 }
 
+/* FUNCTION: __builtin_exit */
+
+void __builtin_exit(int status)
+{
+  (void)status;
+  __CPROVER_assume(0);
+}
+
 /* FUNCTION: _Exit */
 
 #undef _Exit