Date: Tue, 7 Jan 2025 18:37:48 GMT From: Olivier Cochard <olivier@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: 127777fd65d5 - main - devel/cbmc: Update to 6.4.1 Message-ID: <202501071837.507IbmRo068387@gitrepo.freebsd.org>
next in thread | raw e-mail | index | archive | help
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;
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202501071837.507IbmRo068387>