Skip to content

C library: models of strtol_l, strtoul_l, strtoll_l and strtoull_l - #9444

Open
tautschnig wants to merge 2 commits into
diffblue:developfrom
tautschnig:pr/c-strtol-l-family
Open

tautschnig wants to merge 2 commits into
diffblue:developfrom
tautschnig:pr/c-strtol-l-family

Conversation

@tautschnig

Copy link
Copy Markdown
Collaborator

POSIX.1-2024 (and glibc, macOS) have the conversions of strtol and its
siblings with an explicit locale; the conversion of integers does not
depend on it beyond the white-space and digit characters, which the
existing models take from the "C" locale. The models call those of
strtol, strtoul, strtoll and strtoull. glibc names them _isoc23*_l in
C23 mode, which get the same models. libc++'s num_get converts every
integer it reads with strtoll_l or strtoull_l, which had no model. New
tests strtol_l, strtoul_l, strtoll_l and strtoull_l.

Co-authored-by: Kiro kiro-agent@users.noreply.github.com
Depends-on: #9439

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

tautschnig and others added 2 commits November 10, 2026 15:36
C23 7.24.1.7: same conversion rules as strtol, which CBMC already
models; the three sibling spellings had NO model, so calls returned
nondeterministic values -- std::stoll (via libstdc++'s __stoa) and
CBMC's own unsafe_string2int/string2optional silently produced
garbage, discovered by a unit proof over src/util/string2int.cpp.
The models mirror the existing strtol model with the result type
adjusted; the unsigned variants negate the converted value for a
leading '-' (C23 7.24.1.7/5).

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
POSIX.1-2024 (and glibc, macOS) have the conversions of strtol and its
siblings with an explicit locale; the conversion of integers does not
depend on it beyond the white-space and digit characters, which the
existing models take from the "C" locale.  The models call those of
strtol, strtoul, strtoll and strtoull.  glibc names them __isoc23_*_l in
C23 mode, which get the same models.  libc++'s num_get converts every
integer it reads with strtoll_l or strtoull_l, which had no model.  New
tests strtol_l, strtoul_l, strtoll_l and strtoull_l.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9439
Copilot AI balanced review requested due to automatic review settings November 10, 2026 20:49

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota. Try requesting a review at a lower effort level.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing. Review the Copilot code review billing settings.

@codecov

codecov Bot commented Nov 10, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 81.02%. Comparing base (826c1c7) to head (71bceec).
⚠️ Report is 2 commits behind head on develop.

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #9444      +/-   ##
===========================================
- Coverage    81.02%   81.02%   -0.01%     
===========================================
  Files         1723     1723              
  Lines       191314   191314              
  Branches        73       73              
===========================================
- Hits        155020   155017       -3     
- Misses       36294    36297       +3     

☔ View full report in Codecov by Harness.
📢 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.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants