kani
kani copied to clipboard
Generate `benchcomp.yaml` documentation from schema
Description of changes:
This PR adds a validation schema for the benchcomp configuration file format, as well as code to emit that schema into the Kani book. This is in preparation for further PRs that will add similar schemas for the format that a benchcomp parser should emit, and the format that benchcomp visualizers should expect, both of which will also be rendered in the book.
Resolved issues:
Resolves #2592
Related RFC:
None
Call-outs:
N/A
Testing:
- How is this change tested?[
Rendered version](https://karkhaz.github.io/kani/benchcomp-conf.html) on my fork
- Is this a refactor change?
No
Checklist
- [ ] Each commit message has a non-empty body, explaining why the change was made
- [x] Methods or procedures are documented
- [x] 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.
Here is how it looks, the text is slightly out of date (I've since made the example shorter)