Skip to content

List supported coverage criteria in CBMC's help output #6642

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

Merged
merged 1 commit into from
Feb 4, 2022

Conversation

tautschnig
Copy link
Collaborator

Rather than making the user read further documentation, list all
(currently) supported coverage criteria when running cbmc --help.

For consistency, also add "assumes" as an alternative way to request
coverage of assume statements (previously only "assume" was supported,
even though we otherwise included the plural variants where applicable).

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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.

" where CC is one of assertion, assume,\n" \
" branch, condition, cover, decision,\n" \
" location, mcdc, or path\n" \
" (or the plural of these keywords)\n" \
Copy link
Member

Choose a reason for hiding this comment

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

except for mcdc and cover... I'd drop the mention of plural.
Has path ever been implemented?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks, I've updated the text. Also, I thus removed "path" as it seems the only "implementation" is a "TODO" ...

@codecov
Copy link

codecov bot commented Feb 3, 2022

Codecov Report

Merging #6642 (b17a993) into develop (216e74e) will not change coverage.
The diff coverage is 100.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6642   +/-   ##
========================================
  Coverage    76.72%   76.72%           
========================================
  Files         1579     1579           
  Lines       181938   181938           
========================================
  Hits        139587   139587           
  Misses       42351    42351           
Impacted Files Coverage Δ
src/goto-instrument/cover.cpp 83.93% <100.00%> (ø)

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 b345e2a...b17a993. Read the comment docs.

Rather than making the user read further documentation, list all
(currently) supported coverage criteria when running cbmc --help.

For consistency, also add "assumes" as an alternative way to request
coverage of assume statements (previously only "assume" was supported,
even though we otherwise included the plural variants where applicable).
@tautschnig tautschnig force-pushed the feature/document-cover branch from 406dc27 to b17a993 Compare February 4, 2022 16:06
@tautschnig tautschnig merged commit 107ffa2 into diffblue:develop Feb 4, 2022
@tautschnig tautschnig deleted the feature/document-cover branch February 4, 2022 17:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants