Skip to content

[WIP] Filter generated assertions #6688

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
Draft
wants to merge 2 commits into
base: develop
Choose a base branch
from
Draft

[WIP] Filter generated assertions #6688

wants to merge 2 commits into from

Conversation

tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Feb 20, 2022 •
edited
Loading

This changes C/C++ goto checks to be generated at compile time, and
filtered-out based on command-line options at analysis time.

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

@tautschnig tautschnig self-assigned this Feb 20, 2022
@tautschnig tautschnig changed the title [WIP] Filter generated assertions [WIP] Filter generated assertions [depends-on: #6658] Feb 20, 2022
@tautschnig
Replace the goto_check indirection by direct use of goto_check_c
e14e33d 
All existing calls necessarily end up calling goto_check_c.
@tautschnig
Filter generated assertions according to command-line settings
dd7cd37 
Turn into skip C/C++ goto checks that were previously generated, but are
no longer expected as configured via the command line.
@tautschnig tautschnig force-pushed the feature/goto_check_filter branch from 1a2a1dd to dd7cd37 Compare March 8, 2022 22:05
@tautschnig tautschnig changed the title [WIP] Filter generated assertions [depends-on: #6658] [WIP] Filter generated assertions Mar 8, 2022
@tautschnig tautschnig changed the title [WIP] Filter generated assertions [WIP] Filter generated assertions [depends-on: #6716] Mar 25, 2022
tautschnig added a commit that referenced this pull request May 10, 2022
@tautschnig
Merge pull request #6716 from tautschnig/cleanup/goto_check_c
e4d26e0 
Replace the goto_check indirection by direct use of goto_check_c [blocks: #6688]
@tautschnig tautschnig changed the title [WIP] Filter generated assertions [depends-on: #6716] [WIP] Filter generated assertions Nov 9, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs will be requested when the pull request is marked ready for review martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel will be requested when the pull request is marked ready for review peterschrammel is a code owner

@kroening kroening Awaiting requested review from kroening kroening will be requested when the pull request is marked ready for review kroening is a code owner

At least 1 approving review is required to merge this pull request.

Assignees

@tautschnig tautschnig

@kroening kroening

Labels
Property Instrumentation work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@tautschnig @kroening