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

515 Open 1,076 Closed
515 Open 1,076 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

The old construct does not respect the function requirements [C] Bug This is a bug. Something isn't working.
#3359 opened Jul 19, 2024 by celinval Function Contracts
Toolchain upgrade to nightly-2024-07-19 failed
#3358 opened Jul 19, 2024 by github-actions bot
Remove terse output requirement for parallel jobs [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#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.
#3349 opened Jul 16, 2024 by pi314mm Function Contracts
Checking memory initialization in presence of copy and copy_nonoverlapping produces false positives [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.
#3347 opened Jul 16, 2024 by artemagvanian
1
@artemagvanian
Add contract support to intrinsics [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3345 opened Jul 15, 2024 by celinval
Modifies property points to a temporary variable [C] Bug This is a bug. Something isn't working.
#3336 opened Jul 12, 2024 by celinval Function Contracts
Build bundle jobs could test bundles before upload [C] Internal Tracks some internal work. I.e.: Users should not be affected. [I] CI / Infrastructure Work done to CI, tests and infrastructure.
#3331 opened Jul 8, 2024 by adpaco-aws
1
Performance drastically differs across two string indexing operations [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Performance Track performance improvement (Time / Memory / CPU)
#3328 opened Jul 5, 2024 by zhassan-aws
1
Disable Divide by 0 Checks for Floats [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#3327 opened Jul 5, 2024 by cvick32
Add an option to turn requires clauses into assertions [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.
#3326 opened Jul 4, 2024 by celinval Function Contracts
Allow users to annotate functions without body with contracts [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.
#3325 opened Jul 4, 2024 by celinval Function Contracts
2
Uninitialized memory detection mitigates delayed UB, but does not support it fully [E] Unsupported UB Undefined behavior that Kani does not detect Z-UnstableFeature Issues that only occur if a unstable feature is enabled
#3324 opened Jul 4, 2024 by celinval
1
@artemagvanian
1
Kani panicked in codegen/rvalue [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-User Tag user issues / requests
#3318 opened Jul 2, 2024 by TomMD
4
Function Contracts: Mutual recursion function contract wrapper for replace code stub [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3316 opened Jul 2, 2024 by pi314mm Function Contracts
Kani internal panic when calling somehwat complex library path with no symbolic inputs [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-User Tag user issues / requests
#3312 opened Jul 1, 2024 by aaronjeline
4
Overwriting a composite object in an array causes a blowup in variables [E] Performance Track performance improvement (Time / Memory / CPU) T-CBMC Issue related to an existing CBMC issue
#3311 opened Jul 1, 2024 by jsalzbergedu
3
Add core intrisincs tests for f16 and f128 [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#3308 opened Jun 28, 2024 by jaisnan
@jaisnan
Tracking Issue: Automatically Verify Memory Initialization [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-TrackingIssue Issues used to track a large amount of work related to a feature
#3300 opened Jun 27, 2024 by artemagvanian
2 of 9 tasks
@artemagvanian
5
Mutable static variables usage in contract verification trigger UB [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.
#3298 opened Jun 27, 2024 by celinval Function Contracts
2
Contract implementation is unsafe and may trigger UB [C] Bug This is a bug. Something isn't working.
#3293 opened Jun 25, 2024 by celinval Function Contracts
CBMC upgrade to 6.0.1 failed
#3287 opened Jun 24, 2024 by github-actions bot
Add support to Z3 [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3277 opened Jun 19, 2024 by celinval
1
Function Contracts: Better error messages [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#3273 opened Jun 18, 2024 by pi314mm Function Contracts
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.