C library: Refine and improve stdio models by tautschnig · Pull Request #8043 · diffblue/cbmc

tautschnig · 2023-11-16T09:25:28Z

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.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2023-11-16T10:12:54Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.40%. Comparing base (2e6200a) to head (49f4cd1).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8043   +/-   ##
========================================
  Coverage    80.39%   80.40%           
========================================
  Files         1688     1688           
  Lines       207403   207413   +10     
  Branches        73       73           
========================================
+ Hits        166749   166769   +20     
+ Misses       40654    40644   -10

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

BSD systems appear to use `__` prefixed variants of several functions. Define these as needed. Also, avoid handling some GCC-style `__builtin_`-prefixed functions via models when others are done directly in the type checker: do all of them in the type checker.

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.

Copilot

Pull request overview

Refines CBMC’s C-library stdio/math models to improve portability (notably on BSDs where some stdio/math functions are macros) and to ensure stdin/stdout/stderr refer to valid objects when created via fdopen.

Changes:

Adjust stdio models (fdopen, macro #undefs, and fclose) to avoid macro collisions and invalid frees of standard streams.
Expand math support for builtin/macro variants (__isfinite*, __isnormal*, __signbit*) and switch infinities to __CPROVER_*inf*.
Update/add regression tests and run cbmc-library regressions on BSD CI.

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 7 comments.

Show a summary per file

File	Description
src/ansi-c/library_check.sh	Ignores additional platform/builtin math symbols during library checking.
src/ansi-c/library/stdio.c	Improves `fdopen`/`_fdopen` and standard stream handling; undefines macro-wrapped stdio functions locally.
src/ansi-c/library/math.c	Adds/adjusts builtin math entry points and uses `__CPROVER_inf` helpers.
src/ansi-c/c_typecheck_expr.cpp	Typechecks additional compiler builtin identifiers (`__builtin_is`, `__builtin_fabs`).
regression/contracts-dfcc/variant_multidimensional_ackermann/main.c	Disables `printf` call that lacks suitable contracts.
regression/cbmc-library/toupper/main.c	Skips test on BSDs pending conversion-table modeling.
regression/cbmc-library/tolower/main.c	Skips test on BSDs pending conversion-table modeling.
regression/cbmc-library/signbit/main.c	Adds assertions for `signbit` on double/long double (with Apple guard).
regression/cbmc-library/isnormal/main.c	Replaces placeholder failure with a builtin constness check.
regression/cbmc-library/isinf/main.c	Adds runtime and compile-time checks for GCC builtins.
regression/cbmc-library/isfinite/main.c	Adds behavioral checks comparing `isfinite` vs `fpclassify`.
regression/cbmc-library/fileno/main.c	Guards `fileno` assertion when `fdopen` returns NULL.
regression/cbmc-library/copysignl/test.desc	Promotes to CORE and adjusts options.
regression/cbmc-library/cnd_broadcast/test.desc	Promotes to CORE and adjusts options.
regression/cbmc-library/__fpclassify/main.c	Adds IEEE behavior checks and GCC builtin checks.
.github/workflows/bsd.yaml	Runs `cbmc-library` regressions on BSD jobs (some allowed to fail).

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-03-09T15:59:29Z

src/ansi-c/library/stdio.c

+#  if !defined(__linux__) || defined(__GLIBC__)
+    f = malloc(sizeof(FILE));
+#  else
+    f = malloc(sizeof(int));
+#  endif
+  }

+  __CPROVER_assume(fileno(f) == handle);


f can be NULL if malloc fails, but fileno(f) is still evaluated in the __CPROVER_assume, which is undefined behavior. Handle allocation failure explicitly (e.g., set errno = ENOMEM; return NULL;) or add an assumption that f is non-NULL before calling fileno.

Copilot · 2026-03-09T15:59:29Z

src/ansi-c/library/stdio.c

+    return stderr;
+  default:
+  {
+    FILE *f = malloc(sizeof(FILE));


Same issue as the other branch: if malloc returns NULL, fileno(f) is evaluated on a NULL pointer inside __CPROVER_assume. Add an explicit allocation-failure path (set errno = ENOMEM and return NULL) or assume f is non-NULL before calling fileno.

Suggested change

FILE *f = malloc(sizeof(FILE));

FILE *f = malloc(sizeof(FILE));

if(f == NULL)

{

errno = ENOMEM;

return NULL;

}

Copilot · 2026-03-09T15:59:30Z

src/ansi-c/library/stdio.c

+  default:
+    f = malloc(sizeof(FILE));
+  }

+  __CPROVER_assume(fileno(f) == handle);
  return f;


_fdopen has the same NULL-allocation hazard: f may be NULL, but fileno(f) is still evaluated. Add explicit handling for allocation failure (e.g., errno = ENOMEM; return NULL;) or assume f is non-NULL before invoking fileno.

