-
Notifications
You must be signed in to change notification settings - Fork 13k
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
Can't use left shift on enum discriminants #1659
Labels
E-easy
Call for participation: Easy difficulty. Experience needed to fix: Not much. Good first issue.
Comments
The shift operators are missing from |
Thanks, marijnh |
brson
added a commit
that referenced
this issue
Jan 25, 2012
celinval
added a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
Kani compiler used to generate one `goto-program` for all harnesses in one crate. In some cases, this actually had a negative impact on the harness verification time. This was first reported in rust-lang#1659 The main changes were done in the compiler's module `compiler_interface` and the module `project` from the driver. The compiler will now gather all the harnesses beforehand and it will perform reachability + codegen steps for each harness. All files related to a harness `goto-program` will follow the naming convention bellow: ``` <BASE_NAME>_<MANGLED_NAME>.<EXTENSION> ``` This applies to symtab / goto / type_map / restriction files. The metadata file is still generated once per target crate, and its name is still the same (`<BASE_NAME>.kani-metadata.json`). On the driver side, the way we process the artifacts have changed. The driver will now read the metadata for each crate, and collect all artifacts based on the symtab goto file that is recorded in the metadata of each harness. These changes do not apply for `--function`. We still keep all artifacts based on the crate's `<BASE_NAME>` and we have a separate logic to handle that. Fixing this is captured by rust-lang#2129.
celinval
added a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
This adds an executor (scheduler for async futures) to the Kani library, thus supporting `kani::spawn` as a replacement for `tokio::spawn`. It also includes `kani::yield_now` which is similar to `tokio::yield_now`. Co-authored-by: Celina G. Val <celinval@amazon.com>
celinval
added a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
…unctions (rust-lang#1661) Instead of having to manually wrap the code in `kani::spawnable_block_on` as in rust-lang#1659, this PR allows `#[kani::proof]` to be applied to harnesses that use `spawn` as well. For this to happen, the user has to specify a scheduling strategy. Co-authored-by: Celina G. Val <celinval@amazon.com>
Kobzol
pushed a commit
to Kobzol/rust
that referenced
this issue
Dec 30, 2024
bors
pushed a commit
to rust-lang-ci/rust
that referenced
this issue
Jan 2, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
E-easy
Call for participation: Easy difficulty. Experience needed to fix: Not much. Good first issue.
The text was updated successfully, but these errors were encountered: