Skip to content

Document --exclude_rule #393

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

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Document --exclude_rule #393

wants to merge 4 commits into from

Conversation

naftali-g
Copy link
Contributor

@naftali-g naftali-g commented May 12, 2025

Naming convention:

  • PRs for features that are in design should have the "proposal" label
  • PRs for features that haven't landed yet should have the "future" label
  • PRs for upcoming releases should have the "release" label
  • PRs with new documentation for existing features should have the "existing feature" label

Before requesting review:

  • Make sure there is a ticket in the DOC board in Jira
  • Make sure CI is passing
    • Spell check failure may require adding backticks around code or updating spelling_wordlist.txt
    • See README.md for information about style and markdown syntax
    • If the CI Details link gives a 404, you need to log in to readthedocs.com
  • Add link to generated documentation here
    • you can find this by following the read the docs link from the CI check
  • Ask for help in #documentation

Jira ticket: TODO
Link to generated documentation: https://certora-certora-prover-documentation--393.com.readthedocs.build/en/393/docs/prover/cli/options.html#method

@naftali-g naftali-g force-pushed the naftali/exclude_method branch from 0335cdf to 6e21181 Compare May 12, 2025 19:18
@naftali-g naftali-g marked this pull request as ready for review May 12, 2025 19:19
@naftali-g naftali-g requested review from urikirsh and johspaeth May 12, 2025 19:19
Copy link
Contributor

@johspaeth johspaeth left a comment

Choose a reason for hiding this comment

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

Thanks. Tiny suggestion for improvement to make the "when to use it" part more explicit.

Comment on lines +297 to +298
If there are specific methods for which a rule/invariant takes too long to run
or require a different configuration.
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
If there are specific methods for which a rule/invariant takes too long to run
or require a different configuration.
If there are specific methods for which a rule/invariant takes too long to run
or require a different configuration, this config option allows to exclude it from verification.

@johspaeth johspaeth added the release documentation for an upcoming release label May 13, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
release documentation for an upcoming release
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants