Add an option to Kani to verify a custom version of the standard library. #3226
Assignees
Comments
4 tasks
celinval
added a commit
that referenced
this issue
Jun 4, 2024
While at it, I also added a `--skip-libs` to skip rebuilding the Kani libraries and standard library at every `cargo build-dev` execution. We usually only need to rebuild the libraries when we make changes to them or when we update the Rust toolchain. Rebuilding them can be quite time consuming when you are making changes to Kani. Towards #3226 #3153 Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
celinval
added a commit
that referenced
this issue
Jun 6, 2024
This subcommand will take the path to the standard library. It will then use `cargo build -Z build-std` to build the custom standard library and verify any harness found during the build. ## Call out - So far I only performed manual tests. I'm going to add a few unit tests and a script in the next revision. Resolves #3226 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
celinval
added a commit
that referenced
this issue
Jun 7, 2024
In #3226, we added a new command that allow Kani to verify properties in a custom standard library. In this PR, we create a script test that create a modified version of the standard library and runs Kani against it. I also moved the script based tests to run after the more generic regression jobs. I think the script jobs are a bit harder to debug, they may take longer, and they are usually very specific to a few features. So probably best if we run the more generic tests first.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Create an unstable sub-command that users can invoke to verify a local version of the standard library.
Something like:
The text was updated successfully, but these errors were encountered: