From nobody Tue Jan 7 18:37:48 2025 X-Original-To: dev-commits-ports-all@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4YSKY90XrBz5jkZt; Tue, 07 Jan 2025 18:37:49 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R11" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4YSKY84L0Vz4p2s; Tue, 7 Jan 2025 18:37:48 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1736275068; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=qqnW2eTURLZFZiuRhaJxX57q0lxR3ODi5NF9viZpl/8=; b=BMySNdXVsygxHqFMzMPhAQXHUj2YbSuiWAkVdilV2ngdYs17FOdbgxyDSAtT1YxxM9FFX8 +B4sbs1gM2n+2F+k975lLKbPWrb6XQbovqMnOUbhePDyuKEVLU5mS10K/4DRXYnm3Q4pHW /kMcHh7/KLX1pgnUklXPYl2kI8L10NR8RjdZen9/d3GmH4SMLrDW01i9N4S539l+Dbctc1 PFEr1Ahtz6w8I+/Y8FdEPgu8J46pMqM3j1GgmypnZEGY4hPEDU+AqLvGd2xI3C8ck5QsQ1 XDVMW93hYbLT7easKRi1lGkhZmbNBSF9iiX49syVECHs26Rwn7lS49HZ2Dcnrw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1736275068; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=qqnW2eTURLZFZiuRhaJxX57q0lxR3ODi5NF9viZpl/8=; b=XufPpFCNjifumpR75MWHmFtG5X9w8lJykOVkkDGoQoWdGFj80LNKXFLQoZgWarRSpdvALq q6BJeZ/fRizYSCE9wRzAEkkbtYW2qEM6+A2lqrqgOz9m/XkyHdGg2tyR/0adSYYCfrDE7O /6BRtBYhXeRWHbBDn2iTGqJC9IJAuPbjG8RrnUEuUJjfI/gddk7EMMvvnKvJKH86S3FqT5 q30yJ95I2Bs7p2+U+xQ/srjDQ5MhnFvEaCtf7W69AIafybxw5ckXirJ5RJH0F4e9c67m52 HQoC4X/Q0/v6UKIMVTraNSQU5iWDU/1l0sUdy5WIYpKKvifDkt9EOaHJv7RDZA== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1736275068; a=rsa-sha256; cv=none; b=WOfpRHYSxx/1oKH40oEVWmtTCY0Z489gCOb4pkHzEdylhrdZTpxvY4mIAn8+qehGnHiiGL gzqX8ONKpb86X8DRVg4HcI3Q1agQU6p1giNYdyP87GGFjWCkaIjR+hzLpPwJFiH5m2JslA yMDlvCt+f3BCF1zsM2EPLRQbMBlqvWT7ih9FaXHG4yll5Ii8o5xzBvxgGzn/U+X+qAKkFv +I5xEzKD55LdfvZQLb1qIWVzhwjbySzG/gR2B9APGMZyinOozsO2F4hpJqMCN0NZYUIQO3 6QehBPhy59hEhwtpO47CwCBiYZGzW74PB2cYSvGhtLS1S6MzrxT63GrQ3IIJZg== ARC-Authentication-Results: i=1; mx1.freebsd.org; none Received: from gitrepo.freebsd.org (gitrepo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:5]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4YSKY83k59z5Ty; Tue, 07 Jan 2025 18:37:48 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.18.1/8.18.1) with ESMTP id 507Ibm3F068390; Tue, 7 Jan 2025 18:37:48 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.18.1/8.18.1/Submit) id 507IbmRo068387; Tue, 7 Jan 2025 18:37:48 GMT (envelope-from git) Date: Tue, 7 Jan 2025 18:37:48 GMT Message-Id: <202501071837.507IbmRo068387@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Olivier Cochard Subject: git: 127777fd65d5 - main - devel/cbmc: Update to 6.4.1 List-Id: Commit messages for all branches of the ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-all List-Help: List-Post: List-Subscribe: List-Unsubscribe: X-BeenThere: dev-commits-ports-all@freebsd.org Sender: owner-dev-commits-ports-all@FreeBSD.org MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Git-Committer: olivier X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: 127777fd65d52ec536aceb79c04f39d393f5703a Auto-Submitted: auto-generated The branch main has been updated by olivier: URL: https://cgit.FreeBSD.org/ports/commit/?id=127777fd65d52ec536aceb79c04f39d393f5703a commit 127777fd65d52ec536aceb79c04f39d393f5703a Author: Olivier Cochard AuthorDate: 2025-01-07 17:56:15 +0000 Commit: Olivier Cochard 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 with + std::basic_string + +Fixes build with libc++19 that fails with the error: + +> implicit instantiation of undefined template 'std::char_traits' + +Motivation for the change: std::basic_string 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 value= ++ std::basic_string 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 convert_one_string_literal( ++std::basic_string convert_one_string_literal( + const std::string &src) + { + PRECONDITION(src.size() >= 2); +@@ -28,7 +28,7 @@ std::basic_string convert_one_string_lit + PRECONDITION(src[src.size() - 1] == '"'); + PRECONDITION(src[2] == '"'); + +- std::basic_string value= ++ std::basic_string value= + unescape_wide_string(std::string(src, 3, src.size()-4)); + + // turn into utf-8 +@@ -57,7 +57,7 @@ std::basic_string convert_one_string_lit + unescape_string(std::string(src, 1, src.size()-2)); + + // pad into wide string +- std::basic_string value; ++ std::basic_string value; + value.resize(char_value.size()); + for(std::size_t i=0; i value; ++ std::basic_string 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 tmp_value= ++ std::basic_string 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 value_str(1, value); ++ std::basic_string 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 &dest) ++ std::basic_string &dest) + { + dest.push_back(value); + } +@@ -153,10 +153,10 @@ std::string unescape_string(const std::string &src) + return unescape_string_templ(src); + } + +-std::basic_string unescape_wide_string( ++std::basic_string unescape_wide_string( + const std::string &src) + { +- return unescape_string_templ(src); ++ return unescape_string_templ(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 + + std::string unescape_string(const std::string &); +-std::basic_string unescape_wide_string(const std::string &); ++std::basic_string 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 utf32; ++ std::basic_string 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 &s) ++utf32_native_endian_to_utf8(const std::basic_string &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 &s); ++utf32_native_endian_to_utf8(const std::basic_string &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(expr)) ++ [[maybe_unused]] const auto plus_overflow = expr_try_dynamic_cast(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(expr)) ++ if([[maybe_unused]] const auto minus = expr_try_dynamic_cast(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(expr)) ++ [[maybe_unused]] const auto shl_overflow = expr_try_dynamic_cast(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(to_type)) ++ if([[maybe_unused]] const auto to_fixedbv_type = type_try_dynamic_cast(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(to_type)) ++ if([[maybe_unused]] const auto to_floatbv_type = type_try_dynamic_cast(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(to_type)) ++ if([[maybe_unused]] const auto bool_type = type_try_dynamic_cast(to_type)) + return make_not_zero(from_term, cast.op().type()); + if(const auto c_bool_type = type_try_dynamic_cast(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(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 +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 ++# 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 ++# 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;