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

500 Open 1,069 Closed
500 Open 1,069 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

Add core intrisincs tests for f16 and f128 [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#3308 opened Jun 28, 2024 by jaisnan
@jaisnan
UX Improvement: Ensures clause requires type annotation [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3304 opened Jun 28, 2024 by celinval Function Contracts
1
@pi314mm
1
Toolchain upgrade to nightly-2024-06-28 failed
#3303 opened Jun 28, 2024 by github-actions bot
1
Tracking Issue: Automatically Verify Memory Initialization [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-TrackingIssue Issues used to track a large amount of work related to a feature
#3300 opened Jun 27, 2024 by artemagvanian
8 tasks
@artemagvanian
5
Mutable static variables usage in contract verification trigger UB [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.
#3298 opened Jun 27, 2024 by celinval Function Contracts
2
Contract implementation is unsafe and may trigger UB [C] Bug This is a bug. Something isn't working.
#3293 opened Jun 25, 2024 by celinval Function Contracts
CBMC upgrade to 6.0.1 failed
#3287 opened Jun 24, 2024 by github-actions bot
Add support to Z3 [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3277 opened Jun 19, 2024 by celinval
1
Function Contracts: Better error messages [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3273 opened Jun 18, 2024 by pi314mm Function Contracts
Ensure that Arbitrary respects Invariant somehow [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.
#3265 opened Jun 13, 2024 by adpaco-aws
Reachability analysis cannot see through FFI [C] Bug This is a bug. Something isn't working.
#3263 opened Jun 12, 2024 by tautschnig
Review where we might be incorrectly ignoring projects into ZSTs [C] Bug This is a bug. Something isn't working.
#3262 opened Jun 12, 2024 by tautschnig
Cleanup work due to enabling standard library verification [C] Internal Tracks some internal work. I.e.: Users should not be affected. [I] Refactoring / Clean Up Refactoring or cleaning up of existing code
#3257 opened Jun 11, 2024 by celinval
5 tasks
@celinval @jaisnan
Valid value checks does not check char surrogate values [C] Bug This is a bug. Something isn't working.
#3241 opened Jun 7, 2024 by celinval
@adpaco-aws
Property representing unreachable!() is marked as SUCCESS instead of UNREACHABLE [C] Bug This is a bug. Something isn't working.
#3240 opened Jun 7, 2024 by celinval
Contract fails due to promoted constants being havocked [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-High Priority Tag issues that have high priority
#3228 opened Jun 4, 2024 by zhassan-aws Function Contracts
1
12
Disallow side effects in contract expressions [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3213 opened May 30, 2024 by pi314mm Function Contracts
@feliperodri
3
Error when annotating an associated function with a contract [C] Bug This is a bug. Something isn't working. T-High Priority Tag issues that have high priority
#3206 opened May 28, 2024 by zhassan-aws Function Contracts
4
Implement validity checks for unsupported constructs [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3203 opened May 27, 2024 by celinval
4 tasks
@celinval
1
Add support to shadow memory [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3184 opened May 15, 2024 by celinval
@celinval @zhassan-aws
Unexpected failure when modifies attribute points to a ZST [C] Bug This is a bug. Something isn't working.
#3181 opened May 14, 2024 by celinval Function Contracts
@feliperodri
2
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
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
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.