Skip to content

Issues: model-checking/kani

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.

Sign up for GitHub

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

534 Open 1,201 Closed
534 Open 1,201 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Toolchain upgrade to nightly-2024-12-20 failed
#3811 opened Jan 3, 2025 by github-actions bot
1
Cannot use multiple #[stub_verified(..)] attributes to a single harness [C] Bug This is a bug. Something isn't working.
#3804 opened Jan 1, 2025 by ShoyuVanilla
2
No clear CEC functionality or cached operation [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3803 opened Dec 31, 2024 by TomMD
2
Proof harness crashes when verifying a function with a &mut FnMut argument [C] Bug This is a bug. Something isn't working.
#3799 opened Dec 29, 2024 by BusyBeaver-42
@remi-delmas-3000
proof_for_contract much slower than proof (or even runs out of memory) [C] Bug This is a bug. Something isn't working. [E] Performance Track performance improvement (Time / Memory / CPU) T-User Tag user issues / requests
#3797 opened Dec 27, 2024 by BusyBeaver-42
4
proof_for_contract rejects code accepted by proof [C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. T-CBMC Issue related to an existing CBMC issue T-User Tag user issues / requests
#3796 opened Dec 27, 2024 by BusyBeaver-42
1
@remi-delmas-3000
5
Concrete playback feature generates tests that fail Kani assertions [C] Bug This is a bug. Something isn't working. T-User Tag user issues / requests
#3787 opened Dec 16, 2024 by gogdavz
1
Add support for Coroutine Closures [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct
#3783 opened Dec 16, 2024 by carolynzech
Concise list subcommand option that groups by module [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3779 opened Dec 13, 2024 by carolynzech
@carolynzech
Kani module stubs for development [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests
#3778 opened Dec 13, 2024 by ajrudzitis
Can't write contracts for a method defined inside more than one impl block [C] Bug This is a bug. Something isn't working. Z-Contracts Issue related to code contracts
#3773 opened Dec 11, 2024 by carolynzech Function Contracts
@celinval
2
Value-dependent failure with vec! initialization [C] Bug This is a bug. Something isn't working. T-User Tag user issues / requests
#3772 opened Dec 11, 2024 by lancelet
2
Recursion unwinding does not terminate [C] Bug This is a bug. Something isn't working.
#3771 opened Dec 10, 2024 by thanhnguyen-aws
5
Set Kani's --default-unwind to 1 [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests
#3769 opened Dec 9, 2024 by celinval
Casting pointer to usize and back have unexpected behavior [C] Bug This is a bug. Something isn't working.
#3765 opened Dec 7, 2024 by celinval
1
Can't write contracts for functions that return mutable references to input arguments [C] Bug This is a bug. Something isn't working.
#3764 opened Dec 6, 2024 by carolynzech Function Contracts
Limitation in Annotating Function Contracts for Pointers to dyn Trait [C] Bug This is a bug. Something isn't working.
#3763 opened Dec 5, 2024 by xsxszab
Add support to validity checks in the presence of copy_nonoverlapping, copy. [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3762 opened Dec 5, 2024 by celinval
Validity for enumerations with multiple variants. [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3761 opened Dec 5, 2024 by celinval
Implement validity check for FnPtr [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3760 opened Dec 5, 2024 by celinval
Extend validity checks for references and Box [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3759 opened Dec 5, 2024 by celinval
Kani does not detect UB for ptr_offset_from and ptr_offset_from_unsigned [C] Bug This is a bug. Something isn't working. [E] Unsupported UB Undefined behavior that Kani does not detect [F] Soundness Kani failed to detect an issue
#3756 opened Dec 5, 2024 by celinval
1
Abnormal Test Failure with Pointer Generator in Rust Standard Library Verification [C] Bug This is a bug. Something isn't working.
#3743 opened Nov 27, 2024 by xsxszab
Check vtable validity when explicitly creating wide pointer [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported UB Undefined behavior that Kani does not detect
#3738 opened Nov 25, 2024 by celinval
Compilation Error When Stubbing Functions That Return Pointers Using Function Contracts [C] Bug This is a bug. Something isn't working.
#3732 opened Nov 23, 2024 by xsxszab
1
ProTip! Find all open issues with in progress development work with linked:pr.