Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adds an over-approximation model for sysconf #7780

Merged
merged 1 commit into from
Jul 11, 2023

Conversation

feliperodri
Copy link
Collaborator

  • 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.
  • 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).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Jun 22, 2023

Codecov Report

Patch coverage has no change and project coverage change: +0.47 🎉

Comparison is base (64bf1ca) 78.14% compared to head (830a60f) 78.61%.

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7780      +/-   ##
===========================================
+ Coverage    78.14%   78.61%   +0.47%     
===========================================
  Files         1697     1697              
  Lines       193629   193629              
===========================================
+ Hits        151309   152229     +920     
+ Misses       42320    41400     -920     

see 45 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

src/ansi-c/library/unistd.c Outdated Show resolved Hide resolved
src/ansi-c/library/unistd.c Outdated Show resolved Hide resolved
src/ansi-c/library/unistd.c Outdated Show resolved Hide resolved
@feliperodri feliperodri force-pushed the sysconf-model branch 2 times, most recently from 3584288 to b03ede9 Compare July 10, 2023 22:46
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri feliperodri merged commit 4b95215 into diffblue:develop Jul 11, 2023
35 checks passed
@feliperodri feliperodri deleted the sysconf-model branch July 11, 2023 18:58

// We should keep errno as non-determinist as possible, since this model
// nver takes into account the name input.
errno = __VERIFIER_nondet_unsigned_int();
Copy link
Collaborator

Choose a reason for hiding this comment

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

This is prone to arithmetic conversion failures for errno is signed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users aws-high
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants