C library: Refine and improve stdio models

[tautschnig]

Depends-on: #9020

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]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.56%. Comparing base (df24632) to head (e02ec39).
⚠️ Report is 13 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8043      +/-   ##
===========================================
- Coverage    80.57%   80.56%   -0.01%     
===========================================
  Files         1708     1708              
  Lines       189217   189223       +6     
  Branches        73       73              
===========================================
- Hits        152460   152455       -5     
- Misses       36757    36768      +11     

☔ 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.

[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.