Skip to content

Conversation

@karkhaz
Copy link
Contributor

@karkhaz karkhaz commented Apr 17, 2023

This will ensure that benchcomp will continue to correctly parse future changes to Kani's output.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@karkhaz karkhaz requested a review from a team as a code owner April 17, 2023 16:10
@karkhaz karkhaz force-pushed the kk-run-benchcomp-tests branch from 0fbe553 to f6b78c8 Compare April 17, 2023 16:18
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Why do you need to build Kani for benchcomp-tests?

@karkhaz
Copy link
Contributor Author

karkhaz commented Apr 17, 2023

One of the regression tests (and probably more in the future) run Kani on two of the performance benchmarks. So it doesn't do the full perf test, but just runs benchmarks to ensure that it can continue to parse Kani's output in case the output changes later.

I could split the tests into regression tests that do and don't run Kani, but overall the Kani build time is going to dominate so it will take just as long anyway...

We may wish to add different regression tests for other kinds of parsers later. If we're looking to parse CBMC results, I have a patch that adds a litani parser and a regression test that runs litani (not on real proofs, again just something trivial that tests the parser)

@karkhaz karkhaz force-pushed the kk-run-benchcomp-tests branch from f6b78c8 to 814d70c Compare April 17, 2023 16:42
@karkhaz karkhaz enabled auto-merge (squash) April 17, 2023 16:42
@karkhaz karkhaz force-pushed the kk-run-benchcomp-tests branch 4 times, most recently from 74cb494 to 0af1ed1 Compare April 18, 2023 19:58
This will ensure that benchcomp will continue to correctly parse future
changes to Kani's output.
@karkhaz karkhaz force-pushed the kk-run-benchcomp-tests branch from 0af1ed1 to 205f3fc Compare April 19, 2023 03:45
@karkhaz karkhaz merged commit 588baf0 into model-checking:main Apr 19, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants