Skip to content

Issues: model-checking/kani

Beta
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

503 Open 1,306 Closed
503 Open 1,306 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Static union values can panic kani [C] Bug This is a bug. Something isn't working. T-User Tag user issues / requests
#4097 opened May 22, 2025 by teskje
1
@thanhnguyen-aws
2
Invoke cargo once to build all packages in the workspace [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#4094 opened May 21, 2025 by celinval
Kani not resolving qualified paths in verify-std [C] Bug This is a bug. Something isn't working. T-User Tag user issues / requests Z-Contracts Issue related to code contracts
#4084 opened May 18, 2025 by dawidl022
@carolynzech
Kani always rebuilds when running verify-std [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests
#4079 opened May 16, 2025 by dawidl022
2
Add a debug option to generate a flamegraph for compiler performance [C] Internal Tracks some internal work. I.e.: Users should not be affected. [E] Performance Track performance improvement (Time / Memory / CPU)
#4075 opened May 14, 2025 by carolynzech
2
Investigate why contracts don't use resolve_fn_path [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. Z-Contracts Issue related to code contracts
#4057 opened May 7, 2025 by carolynzech
Autoharness include/exclude pattern does not support whitespace [C] Bug This is a bug. Something isn't working. Z-Autoharness Issue related to autoharness subcommand
#4046 opened Apr 25, 2025 by tautschnig
@carolynzech
1
Spurious failure in tests/kani/FunctionContracts/modify_slice_elem.rs [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.
#4029 opened Apr 17, 2025 by zhassan-aws
Redundancy between BoundedArbitrary Vec implementation and kani::any_vec [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.
#4027 opened Apr 17, 2025 by sgpthomas
Document & stabilize the list subcommand [C] Documentation Additions and improvements to our documentation [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-Good First Issue Good for newcomers
#4026 opened Apr 17, 2025 by carolynzech
@carolynzech
Verification results of #[proof] and #[proof_for_contract] are different [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests Z-Contracts Issue related to code contracts
#4021 opened Apr 15, 2025 by zjp-CN
2
goto-cc crash when there are two quantifers in one proof [C] Bug This is a bug. Something isn't working. T-CBMC Issue related to an existing CBMC issue
#4020 opened Apr 15, 2025 by qinheping
@qinheping
Kani crashes on https://github.com/DataDog/libdatadog [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-High Priority Tag issues that have high priority T-User Tag user issues / requests
#4007 opened Apr 10, 2025 by danielsn
1
@carolynzech @zhassan-aws @thanhnguyen-aws
8
Docs mention the removed function kani::expect_fail [C] Documentation Additions and improvements to our documentation
#3999 opened Apr 7, 2025 by sgpthomas
kani-cov is not documented [C] Documentation Additions and improvements to our documentation [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3987 opened Apr 3, 2025 by carolynzech
Create a release bundle with an older glibc [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3977 opened Apr 2, 2025 by zhassan-aws
#[kanitool::is_contract_generated] attribute is not detected [C] Internal Tracks some internal work. I.e.: Users should not be affected. Z-Contracts Issue related to code contracts
#3921 opened Mar 5, 2025 by carolynzech
2
Tracking issue for stable MIR panic with GlobalAsm [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#3919 opened Mar 5, 2025 by remi-delmas-3000
2
Kani gives confusing error message for no_std crates [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#3906 opened Feb 25, 2025 by zhassan-aws
3
Function contract doesn't propagate const function bodies correctly [C] Bug This is a bug. Something isn't working. Z-Contracts Issue related to code contracts
#3905 opened Feb 24, 2025 by thanhnguyen-aws
5
Delayed UB instrumentation regression: slices [C] Bug This is a bug. Something isn't working.
#3881 opened Feb 10, 2025 by carolynzech
2
Tracking Issue: Disabling CBMC's NaN checks [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct.
#3875 opened Feb 5, 2025 by rajath-mk
Support loop modifies in loop contracts [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3871 opened Feb 3, 2025 by qinheping
1
Support dereference in loop contracts [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#3866 opened Jan 30, 2025 by zhassan-aws
Failed Checks: Check that ptr is freeable [C] Bug This is a bug. Something isn't working.
#3864 opened Jan 29, 2025 by thanhnguyen-aws
ProTip! Adding no:label will show everything without a label.