You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It looks like this is due to the basic block containing the loop condition being a parent of the loop body, so when we run all the cleanups for ret or break it runs the condition's cleanups (a 2nd time).
…ip1995
Add new lint "missing_panics_doc"
fixesrust-lang#1974
changelog: Added the "missing_panics_doc" lint which lints when public functions that may panic are missing "# Panics" in their doc comment
celinval
added a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
…ler (rust-lang#1956)
This PR is a pre-req for getting a per-harness reachability algorithm. First we need to stop treating all goto generated by the compiler as the same model which is what this PR does.
For that, I introduce the concept of a project, which is basically a container of artifacts produced by the build system. The goal is to abstracts the verification code from the build system we pick. It also provide methods to get artifacts relevant to a harness. Today this method will return the artifact related to the crate where it is contained, but in the future it can be easily modified to be the harness specific goto model.
The only behavioral change in this PR is that we disabled `--gen-c` for `--function` and `--legacy-linker` to simplify the code since all these options are for internal usage or on track to be deleted.
This change also fixes inconsistent / incorrect behaviors. They are the following:
1. Kani is now sound when two or more targets contains harnesses or no mangled functions that have the same name (rust-lang#1974). Note that this is not the case for `--legacy-linker` and `--function` options.
2. `kani` now respects the `--target-dir` argument provided by the customer.
3. `kani` no longer crash when the crate has no harness (rust-lang#1910).
Co-authored-by: Zyad Hassan <[email protected]>
When I try to run the following program it crashes with an error message from glibc.
The error message is
I tried running the program with valgrind. It then produced a different error message:
If I change the loop to "while true", the program finishes without error.
The text was updated successfully, but these errors were encountered: