Run benchcomp unit and regression tests in CI#2382
Run benchcomp unit and regression tests in CI#2382karkhaz merged 1 commit intomodel-checking:mainfrom
Conversation
0fbe553 to
f6b78c8
Compare
celinval
left a comment
There was a problem hiding this comment.
Why do you need to build Kani for benchcomp-tests?
|
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) |
f6b78c8 to
814d70c
Compare
74cb494 to
0af1ed1
Compare
This will ensure that benchcomp will continue to correctly parse future changes to Kani's output.
0af1ed1 to
205f3fc
Compare
This will ensure that benchcomp will continue to correctly parse future changes to Kani's output.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.