Skip to content

--cover assume: Add assert statements before assume to check for coverage #6329

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 5 commits into from
Sep 9, 2021
Merged

--cover assume: Add assert statements before assume to check for coverage #6329

merged 5 commits into from
Sep 9, 2021

Conversation

NlightNFotis
Copy link
Contributor

This PR describes a proposed fix to #6057.

It is a work in progress, as it still needs some extra test cases,
and documentation (and whatever fixes may spring up as part of
a CI run).

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

@NlightNFotis NlightNFotis self-assigned this Sep 2, 2021
TGWDB
TGWDB requested changes Sep 2, 2021
View reviewed changes
Copy link
Contributor

@TGWDB TGWDB left a comment

Choose a reason for hiding this comment

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

Some comments in the code, two other things (apart from passing existing checks):

  1. It would be good to have more examples, also including examples where there are no vacuous paths.
  2. doxygen!

@codecov
Copy link

codecov bot commented Sep 2, 2021 •
edited
Loading

Codecov Report

Merging #6329 (d0e76ee) into develop (17983dc) will increase coverage by 0.00%.
The diff coverage is 100.00%.

❗ Current head d0e76ee differs from pull request most recent head f869882. Consider uploading reports for the commit f869882 to get more accurate results
Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6329   +/-   ##
========================================
  Coverage    75.90%   75.91%           
========================================
  Files         1514     1515    +1     
  Lines       163942   163972   +30     
========================================
+ Hits        124442   124472   +30     
  Misses       39500    39500
Impacted Files Coverage Δ
src/goto-checker/properties.h 100.00% <ø> (ø)
src/goto-instrument/cover.cpp 84.04% <100.00%> (+0.61%) ⬆️
src/goto-instrument/cover_instrument.h 94.28% <100.00%> (+0.34%) ⬆️
src/goto-instrument/cover_instrument_assume.cpp 100.00% <100.00%> (ø)
src/goto-instrument/contracts/assigns.cpp 97.77% <0.00%> (+0.05%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update f0ab57e...f869882. Read the comment docs.

@NlightNFotis NlightNFotis force-pushed the assertions_before_assume branch 2 times, most recently from f270860 to 4663eee Compare September 6, 2021 15:30
@NlightNFotis NlightNFotis marked this pull request as ready for review September 6, 2021 15:30
TGWDB
TGWDB reviewed Sep 6, 2021
View reviewed changes
@NlightNFotis NlightNFotis force-pushed the assertions_before_assume branch 3 times, most recently from 54754f9 to c1152d1 Compare September 8, 2021 13:43
@NlightNFotis NlightNFotis force-pushed the assertions_before_assume branch 2 times, most recently from f47f6b9 to b5bd0eb Compare September 8, 2021 16:30
NlightNFotis and others added 5 commits September 9, 2021 13:37
@NlightNFotis
Enfold assume in an assert(false) to allow for easier debugging.
16d3a2b 
This allows for easier debugging by allowing `assume(false)`s that
end up emptying the search state space to be identified on a more
granular basis.
@NlightNFotis
Add reference test case for --cover assume code.
ba0d138 
This was provided as reference for an issue described in
diffblue#6057.
@NlightNFotis
Add second test case that features assume statement hidden behind
9b7d9e2 
branch.
@NlightNFotis
[DOCS] Add documentation for the new --cover assume coverage criter…
3514772 
…ion.
@TGWDB @NlightNFotis
Fix Windows error by changing scope of namespace
f869882 
This moves a dummy namespace needed for expr2c to be created as
the argument to the call.
@NlightNFotis NlightNFotis force-pushed the assertions_before_assume branch from d0e76ee to f869882 Compare September 9, 2021 12:37
@TGWDB TGWDB merged commit b4c3a12 into diffblue:develop Sep 9, 2021
@NlightNFotis NlightNFotis deleted the assertions_before_assume branch September 10, 2021 16:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

@TGWDB TGWDB TGWDB approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

Assignees

@NlightNFotis NlightNFotis

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@NlightNFotis @peterschrammel @TGWDB