Skip to content
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

Implement check for write_bytes #3108

Merged
merged 5 commits into from
Apr 5, 2024

Conversation

celinval
Copy link
Contributor

In the previous PR #3085, we did not support checks for write_bytes which is added in this PR.

I am waiting for #3092 to add expected tests.

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

Create a value of `[val; size_of::<T>()]` and check if it is a valid
combination of bytes for T.
@celinval celinval requested a review from a team as a code owner March 26, 2024 00:24
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Mar 26, 2024
@tautschnig tautschnig merged commit b329c85 into model-checking:main Apr 5, 2024
23 checks passed
celinval added a commit that referenced this pull request Apr 17, 2024
Release notes are the following:

### Major Changes
* Fix compilation issue with proc_macro2  (v1.0.80+) and Kani v0.49.0
(#3138).

### What's Changed
* Implement valid value check for `write_bytes` by @celinval in
#3108
* Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval

**Full Changelog**:
kani-0.49.0...kani-0.50.0
zpzigi754 pushed a commit to zpzigi754/kani that referenced this pull request May 8, 2024
In the previous PR model-checking#3085, we did not support checks for `write_bytes`
which is added in this PR.

I am waiting for model-checking#3092 to add expected tests.
zpzigi754 pushed a commit to zpzigi754/kani that referenced this pull request May 8, 2024
Release notes are the following:

### Major Changes
* Fix compilation issue with proc_macro2  (v1.0.80+) and Kani v0.49.0
(model-checking#3138).

### What's Changed
* Implement valid value check for `write_bytes` by @celinval in
model-checking#3108
* Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval

**Full Changelog**:
model-checking/kani@kani-0.49.0...kani-0.50.0
qinheping pushed a commit to qinheping/kani that referenced this pull request May 9, 2024
Release notes are the following:

### Major Changes
* Fix compilation issue with proc_macro2  (v1.0.80+) and Kani v0.49.0
(model-checking#3138).

### What's Changed
* Implement valid value check for `write_bytes` by @celinval in
model-checking#3108
* Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval

**Full Changelog**:
model-checking/kani@kani-0.49.0...kani-0.50.0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants