-
Notifications
You must be signed in to change notification settings - Fork 507
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.
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
Add Kani to CI. #798
Merged
LucioFranco
merged 2 commits into
tokio-rs:master
from
YoshikiTakashima:kani-integration
Jan 17, 2023
Merged
Add Kani to CI. #798
LucioFranco
merged 2 commits into
tokio-rs:master
from
YoshikiTakashima:kani-integration
Jan 17, 2023
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* Added kani integration. * Fix yaml problem. * yaml hash problem * No need to cd? * Use new release, not the hash * Added comment describing the unwind value. Co-authored-by: Yoshiki Takashima <[email protected]>
LucioFranco
approved these changes
Jan 17, 2023
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you @YoshikiTakashima for following up on this! Ill merge this to just get it going, but would you be willing to add somewhere in the readme the commands to run the kani tests locally?
Merged
Jasperav
added a commit
to Jasperav/prost
that referenced
this pull request
Jun 8, 2023
* Allow file descriptor be generated without --include_source_info (tokio-rs#786) * Allow file descriptor be generated without --include_source_info The file descriptor sets generated by rules_proto in bazel don't have this by default, so this allows some flexibility for users to reuse results that are already available to them. It's fairly trivial adjustment so it seemed reasonable to me to allow the flexibility. * revert breaking changes and add default * release 0.11.5 (tokio-rs#788) * Add message and enum attributes to prost-build (tokio-rs#784) closes tokio-rs#783 * chore: Prepare 0.11.6 release (tokio-rs#794) * chore: Added Kani to CI. (#1) (tokio-rs#798) * Added Kani documentation. (tokio-rs#799) * Fix issue with negative nanos in Duration::try_from(), and add tests (tokio-rs#803) * Fix issue with negative nanos in Duration::try_from(), and add a unit test * add proptest for negative nanos * PR comment: remove spurious dbg * Prevent spurious overflow in check_duration_roundtrip test (tokio-rs#804) Co-authored-by: Lucio Franco <[email protected]> * Clarify `default_package_filename` documentation. (tokio-rs#809) * Bump msrv to 1.60 (tokio-rs#814) * chore(types): Remove including generated code (tokio-rs#801) * chore: Update github action (tokio-rs#815) Co-authored-by: Lucio Franco <[email protected]> * chore: Add cargo-machete to detect unused dependencies (tokio-rs#817) * chore: Update msrv to 1.60 (tokio-rs#818) * feat: Added try_normalize to Timestamp (tokio-rs#796) Co-authored-by: Lucio Franco <[email protected]> * Update PropProof docs to note the need to submodule init (tokio-rs#805) Co-authored-by: Lucio Franco <[email protected]> * feat(build): Add direct fds compile support (tokio-rs#819) This commit adds two new compile functions that allow passing a `FileDescriptorSet` and it will generate the Rust code. This allows users to use libraries like `protox` directly and in an ergonomic way. * release 0.11.7 (tokio-rs#821) * fix: correct change in visibility of compiler module (tokio-rs#824) Introduced in tokio-rs#801 Closes tokio-rs#823 * release 0.11.8 (tokio-rs#825) * Add existing roundtrip test to Kani CI and avoid recursive submoduling (tokio-rs#828) * Add existing roundtrip test to Kani CI * Bump up Kani version * Remove `v` from GA version * Update to `syn@2` & `[email protected]` (tokio-rs#833) * Fix corrupted tests and missing CI testing (tokio-rs#832) Co-authored-by: Lucio Franco <[email protected]> * chore: Update to criterion 0.4 (tokio-rs#835) * Fix build in directory not named `prost` (tokio-rs#839) This library will fail to build with the following error when checked out into a directory not named exactly `prost`: error: failed to load manifest for workspace member `/home/alex/src/prost-rs/tests/single-include` Caused by: failed to load manifest for dependency `prost` Caused by: failed to read `/home/alex/src/prost/Cargo.toml` Caused by: No such file or directory (os error 2) This is because the `single-include` test depends on `prost` with the path `../../../prost`. This patch fixes the issue by correcting the path to `../..`. * prost-build: support boxing fields (tokio-rs#802) This allows the user to request boxing of specific fields. This is useful for enum types that might have variants of very different size. * chore: Update to baptiste0928/cargo-install@v2 (tokio-rs#840) Co-authored-by: Lucio Franco <[email protected]> * Fix typo in bail message (tokio-rs#848) --------- Co-authored-by: David Freese <[email protected]> Co-authored-by: Lucio Franco <[email protected]> Co-authored-by: damel_lp <[email protected]> Co-authored-by: Yoshiki Takashima <[email protected]> Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> Co-authored-by: Gilad Naaman <[email protected]> Co-authored-by: tottoto <[email protected]> Co-authored-by: Oliver Browne <[email protected]> Co-authored-by: Marcus Griep <[email protected]> Co-authored-by: Adrian Palacios <[email protected]> Co-authored-by: Donough Liu <[email protected]> Co-authored-by: Alex O'Brien <[email protected]> Co-authored-by: Thomas Orozco <[email protected]> Co-authored-by: Brendon Daugherty <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds Kani to the CI as previously discussed with @LucioFranco.
tests::check_timestamp_roundtrip_via_system_time
proptest harness. We focused on this harness because it was involved in bug MalformedTimestamp
leads to Debug Assert Crash 'attempt to negate with overflow' inimpl TryFrom<Timestamp> for std::time::SystemTime
#682prost-types
are blocked by Kani issue 274. We are working to implement the required features to resolve 274 and we will submit a second PR to enable these harnesses once Kani implements the feature.prost-types
will be difficult to support within GitHub Actions due to Kani's large memory consumption when running these harnesses.