C library: Refine and improve stdio models

[tautschnig]

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.01%. Comparing base (7a4df92) to head (5d17b24).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8043   +/-   ##
========================================
  Coverage    80.01%   80.01%           
========================================
  Files         1703     1703           
  Lines       188396   188402    +6     
  Branches        73       73           
========================================
+ Hits        150738   150744    +6     
  Misses       37658    37658           

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