From c4ce19917cb89cbecec60adaac1abfc34660907b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 17 Jul 2026 10:50:39 +0000 Subject: [PATCH 1/2] C front-end: permit taking the address of built-in functions Referencing a built-in function outside a direct call, such as when taking its address, failed with "failed to find symbol" (CONVERSION ERROR) because only typecheck_side_effect_function_call would consult builtin_factory to add declarations of built-ins on demand. Also try builtin_factory when a symbol expression fails to resolve, so that code like 'void (*f)(int) = __builtin_exit;' type-checks. Direct calls to built-ins that CBMC rewrites into expressions are unaffected, as that rewriting happens for all calls irrespective of a symbol table entry. Calls via function pointers to built-ins without a library model continue to be flagged by the no-body checks. Fixes: https://github.com/diffblue/cbmc/issues/8811 Co-authored-by: Kiro --- .../ansi-c/gcc_builtins_address_of/main.c | 22 +++++++++++++++++++ .../ansi-c/gcc_builtins_address_of/test.desc | 8 +++++++ src/ansi-c/c_typecheck_expr.cpp | 12 +++++++--- 3 files changed, 39 insertions(+), 3 deletions(-) create mode 100644 regression/ansi-c/gcc_builtins_address_of/main.c create mode 100644 regression/ansi-c/gcc_builtins_address_of/test.desc diff --git a/regression/ansi-c/gcc_builtins_address_of/main.c b/regression/ansi-c/gcc_builtins_address_of/main.c new file mode 100644 index 00000000000..37af4a19fb5 --- /dev/null +++ b/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 diff --git a/regression/ansi-c/gcc_builtins_address_of/test.desc b/regression/ansi-c/gcc_builtins_address_of/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/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$ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 55a8cb69ef6..476611b8378 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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; From e8177e2887cdc5f3db3dbdc59ae8c4a83f43e460 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 17 Jul 2026 10:50:39 +0000 Subject: [PATCH 2/2] C library: add model for __builtin_exit GCC permits taking the address of __builtin_exit and calling it like a regular function. Model it like exit so that programs referencing __builtin_exit can be verified instead of failing the no-body check. Co-authored-by: Kiro --- regression/cbmc-library/__builtin_exit/main.c | 8 ++++++++ regression/cbmc-library/__builtin_exit/test.desc | 8 ++++++++ regression/cbmc/gcc_builtins_address_of/main.c | 11 +++++++++++ regression/cbmc/gcc_builtins_address_of/test.desc | 9 +++++++++ src/ansi-c/library/stdlib.c | 8 ++++++++ 5 files changed, 44 insertions(+) create mode 100644 regression/cbmc-library/__builtin_exit/main.c create mode 100644 regression/cbmc-library/__builtin_exit/test.desc create mode 100644 regression/cbmc/gcc_builtins_address_of/main.c create mode 100644 regression/cbmc/gcc_builtins_address_of/test.desc diff --git a/regression/cbmc-library/__builtin_exit/main.c b/regression/cbmc-library/__builtin_exit/main.c new file mode 100644 index 00000000000..97f30e97806 --- /dev/null +++ b/regression/cbmc-library/__builtin_exit/main.c @@ -0,0 +1,8 @@ +#include + +int main() +{ + __builtin_exit(0); + assert(0); + return 0; +} diff --git a/regression/cbmc-library/__builtin_exit/test.desc b/regression/cbmc-library/__builtin_exit/test.desc new file mode 100644 index 00000000000..28345e3383d --- /dev/null +++ b/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 diff --git a/regression/cbmc/gcc_builtins_address_of/main.c b/regression/cbmc/gcc_builtins_address_of/main.c new file mode 100644 index 00000000000..df93ed99d43 --- /dev/null +++ b/regression/cbmc/gcc_builtins_address_of/main.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + void (*f)(int) = __builtin_exit; + int (*g)(float) = __builtin_isnanf; + assert(!g(3.14f)); + f(1); + assert(0); + return 0; +} diff --git a/regression/cbmc/gcc_builtins_address_of/test.desc b/regression/cbmc/gcc_builtins_address_of/test.desc new file mode 100644 index 00000000000..f7efa2024df --- /dev/null +++ b/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$ diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index c82b495e256..bcfcd16f743 100644 --- a/src/ansi-c/library/stdlib.c +++ b/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