Skip to content

Link errors on NetBSD (undefined reference to ...) #9088

Description

@alnsn

Summary

Version 6.10.0 (latest at the time of writing) doesn't link bin/cbmc on NetBSD/amd64 10.1. It builds all other binaries fine.

Details

First, you need to apply the following patch:

--- src/ansi-c/library/stdio.c.orig     2026-04-14 18:24:47.000000000 +0000
+++ src/ansi-c/library/stdio.c
@@ -7,7 +7,7 @@
 #endif

 /* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
-#if defined(__OpenBSD__)
+#if defined(__OpenBSD__) || defined(__FreeBSD__) || defined(__NetBSD__)
 #undef getchar
 #undef putchar
 #undef getc
@@ -373,7 +373,11 @@ __CPROVER_HIDE:;
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 int __VERIFIER_nondet_int(void);

+#if defined(__NetBSD__)
+char *__fgets_chk(char *str, int size, __CPROVER_size_t bufsize, FILE *stream)
+#else
 char *__fgets_chk(char *str, __CPROVER_size_t bufsize, int size, FILE *stream)
+#endif
 {
 __CPROVER_HIDE:;
   (void)bufsize;

Then build with -DWITH_JBMC=OFF.

Build Log

[ 79%] Linking CXX executable ../../bin/cbmc
[ 80%] Built target goto-bmc
[ 81%] Built target lib-unit
[ 81%] Built target api-binary-driver
[100%] Built target unit
ld: ../../lib/libbig-int.a(bigint.cc.o): in function `BigInt::as_string(char*, unsigned int, unsigned int) const':
bigint.cc:(.text+0x99f): warning: Warning: reference to the libc supplied alloca(3); this most likely will not work. Please use the compiler provided version of alloca(3), by supplying the appropriate compiler flags (e.g. -std=gnu99).
ld: ../../lib/libansi-c.a(goto_check_c.cpp.o): in function `goto_check_ct::get_pointer_is_null_condition(exprt const&, exprt const&)':
goto_check_c.cpp:(.text+0x9e2d): undefined reference to `local_bitvector_analysist::get(std::_List_const_iterator<goto_programt::instructiont>, exprt const&)'
ld: ../../lib/libansi-c.a(goto_check_c.cpp.o): in function `goto_check_ct::get_pointer_points_to_valid_memory_conditions[abi:cxx11](exprt const&, exprt const&)':
goto_check_c.cpp:(.text+0xa1b4): undefined reference to `local_bitvector_analysist::get(std::_List_const_iterator<goto_programt::instructiont>, exprt const&)'
ld: ../../lib/libansi-c.a(goto_check_c.cpp.o): in function `local_bitvector_analysist::local_bitvector_analysist(goto_functiont const&, namespacet const&)':
goto_check_c.cpp:(.text._ZN25local_bitvector_analysistC2ERK14goto_functiontRK10namespacet[_ZN25local_bitvector_analysistC5ERK14goto_functiontRK10namespacet]+0x9e): undefined reference to `localst::build(goto_functiont const&)'
ld: goto_check_c.cpp:(.text._ZN25local_bitvector_analysistC2ERK14goto_functiontRK10namespacet[_ZN25local_bitvector_analysistC5ERK14goto_functiontRK10namespacet]+0x103): undefined reference to `local_cfgt::build(goto_programt const&)'
ld: goto_check_c.cpp:(.text._ZN25local_bitvector_analysistC2ERK14goto_functiontRK10namespacet[_ZN25local_bitvector_analysistC5ERK14goto_functiontRK10namespacet]+0x1a3): undefined reference to `local_bitvector_analysist::build()'
gmake[2]: *** [src/cbmc/CMakeFiles/cbmc.dir/build.make:127: bin/cbmc] Error 1
gmake[1]: *** [CMakeFiles/Makefile2:3264: src/cbmc/CMakeFiles/cbmc.dir/all] Error 2
gmake: *** [Makefile:166: all] Error 2
*** Error code 2

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions