head	1.1;
access;
symbols;
locks; strict;
comment	@ * @;


1.1
date	2026.10.17.16.55.46;	author alnsn;	state Exp;
branches;
next	;
commitid	CknMhgn24aCkRQZG;


desc
@@


1.1
log
@Initial import of devel/cbmc version 6.10.0.

CBMC is a Bounded Model Checker for C and C++ programs. It supports
C89, C99, most of C11, C17, C23 and most compiler extensions provided
by gcc and Visual Studio. It also supports SystemC using Scoot. It
allows verifying array bounds (buffer overflows), pointer safety,
exceptions and user-specified assertions. Furthermore, it can check
C and C++ for consistency with other languages, such as Verilog.
The verification is performed by unwinding the loops in the program
and passing the resulting equation to a decision procedure.
@
text
@$NetBSD$

Undefine problematic macros.

--- 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;
@