Copilot · 2026-03-09T15:59:30Z

regression/cbmc-library/signbit/main.c

+#endif
+  assert(signbit(1.0l) == 0);


The Apple version guard only applies to the negative long double assertion, but the positive long double assertion remains unguarded. If signbit(long double) is unavailable/incorrect on older Apple targets (as implied by the guard), the 1.0l assertion should likely be inside the same #if (or be guarded by an equivalent condition) to avoid inconsistent behavior across Apple versions.

Suggested change

#endif

assert(signbit(1.0l) == 0);

assert(signbit(1.0l) == 0);

#endif

Copilot · 2026-03-09T15:59:30Z

regression/cbmc-library/copysignl/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c


Promoting this test from KNOWNBUG to CORE also removes the previous --pointer-check --bounds-check options. If the intent is to keep the same verification strength while reclassifying the test, consider retaining those options (or documenting in the PR/commit message why they should be dropped).

Suggested change

main.c

main.c --pointer-check --bounds-check

Copilot · 2026-03-09T15:59:31Z

regression/cbmc-library/cnd_broadcast/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE


Same as copysignl: switching to CORE also drops --pointer-check --bounds-check. Consider keeping the checks (or documenting why the test should run without them) to avoid unintentionally weakening coverage.

Suggested change

CORE

CORE --pointer-check --bounds-check

Copilot · 2026-03-09T15:59:31Z

.github/workflows/bsd.yaml

+            # 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


|| true will mask any new regressions in regression/cbmc-library on OpenBSD. Prefer using the workflow’s continue-on-error: true for that step/job, or skipping/xfailing only the known failing tests (e.g., by tagging or filtering), so unrelated failures still surface in CI logs/status.

tautschnig added the C Front End label Nov 16, 2023

tautschnig self-assigned this Nov 16, 2023

tautschnig force-pushed the bugfixes/stdio branch 4 times, most recently from d479dc1 to 3917e27 Compare December 19, 2023 13:51

tautschnig marked this pull request as ready for review December 19, 2023 13:51

tautschnig requested review from a team, kroening, peterschrammel and remi-delmas-3000 as code owners December 19, 2023 13:51

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Dec 19, 2023

tautschnig force-pushed the bugfixes/stdio branch from 3917e27 to 85ca3e5 Compare December 19, 2023 13:53

tautschnig mentioned this pull request Sep 22, 2024

C library: fix build on FreeBSD #8463

Closed

7 tasks

tautschnig force-pushed the bugfixes/stdio branch 2 times, most recently from 3d5bb00 to 22e9222 Compare May 30, 2025 11:07

tautschnig force-pushed the bugfixes/stdio branch from 22e9222 to 94cbfa2 Compare June 25, 2025 07:43

tautschnig assigned tautschnig and unassigned kroening and peterschrammel Jun 25, 2025

tautschnig force-pushed the bugfixes/stdio branch 3 times, most recently from e7bf25e to e0c978c Compare July 4, 2025 21:41

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Jul 4, 2025

tautschnig force-pushed the bugfixes/stdio branch from e0c978c to 49f4cd1 Compare July 28, 2025 11:25

tautschnig added 2 commits March 9, 2026 15:51

C library: Refine and improve stdio models

aa95077

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.

Copilot AI review requested due to automatic review settings March 9, 2026 15:51

tautschnig force-pushed the bugfixes/stdio branch from 49f4cd1 to aa95077 Compare March 9, 2026 15:51

Copilot AI reviewed Mar 9, 2026

View reviewed changes

Copilot started reviewing on behalf of tautschnig March 9, 2026 18:30 View session

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

C library: Refine and improve stdio models#8043

C library: Refine and improve stdio models#8043
tautschnig wants to merge 2 commits intodiffblue:developfrom
tautschnig:bugfixes/stdio

tautschnig commented Nov 16, 2023

Uh oh!

codecov bot commented Nov 16, 2023 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Mar 9, 2026

Uh oh!

Copilot AI Mar 9, 2026

Uh oh!

Copilot AI Mar 9, 2026

Uh oh!

Copilot AI Mar 9, 2026

Uh oh!

Copilot AI Mar 9, 2026

Uh oh!

Copilot AI Mar 9, 2026

Uh oh!

Copilot AI Mar 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

-    FILE *f = malloc(sizeof(FILE));
+    FILE *f = malloc(sizeof(FILE));
+    if(f == NULL)
+    {
+      errno = ENOMEM;
+      return NULL;
+    }

Conversation

tautschnig commented Nov 16, 2023

Uh oh!

codecov bot commented Nov 16, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 9, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

codecov bot commented Nov 16, 2023 •

edited

Loading