Allow items to be anonymous #3300
Labels
A-frontend
Area: Compiler frontend (errors, parsing and HIR)
C-cleanup
Category: PRs that clean code up or issues documenting cleanup.
Comments
|
Not critical for 0.6, de-milestoning |
|
This seems to be obsolete, since we don't have anonymous foreign mods anymore. |
estebank
added a commit
to estebank/rust
that referenced
this issue
Dec 22, 2016
Removed FIXME comment referencing rust-lang#3300.
bors
added a commit
that referenced
this issue
Dec 22, 2016
Remove outdated FIXME comment Removed outdated FIXME comment referencing #3300 to allow anonymous items.
RalfJung
pushed a commit
to RalfJung/rust
that referenced
this issue
Feb 17, 2024
Rustup With rust-lang#121035 landed we can rustfmt format `async FnOnce`.
jaisnan
pushed a commit
to jaisnan/rust-dev
that referenced
this issue
Jul 29, 2024
This PR enables automatic memory initialization proofs for raw pointers in Kani. This is done without any extra instrumentation from the user. Currently, due to high memory consumption and only partial support of pointee types for which memory initialization proofs work, this feature is gated behind `-Z uninit-checks` flag. Note that because it uses shadow memory under the hood, programs using this feature need to pass `-Z ghost-state` flag as well. This PR is a part of working towards rust-lang#3300. 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: Celina G. Val <celinval@amazon.com>
jaisnan
pushed a commit
to jaisnan/rust-dev
that referenced
this issue
Jul 29, 2024
…cks (rust-lang#3313) This is a follow-up PR for rust-lang#3264, a part of the larger work towards rust-lang#3300. This PR introduces: - Use of demonic non-determinism (prophecy variables) to improve memory initialization checks performance; - Instead of keeping track of memory initialization of each possibly uninitialized byte pointed to by some pointer, one is chosen non-deterministically; - Tests for proper memory initialization checks injection for compiler intrinsics; - Separate functions for checking memory initialization of slice chunks. 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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
jaisnan
pushed a commit
to jaisnan/rust-dev
that referenced
this issue
Jul 29, 2024
… reinstrumentation (rust-lang#3344) Recently added memory initialization checks (see rust-lang#3300 for an overview) code suffers from re-instrumentation due to automatically added pointer checks to the instrumentation code. This PR adds an internal `kanitool::disable_checks` attribute to disable automatically generated CBMC checks inside internal instrumentation. This, in turn, relies on CBMC pragmas (https://www.cprover.org/cprover-manual/properties/#usinggotoinstrument). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Right now, if we have an anonymous item, we use a dummy ident for its
identfield in the AST. This should really be an option, since for example, anonymous foreign mods will soon be allowed.The text was updated successfully, but these errors were encountered: