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

519 Open 1,184 Closed
519 Open 1,184 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

Compilation Error When Stubbing Functions That Return Pointers Using Function Contracts [C] Bug This is a bug. Something isn't working.
#3732 opened Nov 23, 2024 by xsxszab
1
Toolchain upgrade to nightly-2024-11-20 failed
#3731 opened Nov 21, 2024 by github-actions bot
Add support for dev setup on Ubuntu 24.04 [C] Bug This is a bug. Something isn't working. T-User Tag user issues / requests
#3728 opened Nov 19, 2024 by rafaelsamenezes
1
Compilation error when using string in assert [C] Bug This is a bug. Something isn't working.
#3717 opened Nov 15, 2024 by zhassan-aws
Add support for in_range [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests
#3711 opened Nov 12, 2024 by Yenyun035
@zhassan-aws
1
Kani misses out of bounds index for get_unchecked with raw pointer to slice [C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue
#3707 opened Nov 11, 2024 by carolynzech
@celinval
5
Support struct field accessing in loop contracts [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3700 opened Nov 8, 2024 by qinheping
@qinheping
loop_old in loop contracts [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3697 opened Nov 8, 2024 by qinheping
@qinheping
1
Generate non-deterministic pointer variables [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3696 opened Nov 8, 2024 by stogaru
Propose new Kani API to compare two objects byte-by-byte [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3693 opened Nov 7, 2024 by QinyuanWu
2
Failed to use loop contracts to prove contracts harness for proofs with nested loops [C] Bug This is a bug. Something isn't working.
#3685 opened Nov 5, 2024 by qinheping
@qinheping
Failed to stub_verified contracts with slices in kani::modifies [C] Bug This is a bug. Something isn't working.
#3682 opened Nov 5, 2024 by qinheping
Add option --stack-trace to print the stack trace of a failure [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.
#3681 opened Nov 4, 2024 by celinval
1
Crash in CBMC output parser with aws-lc-sys crate [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#3679 opened Nov 4, 2024 by zhassan-aws
5
Proposal for new Kani API similar to CPROVER_r_ok and CPROVER_w_ok [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3672 opened Nov 1, 2024 by QinyuanWu
3
Spurious failure due to pointer operation returning non-deterministic value for dangling pointer [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-CBMC Issue related to an existing CBMC issue
#3670 opened Nov 1, 2024 by celinval
14
Feature Request: Support for Unsized Types in kani::mem::same_allocation API [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3663 opened Oct 30, 2024 by xsxszab
Support deriving kani::Invariant for enums [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3647 opened Oct 25, 2024 by carolynzech
Disable floating-point overflow checks
#3620 opened Oct 20, 2024 by cospectrum
9
Kani miss overflow when computing size_of_val [C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue
#3616 opened Oct 18, 2024 by celinval
@celinval
ICE: Kani compiler crashes when invoking from_raw_parts for slices [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#3615 opened Oct 18, 2024 by celinval
@carolynzech
2
High memory consumption for interior mutability function contract test [C] Bug This is a bug. Something isn't working. [E] Performance Track performance improvement (Time / Memory / CPU)
#3611 opened Oct 17, 2024 by zhassan-aws
Loop contracts in closures and coroutines [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3599 opened Oct 14, 2024 by qinheping
@qinheping
ICE: unable to find field 0 for type StructTag (never_type) [C] Bug This is a bug. Something isn't working.
#3596 opened Oct 13, 2024 by matthiaskrgr
Create macro to generate harnesses for contract [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3590 opened Oct 10, 2024 by celinval Function Contracts
5
ProTip! no:milestone will show everything without a milestone.