-
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
ICE: This is a bug. Something isn't working.
[F] Crash
Kani crashed
failed to resolve instance for <dyn ThriftService as ThriftService>::foo
[C] Bug
#3494
opened Sep 5, 2024 by
matthiaskrgr
Upgrade upload-artifact and download-artifact actions
[C] Internal
Tracks some internal work. I.e.: Users should not be affected.
[I] CI / Infrastructure
Work done to CI, tests and infrastructure.
T-High Priority
Tag issues that have high priority
#3492
opened Sep 4, 2024 by
zhassan-aws
Stacked Borrows In Kani -- Extend Feature to handle more code
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
#3475
opened Aug 30, 2024 by
jsalzbergedu
Enums that are #[repr(u8)] are slower than u8
[C] Bug
This is a bug. Something isn't working.
#3471
opened Aug 30, 2024 by
jsalzbergedu
ICE Resolving This is a bug. Something isn't working.
Z-Contracts
Issue related to code contracts
proof_for_contract
target
[C] Bug
Fast fail
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
T-User
Tag user issues / requests
#3458
opened Aug 24, 2024 by
cospectrum
Confusing coverage result: Uncovered argument for This is a bug. Something isn't working.
[E] User Experience
An UX enhancement for an existing feature. Including deprecation of an existing one.
[F] Spurious Failure
Issues that cause Kani verification to fail despite the code being correct.
Z-UnstableFeature
Issues that only occur if a unstable feature is enabled
match
[C] Bug
#3456
opened Aug 20, 2024 by
adpaco-aws
Confusing coverage result: Uncovered end of block on This is a bug. Something isn't working.
[E] User Experience
An UX enhancement for an existing feature. Including deprecation of an existing one.
[F] Spurious Failure
Issues that cause Kani verification to fail despite the code being correct.
Z-UnstableFeature
Issues that only occur if a unstable feature is enabled
if
statement
[C] Bug
#3455
opened Aug 20, 2024 by
adpaco-aws
thread 'main' panicked at ...kani-verifier-0.54.0/src/lib.rs:156:38: No exit code?
#3451
opened Aug 19, 2024 by
weaversa
ICE: This is a bug. Something isn't working.
missing tokens for node: Expr
[C] Bug
#3446
opened Aug 16, 2024 by
matthiaskrgr
Coverage metadata should include mappings for all source code
[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.
#3445
opened Aug 16, 2024 by
adpaco-aws
Rust's coverage instrumentation assumes function calls never panic
[C] Bug
This is a bug. Something isn't working.
[F] Soundness
Kani failed to detect an issue
Z-UnstableFeature
Issues that only occur if a unstable feature is enabled
#3441
opened Aug 15, 2024 by
adpaco-aws
Move kani APIs that are visible only to the compiler to a private Tracks some internal work. I.e.: Users should not be affected.
[I] Refactoring / Clean Up
Refactoring or cleaning up of existing code
instrumentation
module
[C] Internal
#3440
opened Aug 15, 2024 by
celinval
Fix Kani Std check not running on Tracks some internal work. I.e.: Users should not be affected.
features/verify-rust-std
[C] Internal
#3437
opened Aug 13, 2024 by
jaisnan
Adding regressions tests for output based on output configuration
[C] Internal
Tracks some internal work. I.e.: Users should not be affected.
#3412
opened Aug 4, 2024 by
Alexander-Aghili
Can't resolve incoherent impls
[C] Bug
This is a bug. Something isn't working.
#3404
opened Aug 1, 2024 by
carolynzech
The 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.
Z-Contracts
Issue related to code contracts
#[safety_constraint(...)]
can be specified without deriving Arbitrary
or Invariant
[C] Feature / Enhancement
#3396
opened Jul 30, 2024 by
adpaco-aws
question: semantics of rust
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
#3385
opened Jul 25, 2024 by
florianschanda
Add support for transitive modifies clause
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
Z-Contracts
Issue related to code contracts
Contract requirement not respected
[C] Bug
This is a bug. Something isn't working.
Z-Contracts
Issue related to code contracts
Remove terse output requirement for parallel jobs
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
T-User
Tag user issues / requests
#3357
opened Jul 18, 2024 by
Alexander-Aghili
Harness Output in Individual Files
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
#3356
opened Jul 18, 2024 by
Alexander-Aghili
Function Contracts: Modifies for str
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
Z-Contracts
Issue related to code contracts
Previous Next
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.