git: 127777fd65d5 - main - devel/cbmc: Update to 6.4.1
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Tue, 07 Jan 2025 18:37:48 UTC
The branch main has been updated by olivier:
URL: https://cgit.FreeBSD.org/ports/commit/?id=127777fd65d52ec536aceb79c04f39d393f5703a
commit 127777fd65d52ec536aceb79c04f39d393f5703a
Author: Olivier Cochard <olivier@FreeBSD.org>
AuthorDate: 2025-01-07 17:56:15 +0000
Commit: Olivier Cochard <olivier@FreeBSD.org>
CommitDate: 2025-01-07 18:37:29 +0000
devel/cbmc: Update to 6.4.1
---
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, 555 insertions(+), 4 deletions(-)
diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile
index 92743c0170be..28f926218b10 100644
--- a/devel/cbmc/Makefile
+++ b/devel/cbmc/Makefile
@@ -1,5 +1,5 @@
PORTNAME= cbmc
-PORTVERSION= 6.3.1
+PORTVERSION= 6.4.1
DISTVERSIONPREFIX= cbmc-
CATEGORIES= devel
MASTER_SITES= DEBIAN/pool/main/m/minisat2:minisat
diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo
index bff667f3f615..36f820a95e09 100644
--- a/devel/cbmc/distinfo
+++ b/devel/cbmc/distinfo
@@ -1,5 +1,5 @@
-TIMESTAMP = 1730030005
+TIMESTAMP = 1736265016
SHA256 (minisat2_2.2.1.orig.tar.gz) = e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40
SIZE (minisat2_2.2.1.orig.tar.gz) = 44229
-SHA256 (diffblue-cbmc-cbmc-6.3.1_GH0.tar.gz) = cc9183eff2046b41cae28c21e551184e5dbb8125b06c6043ceaceb44dd75886c
-SIZE (diffblue-cbmc-cbmc-6.3.1_GH0.tar.gz) = 9120942
+SHA256 (diffblue-cbmc-cbmc-6.4.1_GH0.tar.gz) = 09507765190bd14d07452b68003087160c80325b251a6f13d50845bb5f44ae7e
+SIZE (diffblue-cbmc-cbmc-6.4.1_GH0.tar.gz) = 9127951
diff --git a/devel/cbmc/files/patch-libc19 b/devel/cbmc/files/patch-libc19
new file mode 100644
index 000000000000..d90dd36c26e3
--- /dev/null
+++ b/devel/cbmc/files/patch-libc19
@@ -0,0 +1,171 @@
+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
new file mode 100644
index 000000000000..465a2fe8aac6
--- /dev/null
+++ b/devel/cbmc/files/patch-src_solvers_flattening_boolbv__overflow.cpp
@@ -0,0 +1,28 @@
+--- 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
new file mode 100644
index 000000000000..f146dee4a4fc
--- /dev/null
+++ b/devel/cbmc/files/patch-src_solvers_smt2__incremental_convert__expr__to__smt.cpp
@@ -0,0 +1,37 @@
+--- 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
new file mode 100644
index 000000000000..bf9b3d6fe6b8
--- /dev/null
+++ b/devel/cbmc/files/patch-stdio-models-freebsd
@@ -0,0 +1,315 @@
+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;