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

419 Open 797 Closed
419 Open 797 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

Memory blows up on a small program involving String split [C] Bug This is a bug. Something isn't working. [E] Performance Track performance improvement (Time / Memory / CPU)
#2302 opened Mar 17, 2023 by zhassan-aws
How to assume the pointer's validity passed from an external interface? [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#2300 opened Mar 17, 2023 by zpzigi754
1
Option that causes verification to fail for uncoverable cover statements [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
#2299 opened Mar 13, 2023 by adpaco-aws
@adpaco-aws
Delay declaring variables [C] Internal Tracks some internal work. I.e.: Users should not be affected. Z-Kani Compiler Issues that require some changes to the compiler
#2298 opened Mar 10, 2023 by celinval
Add flag to generate GOTO program [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#2296 opened Mar 10, 2023 by feliperodri
assess scan execution could be parallelized [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#2294 opened Mar 10, 2023 by adpaco-aws
1
Check CaDiCaL version on regression script [C] Bug This is a bug. Something isn't working.
#2289 opened Mar 9, 2023 by feliperodri
@zhassan-aws
1
Kani doesn't have an --exact flag to call for singular harnesses [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#2285 opened Mar 8, 2023 by jaisnan
Kani doesn't handle system calls [E] Unsupported Construct Add support to an unsupported construct [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. T-CBMC Issue related to an existing CBMC issue T-User Tag user issues / requests
#2284 opened Mar 8, 2023 by adpaco-aws
4
Update rust toolchain version for Kani 0.24 Z-Sync Upstream Fetch changes from rustc repository. Old Rebase
#2283 opened Mar 8, 2023 by celinval
1
@tautschnig @qinheping
3
Create mechanism to enable / disable APIs [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-RFC Label RFC PRs and Issues
#2279 opened Mar 7, 2023 by celinval Maintenance
@celinval
Add a CI pass for pull requests that detects perfomance regressions compared to HEAD
#2277 opened Mar 7, 2023 by karkhaz
@karkhaz
Develop a more reliable mechanism for overriding std macros [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2275 opened Mar 7, 2023 by zhassan-aws
ICE: Type dyn* std::future::Future<Output = usize> must be a trait type (a dynamic type) [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2266 opened Mar 3, 2023 by matthiaskrgr
va_arg is currently not supported by kani [C] Bug This is a bug. Something isn't working.
#2265 opened Mar 3, 2023 by matthiaskrgr
projection mismatch [C] Bug This is a bug. Something isn't working. [E] Unsupported Construct Add support to an unsupported construct Z-Kani Compiler Issues that require some changes to the compiler
#2264 opened Mar 3, 2023 by matthiaskrgr
1
ICE unreachable!(): operand.rs [C] Bug This is a bug. Something isn't working.
#2262 opened Mar 2, 2023 by matthiaskrgr
ICE: control character found while parsing a string [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2261 opened Mar 2, 2023 by matthiaskrgr
@adpaco-aws
3
ICE: Function call does not type check: #![feature(unboxed_closures/tuple_trait)] [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2260 opened Mar 2, 2023 by matthiaskrgr
ICE: prev_args.len() == 1 [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2259 opened Mar 2, 2023 by matthiaskrgr
ICE: index out of bounds: extern_types [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2258 opened Mar 2, 2023 by matthiaskrgr
ICE: Can't apply .member operation to ... [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2256 opened Mar 2, 2023 by matthiaskrgr
ICE: Can't take address of Expr [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2255 opened Mar 2, 2023 by matthiaskrgr
ICE: Error in struct_expr; mismatch in number of fields and values [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2254 opened Mar 2, 2023 by matthiaskrgr
ICE: place: Unexpected type mismatch in projection: [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2253 opened Mar 2, 2023 by matthiaskrgr
1
ProTip! Mix and match filters to narrow down what you’re looking for.