Check cbmc-library regressions for completeness #4658
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
force-pushed
the
library-check
branch
from
32a309f to
edbd1fd
Compare
Codecov ReportBase: 78.36% // Head: 78.37% // Increases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #4658 +/- ##
========================================
Coverage 78.36% 78.37%
========================================
Files 1647 1647
Lines 189961 189984 +23
========================================
+ Hits 148861 148895 +34
+ Misses 41100 41089 -11
Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report at Codecov. |
tautschnig
force-pushed
the
library-check
branch
from
edbd1fd to
1d9fb6c
Compare
tautschnig
force-pushed
the
library-check
branch
3 times, most recently
from
bc49a57 to
05d6e86
Compare
tautschnig
changed the title
|
#5780 fixes the CSmith failure. |
tautschnig
force-pushed
the
library-check
branch
2 times, most recently
from
720c033 to
26012d0
Compare
tautschnig
force-pushed
the
library-check
branch
from
26012d0 to
01e05af
Compare
tautschnig
force-pushed
the
library-check
branch
from
01e05af to
c5969b6
Compare
tautschnig
changed the title
tautschnig
force-pushed
the
library-check
branch
from
c5969b6 to
d08cb19
Compare
tautschnig
force-pushed
the
library-check
branch
2 times, most recently
from
191d421 to
7e6024e
Compare
tautschnig
force-pushed
the
library-check
branch
from
7e6024e to
c6a5f55
Compare
tautschnig
force-pushed
the
library-check
branch
2 times, most recently
from
671d3a4 to
ca7b6d9
Compare
In cbmc-library/, we organise regression tests by the name of the library function they are exercising.
In cbmc-library/, we organise regression tests by the name of the library function they are exercising.
This test has been built to exercise --nan-check, not necessarily to exercise particular library functions (even when it does use library functions).
In cbmc-library/, we organise regression tests by the name of the library function they are exercising. Rename these tests with the library function they exercise. For those not focussing on library functions, move them to cbmc/ instead. As those tests are also run past the cprover SMT solver, three tests newly demonstrated issues in the SMT back-end.
These are all marked KNOWNBUG and need tweaking.
These are whitespace changes only.
This will make sure that newly added library functions are also covered by tests.
tautschnig
force-pushed
the
library-check
branch
from
ca7b6d9 to
e8f5ffd
Compare
tautschnig
assigned tautschnig and unassigned kroening, remi-delmas-3000 and peterschrammel
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.
This will make sure that newly added library functions are also covered by
tests.