git: 2a9a7b3cc92e - main - devel/cbmc: update to 6.9.0
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Sat, 20 Jun 2026 16:23:54 UTC
The branch main has been updated by olivier:
URL: https://cgit.FreeBSD.org/ports/commit/?id=2a9a7b3cc92e0ea7ba5b51a50be0f0c29e410f48
commit 2a9a7b3cc92e0ea7ba5b51a50be0f0c29e410f48
Author: Olivier Cochard <olivier@FreeBSD.org>
AuthorDate: 2026-06-20 16:19:10 +0000
Commit: Olivier Cochard <olivier@FreeBSD.org>
CommitDate: 2026-06-20 16:22:44 +0000
devel/cbmc: update to 6.9.0
Reported by: lwhsu
---
devel/cbmc/Makefile | 2 +-
devel/cbmc/distinfo | 6 +-
devel/cbmc/files/patch-libc19 | 171 -----------
...tch-src_solvers_flattening_boolbv__overflow.cpp | 28 --
...rs_smt2__incremental_convert__expr__to__smt.cpp | 37 ---
devel/cbmc/files/patch-stdio-models-freebsd | 315 ---------------------
6 files changed, 4 insertions(+), 555 deletions(-)
diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile
index 28f926218b10..0743231deea4 100644
--- a/devel/cbmc/Makefile
+++ b/devel/cbmc/Makefile
@@ -1,5 +1,5 @@
PORTNAME= cbmc
-PORTVERSION= 6.4.1
+PORTVERSION= 6.9.0
DISTVERSIONPREFIX= cbmc-
CATEGORIES= devel
MASTER_SITES= DEBIAN/pool/main/m/minisat2:minisat
diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo
index 36f820a95e09..169a9728240a 100644
--- a/devel/cbmc/distinfo
+++ b/devel/cbmc/distinfo
@@ -1,5 +1,5 @@
-TIMESTAMP = 1736265016
+TIMESTAMP = 1781965816
SHA256 (minisat2_2.2.1.orig.tar.gz) = e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40
SIZE (minisat2_2.2.1.orig.tar.gz) = 44229
-SHA256 (diffblue-cbmc-cbmc-6.4.1_GH0.tar.gz) = 09507765190bd14d07452b68003087160c80325b251a6f13d50845bb5f44ae7e
-SIZE (diffblue-cbmc-cbmc-6.4.1_GH0.tar.gz) = 9127951
+SHA256 (diffblue-cbmc-cbmc-6.9.0_GH0.tar.gz) = 05bb5719273edba6e01842dfbc63349fc38f6774bd39074887e1fcec867c92ca
+SIZE (diffblue-cbmc-cbmc-6.9.0_GH0.tar.gz) = 9239653
diff --git a/devel/cbmc/files/patch-libc19 b/devel/cbmc/files/patch-libc19
deleted file mode 100644
index d90dd36c26e3..000000000000
--- a/devel/cbmc/files/patch-libc19
+++ /dev/null
@@ -1,171 +0,0 @@
-From 6ba37b383990f1542005fc252bcd3030c477d8ba Mon Sep 17 00:00:00 2001
-From: Sergei Zimmerman <145775305+xokdvium@users.noreply.github.com>
-Date: Mon, 6 Jan 2025 19:13:29 +0300
-Subject: [PATCH] util: Replace std::basic_string<unsigned> with
- std::basic_string<char32_t>
-
-Fixes build with libc++19 that fails with the error:
-
-> implicit instantiation of undefined template 'std::char_traits<unsigned int>'
-
-Motivation for the change: std::basic_string<T> requires that
-T implements std::char_traits and standard library provides specializations only
-for the following types: char, char16_t, char32_t, wchar_t as per [1].
-
-Note that this has been pointed out during a review previously [2], but made its
-way back into the code in other places.
-
-libc++19 has dropped implementations of std::char_traits for types not required
-by the standard [3].
-
-> The base template for std::char_traits has been removed in LLVM 19.
-> If you are using std::char_traits with types other than char, wchar_t, char8_t, char16_t, char32_t
-> or a custom character type for which you specialized std::char_traits, your code will stop working.
-
-[1] N4713, 24.2.1 Character traits [char.traits] (C++17)
-[2] https://www.github.com/diffblue/cbmc/pull/5277#discussion_r396609205
-[3] https://libcxx.llvm.org/ReleaseNotes/19.html#deprecations-and-removals
---- src/ansi-c/literals/convert_character_literal.cpp.orig 2024-11-28 20:55:26 UTC
-+++ src/ansi-c/literals/convert_character_literal.cpp
-@@ -32,7 +32,7 @@ exprt convert_character_literal(
- PRECONDITION(src[1] == '\'');
- PRECONDITION(src[src.size() - 1] == '\'');
-
-- std::basic_string<unsigned int> value=
-+ std::basic_string<char32_t> value=
- unescape_wide_string(std::string(src, 2, src.size()-3));
- // the parser rejects empty character constants
- CHECK_RETURN(!value.empty());
- src/ansi-c/literals/convert_character_literal.cpp | 2 +-
- src/ansi-c/literals/convert_string_literal.cpp | 10 +++++-----
- src/ansi-c/literals/unescape_string.cpp | 8 ++++----
- src/ansi-c/literals/unescape_string.h | 2 +-
- src/ansi-c/scanner.l | 2 +-
- src/util/unicode.cpp | 2 +-
- src/util/unicode.h | 2 +-
- 7 files changed, 14 insertions(+), 14 deletions(-)
-
---- src/ansi-c/literals/convert_string_literal.cpp.orig 2024-11-28 20:55:26 UTC
-+++ src/ansi-c/literals/convert_string_literal.cpp
-@@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
-
- #include "unescape_string.h"
-
--std::basic_string<unsigned int> convert_one_string_literal(
-+std::basic_string<char32_t> convert_one_string_literal(
- const std::string &src)
- {
- PRECONDITION(src.size() >= 2);
-@@ -28,7 +28,7 @@ std::basic_string<unsigned int> convert_one_string_lit
- PRECONDITION(src[src.size() - 1] == '"');
- PRECONDITION(src[2] == '"');
-
-- std::basic_string<unsigned int> value=
-+ std::basic_string<char32_t> value=
- unescape_wide_string(std::string(src, 3, src.size()-4));
-
- // turn into utf-8
-@@ -57,7 +57,7 @@ std::basic_string<unsigned int> convert_one_string_lit
- unescape_string(std::string(src, 1, src.size()-2));
-
- // pad into wide string
-- std::basic_string<unsigned int> value;
-+ std::basic_string<char32_t> value;
- value.resize(char_value.size());
- for(std::size_t i=0; i<char_value.size(); i++)
- value[i]=char_value[i];
-@@ -72,7 +72,7 @@ exprt convert_string_literal(const std::string &src)
- // e.g., something like "asd" "xyz".
- // GCC allows "asd" L"xyz"!
-
-- std::basic_string<unsigned int> value;
-+ std::basic_string<char32_t> value;
-
- char wide=0;
-
-@@ -101,7 +101,7 @@ exprt convert_string_literal(const std::string &src)
- INVARIANT(j < src.size(), "non-terminated string constant '" + src + "'");
-
- std::string tmp_src=std::string(src, i, j-i+1);
-- std::basic_string<unsigned int> tmp_value=
-+ std::basic_string<char32_t> tmp_value=
- convert_one_string_literal(tmp_src);
- value.append(tmp_value);
- i=j;
---- src/ansi-c/literals/unescape_string.cpp.orig 2024-11-28 20:55:26 UTC
-+++ src/ansi-c/literals/unescape_string.cpp
-@@ -20,7 +20,7 @@ static void append_universal_char(
- unsigned int value,
- std::string &dest)
- {
-- std::basic_string<unsigned int> value_str(1, value);
-+ std::basic_string<char32_t> value_str(1, value);
-
- // turn into utf-8
- const std::string utf8_value = utf32_native_endian_to_utf8(value_str);
-@@ -30,7 +30,7 @@ static void append_universal_char(
-
- static void append_universal_char(
- unsigned int value,
-- std::basic_string<unsigned int> &dest)
-+ std::basic_string<char32_t> &dest)
- {
- dest.push_back(value);
- }
-@@ -153,10 +153,10 @@ std::string unescape_string(const std::string &src)
- return unescape_string_templ<char>(src);
- }
-
--std::basic_string<unsigned int> unescape_wide_string(
-+std::basic_string<char32_t> unescape_wide_string(
- const std::string &src)
- {
-- return unescape_string_templ<unsigned int>(src);
-+ return unescape_string_templ<char32_t>(src);
- }
-
- unsigned hex_to_unsigned(const char *hex, std::size_t digits)
---- src/ansi-c/literals/unescape_string.h.orig 2024-11-28 20:55:26 UTC
-+++ src/ansi-c/literals/unescape_string.h
-@@ -15,7 +15,7 @@ std::string unescape_string(const std::string &);
- #include <string>
-
- std::string unescape_string(const std::string &);
--std::basic_string<unsigned int> unescape_wide_string(const std::string &);
-+std::basic_string<char32_t> unescape_wide_string(const std::string &);
-
- unsigned hex_to_unsigned(const char *, std::size_t digits);
- unsigned octal_to_unsigned(const char *, std::size_t digits);
---- src/ansi-c/scanner.l.orig 2024-11-28 20:55:26 UTC
-+++ src/ansi-c/scanner.l
-@@ -89,7 +89,7 @@ int make_identifier()
- for(; *p!=0 && digits>0; digits--, p++);
- p--; // go back for p++ later
-
-- std::basic_string<unsigned> utf32;
-+ std::basic_string<char32_t> utf32;
- utf32+=letter;
-
- // turn into utf-8
---- src/util/unicode.cpp.orig 2024-11-28 20:55:26 UTC
-+++ src/util/unicode.cpp
-@@ -134,7 +134,7 @@ std::string
- /// \param s: UTF-32 encoded wide string
- /// \return utf8-encoded string with the same unicode characters as the input.
- std::string
--utf32_native_endian_to_utf8(const std::basic_string<unsigned int> &s)
-+utf32_native_endian_to_utf8(const std::basic_string<char32_t> &s)
- {
- std::string result;
-
---- src/util/unicode.h.orig 2024-11-28 20:55:26 UTC
-+++ src/util/unicode.h
-@@ -29,7 +29,7 @@ std::string
- #endif
-
- std::string
--utf32_native_endian_to_utf8(const std::basic_string<unsigned int> &s);
-+utf32_native_endian_to_utf8(const std::basic_string<char32_t> &s);
-
- /// \param utf8_str: UTF-8 string
- /// \return UTF-32 encoding of the string
diff --git a/devel/cbmc/files/patch-src_solvers_flattening_boolbv__overflow.cpp b/devel/cbmc/files/patch-src_solvers_flattening_boolbv__overflow.cpp
deleted file mode 100644
index 465a2fe8aac6..000000000000
--- a/devel/cbmc/files/patch-src_solvers_flattening_boolbv__overflow.cpp
+++ /dev/null
@@ -1,28 +0,0 @@
---- src/solvers/flattening/boolbv_overflow.cpp.orig 2025-01-07 17:20:50 UTC
-+++ src/solvers/flattening/boolbv_overflow.cpp
-@@ -126,14 +126,14 @@ literalt boolbvt::convert_binary_overflow(const binary
- : bv_utilst::representationt::UNSIGNED;
-
- if(
-- const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
-+ [[maybe_unused]] const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
- {
- if(bv0.size() != bv1.size())
- return SUB::convert_rest(expr);
-
- return bv_utils.overflow_add(bv0, bv1, rep);
- }
-- if(const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
-+ if([[maybe_unused]] const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
- {
- if(bv0.size() != bv1.size())
- return SUB::convert_rest(expr);
-@@ -159,7 +159,7 @@ literalt boolbvt::convert_binary_overflow(const binary
- return mult_overflow_result(prop, bv0, bv1, rep).back();
- }
- else if(
-- const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
-+ [[maybe_unused]] const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
- {
- DATA_INVARIANT(!bv0.empty(), "zero-sized operand");
-
diff --git a/devel/cbmc/files/patch-src_solvers_smt2__incremental_convert__expr__to__smt.cpp b/devel/cbmc/files/patch-src_solvers_smt2__incremental_convert__expr__to__smt.cpp
deleted file mode 100644
index f146dee4a4fc..000000000000
--- a/devel/cbmc/files/patch-src_solvers_smt2__incremental_convert__expr__to__smt.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
---- src/solvers/smt2_incremental/convert_expr_to_smt.cpp.orig 2025-01-07 17:23:07 UTC
-+++ src/solvers/smt2_incremental/convert_expr_to_smt.cpp
-@@ -175,14 +175,14 @@ static smt_termt make_bitvector_resize_cast(
- const bitvector_typet &from_type,
- const bitvector_typet &to_type)
- {
-- if(const auto to_fixedbv_type = type_try_dynamic_cast<fixedbv_typet>(to_type))
-+ if([[maybe_unused]] const auto to_fixedbv_type = type_try_dynamic_cast<fixedbv_typet>(to_type))
- {
- UNIMPLEMENTED_FEATURE(
- "Generation of SMT formula for type cast to fixed-point bitvector "
- "type: " +
- to_type.pretty());
- }
-- if(const auto to_floatbv_type = type_try_dynamic_cast<floatbv_typet>(to_type))
-+ if([[maybe_unused]] const auto to_floatbv_type = type_try_dynamic_cast<floatbv_typet>(to_type))
- {
- UNIMPLEMENTED_FEATURE(
- "Generation of SMT formula for type cast to floating-point bitvector "
-@@ -258,7 +258,7 @@ static smt_termt convert_expr_to_smt(
- const auto &from_term = converted.at(cast.op());
- const typet &from_type = cast.op().type();
- const typet &to_type = cast.type();
-- if(const auto bool_type = type_try_dynamic_cast<bool_typet>(to_type))
-+ if([[maybe_unused]] const auto bool_type = type_try_dynamic_cast<bool_typet>(to_type))
- return make_not_zero(from_term, cast.op().type());
- if(const auto c_bool_type = type_try_dynamic_cast<c_bool_typet>(to_type))
- return convert_c_bool_cast(from_term, from_type, *c_bool_type);
-@@ -894,7 +894,7 @@ static smt_termt convert_expr_to_smt(
- "encoding.");
- const size_t offset_bits = type->get_width() - object_bits;
- if(
-- const auto symbol =
-+ [[maybe_unused]] const auto symbol =
- expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
- {
- const smt_bit_vector_constant_termt offset{0, offset_bits};
diff --git a/devel/cbmc/files/patch-stdio-models-freebsd b/devel/cbmc/files/patch-stdio-models-freebsd
deleted file mode 100644
index bf9b3d6fe6b8..000000000000
--- a/devel/cbmc/files/patch-stdio-models-freebsd
+++ /dev/null
@@ -1,315 +0,0 @@
-From 85ca3e5392902f15d3ce1a4a8004fc7f9a7657d8 Mon Sep 17 00:00:00 2001
-From: Michael Tautschnig <tautschn@amazon.com>
-Date: Fri, 29 Sep 2023 11:45:30 +0000
-Subject: [PATCH] C library: Refine and improve stdio models
-
-Fixes portability to FreeBSD, which redefines several functions as
-macros that would only conditionally call that function. Also, ensure
-that stdin/stdout/stderr point to valid objects when those are
-fdopen'ed.
---- .github/workflows/bsd.yaml.orig 2024-11-28 20:55:26 UTC
-+++ .github/workflows/bsd.yaml
-@@ -63,6 +63,7 @@ jobs:
- # gmake TAGS='[!shouldfail]' -C jbmc/unit test
- echo "Run regression tests"
- gmake -C regression/cbmc test
-+ gmake -C regression/cbmc-library test
- # gmake -C regression test-parallel JOBS=2
- # gmake -C regression/cbmc test-paths-lifo
- # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
-@@ -125,6 +126,10 @@ jobs:
- # gmake TAGS='[!shouldfail]' -C jbmc/unit test
- echo "Run regression tests"
- gmake -C regression/cbmc test
-+ # TODO: fileno and *fprintf tests are failing, requires debugging
-+ # https://github.com/openbsd/src/blob/master/include/stdio.h may be
-+ # useful (likely need to allocate __sF)
-+ gmake -C regression/cbmc-library test || true
- # gmake -C regression test-parallel JOBS=2
- # gmake -C regression/cbmc test-paths-lifo
- # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
-@@ -190,6 +195,7 @@ jobs:
- echo "Run regression tests"
- # TODO: we need to model some more library functions
- gmake -C regression/cbmc test || true
-+ gmake -C regression/cbmc-library test || true
- # gmake -C regression test-parallel JOBS=2
- # gmake -C regression/cbmc test-paths-lifo
- # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
- .github/workflows/bsd.yaml | 6 +
- regression/cbmc-library/fileno-01/main.c | 8 +-
- .../variant_multidimensional_ackermann/main.c | 3 +-
- src/ansi-c/library/stdio.c | 139 +++++++++++++++---
- 4 files changed, 132 insertions(+), 24 deletions(-)
-
---- regression/cbmc-library/fileno-01/main.c.orig 2024-11-28 20:55:26 UTC
-+++ regression/cbmc-library/fileno-01/main.c
-@@ -3,14 +3,10 @@ int main()
-
- int main()
- {
-- // requires initialization of stdin/stdout/stderr
-- // assert(fileno(stdin) == 0);
-- // assert(fileno(stdout) == 1);
-- // assert(fileno(stderr) == 2);
--
- int fd;
- FILE *some_file = fdopen(fd, "");
-- assert(fileno(some_file) >= -1);
-+ if(some_file)
-+ assert(fileno(some_file) >= -1);
-
- return 0;
- }
---- regression/contracts-dfcc/variant_multidimensional_ackermann/main.c.orig 2024-11-28 20:55:26 UTC
-+++ regression/contracts-dfcc/variant_multidimensional_ackermann/main.c
-@@ -8,7 +8,8 @@ int main()
- int n = 5;
- int result = ackermann(m, n);
-
-- printf("Result of the Ackermann function: %d\n", result);
-+ // we don't currently have contracts on what printf is assigning to
-+ // printf("Result of the Ackermann function: %d\n", result);
- return 0;
- }
-
---- src/ansi-c/library/stdio.c.orig 2024-11-28 20:55:26 UTC
-+++ src/ansi-c/library/stdio.c
-@@ -6,15 +6,7 @@
- #define __CPROVER_STDIO_H_INCLUDED
- #endif
-
--/* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
--#if defined(__OpenBSD__)
--#undef getchar
- #undef putchar
--#undef getc
--#undef feof
--#undef ferror
--#undef fileno
--#endif
-
- __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
-
-@@ -237,7 +229,8 @@ __CPROVER_HIDE:;
- __CPROVER_set_must(stream, "closed");
- #endif
- int return_value=__VERIFIER_nondet_int();
-- free(stream);
-+ if(stream != stdin && stream != stdout && stream != stderr)
-+ free(stream);
- return return_value;
- }
-
-@@ -253,25 +246,83 @@ __CPROVER_HIDE:;
- #define __CPROVER_STDLIB_H_INCLUDED
- #endif
-
-+#ifndef __CPROVER_ERRNO_H_INCLUDED
-+# include <errno.h>
-+# define __CPROVER_ERRNO_H_INCLUDED
-+#endif
-+
- FILE *fdopen(int handle, const char *mode)
- {
- __CPROVER_HIDE:;
-- (void)handle;
-+ if(handle < 0)
-+ {
-+ errno = EBADF;
-+ return NULL;
-+ }
- (void)*mode;
- #ifdef __CPROVER_STRING_ABSTRACTION
- __CPROVER_assert(__CPROVER_is_zero_string(mode),
- "fdopen zero-termination of 2nd argument");
- #endif
-
--#if !defined(__linux__) || defined(__GLIBC__)
-- FILE *f=malloc(sizeof(FILE));
-+#if defined(_WIN32) || defined(__OpenBSD__) || defined(__NetBSD__)
-+ switch(handle)
-+ {
-+ case 0:
-+ return stdin;
-+ case 1:
-+ return stdout;
-+ case 2:
-+ return stderr;
-+ default:
-+ {
-+ FILE *f = malloc(sizeof(FILE));
-+ __CPROVER_assume(fileno(f) == handle);
-+ return f;
-+ }
-+ }
- #else
-- // libraries need to expose the definition of FILE; this is the
-+# if !defined(__linux__) || defined(__GLIBC__)
-+ static FILE stdin_file;
-+ static FILE stdout_file;
-+ static FILE stderr_file;
-+# else
-+ // libraries need not expose the definition of FILE; this is the
- // case for musl
-- FILE *f=malloc(sizeof(int));
--#endif
-+ static int stdin_file;
-+ static int stdout_file;
-+ static int stderr_file;
-+# endif
-
-+ FILE *f = NULL;
-+ switch(handle)
-+ {
-+ case 0:
-+ stdin = &stdin_file;
-+ __CPROVER_havoc_object(&stdin_file);
-+ f = &stdin_file;
-+ break;
-+ case 1:
-+ stdout = &stdout_file;
-+ __CPROVER_havoc_object(&stdout_file);
-+ f = &stdout_file;
-+ break;
-+ case 2:
-+ stderr = &stderr_file;
-+ __CPROVER_havoc_object(&stderr_file);
-+ f = &stderr_file;
-+ break;
-+ default:
-+# if !defined(__linux__) || defined(__GLIBC__)
-+ f = malloc(sizeof(FILE));
-+# else
-+ f = malloc(sizeof(int));
-+# endif
-+ }
-+
-+ __CPROVER_assume(fileno(f) == handle);
- return f;
-+#endif
- }
-
- /* FUNCTION: _fdopen */
-@@ -291,19 +342,60 @@ FILE *fdopen(int handle, const char *mode)
- #define __CPROVER_STDLIB_H_INCLUDED
- #endif
-
-+#ifndef __CPROVER_ERRNO_H_INCLUDED
-+# include <errno.h>
-+# define __CPROVER_ERRNO_H_INCLUDED
-+#endif
-+
- #ifdef __APPLE__
-+
-+# ifndef LIBRARY_CHECK
-+FILE *stdin;
-+FILE *stdout;
-+FILE *stderr;
-+# endif
-+
- FILE *_fdopen(int handle, const char *mode)
- {
- __CPROVER_HIDE:;
-- (void)handle;
-+ if(handle < 0)
-+ {
-+ errno = EBADF;
-+ return NULL;
-+ }
- (void)*mode;
- #ifdef __CPROVER_STRING_ABSTRACTION
- __CPROVER_assert(__CPROVER_is_zero_string(mode),
- "fdopen zero-termination of 2nd argument");
- #endif
-
-- FILE *f=malloc(sizeof(FILE));
-+ static FILE stdin_file;
-+ static FILE stdout_file;
-+ static FILE stderr_file;
-
-+ FILE *f = NULL;
-+ switch(handle)
-+ {
-+ case 0:
-+ stdin = &stdin_file;
-+ __CPROVER_havoc_object(&stdin_file);
-+ f = &stdin_file;
-+ break;
-+ case 1:
-+ stdout = &stdout_file;
-+ __CPROVER_havoc_object(&stdout_file);
-+ f = &stdout_file;
-+ break;
-+ case 2:
-+ stderr = &stderr_file;
-+ __CPROVER_havoc_object(&stderr_file);
-+ f = &stderr_file;
-+ break;
-+ default:
-+ f = malloc(sizeof(FILE));
-+ }
-+
-+ __CPROVER_assume(fileno(f) == handle);
- return f;
- }
- #endif
-@@ -506,6 +598,8 @@ __CPROVER_HIDE:;
- #define __CPROVER_STDIO_H_INCLUDED
- #endif
-
-+#undef feof
-+
- int __VERIFIER_nondet_int(void);
-
- int feof(FILE *stream)
-@@ -538,6 +632,8 @@ int feof(FILE *stream)
- #define __CPROVER_STDIO_H_INCLUDED
- #endif
-
-+#undef ferror
-+
- int __VERIFIER_nondet_int(void);
-
- int ferror(FILE *stream)
-@@ -570,6 +666,8 @@ int ferror(FILE *stream)
- #define __CPROVER_STDIO_H_INCLUDED
- #endif
-
-+#undef fileno
-+
- int __VERIFIER_nondet_int(void);
-
- int fileno(FILE *stream)
-@@ -735,6 +833,8 @@ int fgetc(FILE *stream)
- #define __CPROVER_STDIO_H_INCLUDED
- #endif
-
-+#undef getc
-+
- int __VERIFIER_nondet_int(void);
-
- int getc(FILE *stream)
-@@ -771,6 +871,8 @@ int getc(FILE *stream)
- #define __CPROVER_STDIO_H_INCLUDED
- #endif
-
-+#undef getchar
-+
- int __VERIFIER_nondet_int(void);
-
- int getchar(void)
-@@ -1939,10 +2041,13 @@ FILE *__acrt_iob_func(unsigned fd)
- switch(fd)
- {
- case 0:
-+ __CPROVER_havoc_object(&stdin_file);
- return &stdin_file;
- case 1:
-+ __CPROVER_havoc_object(&stdout_file);
- return &stdout_file;
- case 2:
-+ __CPROVER_havoc_object(&stderr_file);
- return &stderr_file;
- default:
- return (FILE *)0;