-
Notifications
You must be signed in to change notification settings - Fork 84
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
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
kani fails to untar on Ubuntu 24.04
[C] Bug
This is a bug. Something isn't working.
#3248
opened Jun 10, 2024 by
agvallejo
Valid value checks does not check This is a bug. Something isn't working.
char
surrogate values
[C] Bug
#3241
opened Jun 7, 2024 by
celinval
Property representing This is a bug. Something isn't working.
unreachable!()
is marked as SUCCESS instead of UNREACHABLE
[C] Bug
#3240
opened Jun 7, 2024 by
celinval
Contracts: macro allowing for contraction of specific variables
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
Kani fails to detect use of a dangling pointer dereference in println
[C] Bug
This is a bug. Something isn't working.
[F] Soundness
Kani failed to detect an issue
#3235
opened Jun 6, 2024 by
jsalzbergedu
Contract unexpectedly fails
[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
Disallow side effects in contract expressions
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
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
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
3 tasks
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
Unexpected failure when This is a bug. Something isn't working.
modifies
attribute points to a ZST
[C] Bug
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
#3163
opened Apr 25, 2024 by
Necromaticon
Enable Kani to verify the standard library crates
#3152
opened Apr 19, 2024 by
celinval
1 of 4 tasks
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
Avoid weaker comparison for targets in Tracks some internal work. I.e.: Users should not be affected.
run_cargo
[C] Internal
#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.
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
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
Previous Next
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.