C library header de-duplication #6490
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
requested review from
chrisr-diffblue and
kroening
as code owners
tautschnig
force-pushed
the
c-library-cleanup
branch
from
01e6bbe to
bfa2735
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6490 +/- ##
========================================
Coverage 76.10% 76.10%
========================================
Files 1548 1548
Lines 166326 166326
========================================
Hits 126576 126576
Misses 39750 39750 Continue to review full report at Codecov.
|
martin-cs
approved these changes
Nov 30, 2021
| @@ -7,6 +7,7 @@ for f in "$@"; do | |||
| echo "Checking ${f}" | |||
| cp "${f}" __libcheck.c | |||
| perl -p -i -e 's/(__builtin_[^v])/s$1/' __libcheck.c | |||
| perl -p -i -e 's/s(__builtin_unreachable)/$1/' __libcheck.c | |||
There was a problem hiding this comment.
Couldn't you just do this for __CPROVER_assume(0) instead?
There was a problem hiding this comment.
That would be a valid hack, but then it's only __CPROVER_assume(0) that actually makes the code thereafter unreachable, so it's a bit strange perhaps?
tautschnig
force-pushed
the
c-library-cleanup
branch
from
bfa2735 to
638a520
Compare
kroening
approved these changes
Dec 5, 2021
Fixes the declaration in builtin_headers.h. Type checking actually ignored this declaration and would always generate the expression of the correct type.
Makes GCC happier when doing library validation. Our C front-end would implicitly generate nondet return values of the correct type, so this does not actually change any verification behaviour.
The uninitialised local variable can trip up GCC's validation. Use a __VERIFIER_nondet_ function as is already done elsewhere.
These calls are wrapped in #ifdef LIBRARY_CHECK and exist for the sole purpose of making library_check.sh not warn about `noreturn` functions seemingly returning.
tautschnig
force-pushed
the
c-library-cleanup
branch
from
638a520 to
fc7072d
Compare
library/cprover.h exists for the sole purpose of syntax-checking the C library using the system's C compiler. The declarations in there, however, did not always match those of the authoritative cprover_builtin_library.h. To avoid this split-brain problem, just include cprover_builtin_library.h after providing a few declarations otherwise generated by ansi_c_internal_additions.cpp.
tautschnig
force-pushed
the
c-library-cleanup
branch
from
fc7072d to
5295845
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Please review commit-by-commit: the goal of this PR is spelled out in the last commit in this series (removing duplicate-and-conflicting declarations), and the commits before this one enable this work while making sure
library_check.shremains happy.