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

499 Open 1,134 Closed
499 Open 1,134 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

Toolchain upgrade to nightly-2024-09-13 failed
#3525 opened Sep 18, 2024 by github-actions bot
1
CBMC upgrade to 6.2.0 failed
#3507 opened Sep 9, 2024 by github-actions bot
ICE: failed to resolve instance for <dyn ThriftService as ThriftService>::foo [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#3494 opened Sep 5, 2024 by matthiaskrgr
1
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
2
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
2
ICE Resolving proof_for_contract target [C] Bug This is a bug. Something isn't working. Z-Contracts Issue related to code contracts
#3467 opened Aug 29, 2024 by carolynzech Function Contracts
2
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
1
Confusing coverage result: Uncovered argument for match [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. [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
#3456 opened Aug 20, 2024 by adpaco-aws
Confusing coverage result: Uncovered end of block on if statement [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. [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
#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
4
ICE: missing tokens for node: Expr [C] Bug This is a bug. Something isn't working.
#3446 opened Aug 16, 2024 by matthiaskrgr
2
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 instrumentation module [C] Internal Tracks some internal work. I.e.: Users should not be affected. [I] Refactoring / Clean Up Refactoring or cleaning up of existing code
#3440 opened Aug 15, 2024 by celinval
Fix Kani Std check not running on features/verify-rust-std [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#3437 opened Aug 13, 2024 by jaisnan
@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 #[safety_constraint(...)] can be specified without deriving Arbitrary or Invariant [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. Z-Contracts Issue related to code contracts
#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
3
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
#3372 opened Jul 23, 2024 by celinval Function Contracts
1
Contract requirement not respected [C] Bug This is a bug. Something isn't working. Z-Contracts Issue related to code contracts
#3370 opened Jul 22, 2024 by celinval Function Contracts
1
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
2
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
1
5
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
#3349 opened Jul 16, 2024 by pi314mm Function Contracts
ProTip! Type g i on any issue or pull request to go back to the issue listing page.