Date: Sat, 20 Jun 2026 16:23:54 +0000 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: 2a9a7b3cc92e - main - devel/cbmc: update to 6.9.0 Message-ID: <6a36be9a.1837f.38588c91@gitrepo.freebsd.org>
index | next in thread | raw e-mail
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;home | help
Want to link to this message? Use this
URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?6a36be9a.1837f.38588c91>