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

507 Open 1,020 Closed
507 Open 1,020 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

Create an API for loop contracts [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3168 opened May 1, 2024 by qinheping
--tests flag should enable #[test] attributes and behavior [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3163 opened Apr 25, 2024 by Necromaticon
2
Toolchain upgrade to nightly-2024-04-22 failed
#3161 opened Apr 23, 2024 by github-actions bot
1
6
Create a #[no_core] Kani library
#3153 opened Apr 19, 2024 by celinval
@celinval
Enable Kani to verify the standard library crates
#3152 opened Apr 19, 2024 by celinval
4 tasks
@celinval
1
Add support for uninterpreted function stub [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests
#3112 opened Mar 27, 2024 by celinval
2
Avoid weaker comparison for targets in run_cargo [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#3111 opened Mar 26, 2024 by adpaco-aws
Concrete playback tests could include more information [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. T-User Tag user issues / requests
#3110 opened Mar 26, 2024 by adpaco-aws
Missing modifies clause triggers very confusing error [C] Bug This is a bug. Something isn't working.
#3106 opened Mar 25, 2024 by celinval Function Contracts MVP
Kani symbols not available in path dependency when build script depends on same local crate [C] Bug This is a bug. Something isn't working. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. T-User Tag user issues / requests
#3101 opened Mar 22, 2024 by xarantolus
1
Spurious failures caused by handling of storage markers [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.
#3099 opened Mar 21, 2024 by zhassan-aws
1
1
Add support to type invariants [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3095 opened Mar 19, 2024 by celinval
@feliperodri
Create std contracts regression [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#3094 opened Mar 19, 2024 by celinval
@celinval
Kani should detect Rust specific undefined behavior [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3089 opened Mar 18, 2024 by celinval
3 tasks
Kani fails to detect for loop bound after upgrade to nightly-2024-03-15 [C] Bug This is a bug. Something isn't working. T-High Priority Tag issues that have high priority
#3088 opened Mar 18, 2024 by celinval
Migrate stubbing transformation to be performed in the instance body [C] Internal Tracks some internal work. I.e.: Users should not be affected. [I] Refactoring / Clean Up Refactoring or cleaning up of existing code
#3072 opened Mar 12, 2024 by celinval
Kani crashes when coverage is enabled and an unwind assertion fails [C] Bug This is a bug. Something isn't working.
#3070 opened Mar 11, 2024 by zhassan-aws
@adpaco-aws
1
Handle new F16 and F128 types [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3069 opened Mar 11, 2024 by zhassan-aws
1
Remove --enable-unstable [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.
#3068 opened Mar 11, 2024 by celinval
Cleanup flow to setup cargo kani [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#3060 opened Mar 6, 2024 by jaisnan
@jaisnan
How to pass target-feature in cargo-kani? [C] Bug This is a bug. Something isn't working.
#3059 opened Mar 6, 2024 by zpzigi754
6
Document how to debug slowness of the proof
#3041 opened Feb 22, 2024 by Kixunil
3
Out of memory with Kani 0.46.0 on an s2n-quic harness [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Performance Track performance improvement (Time / Memory / CPU) T-High Priority Tag issues that have high priority T-User Tag user issues / requests
#3030 opened Feb 15, 2024 by zhassan-aws
@tautschnig
11
crates.io stub and docs.rs documentation [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3029 opened Feb 14, 2024 by GrigorenkoPV
3
Contracts: Can't include non-Copy types in contract [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#3027 opened Feb 13, 2024 by adpaco-aws
@feliperodri
4
ProTip! Type g i on any issue or pull request to go back to the issue listing page.