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

Clear current search query, filters, and sorts
0 Open 1,141 Closed
0 Open 1,141 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-15 failed
#3530 by github-actions bot was closed Sep 22, 2024
1
RMC needs a __VERIFIER_assume predicate
#114 by danielsn was closed May 14, 2021
1
@danielsn
Cleanup hooks.rs
#117 by danielsn was closed May 21, 2021
1
Extern crate usage causes Box predicate to fail [F] Crash Kani crashed
#113 by adpaco-aws was closed May 25, 2021
1
@danielsn
The abort instrinsic doesn't have a target, so target.unwrap() crashes [C] Bug This is a bug. Something isn't working.
#150 by danielsn was closed May 26, 2021
1
Feature request: Reliable way to determine whether a type represents a box
#152 by danielsn was closed Sep 22, 2021
1
@danielsn
Using f64::powi causes type error. [C] Bug This is a bug. Something isn't working.
#135 by vecchiot-aws was closed May 27, 2021
1
@vecchiot-aws
Places with missing Location. [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.
#136 by vecchiot-aws was closed Jun 12, 2024
89 tasks
1
RMC can't handle u128 constants [C] Bug This is a bug. Something isn't working.
#140 by danielsn was closed May 21, 2021
1
Update CBMC version check to 5.30 in rmc-regression.sh [C] Bug This is a bug. Something isn't working.
#164 by avanhatt was closed Jun 2, 2021
2
Move all tests under rust-tests to compiletest
#165 by bdalrhm was closed Jun 7, 2021
1
@bdalrhm
Port Cargo Tests into compiletest.
#177 by bdalrhm was closed Jun 16, 2021
1
@bdalrhm
Get basic understanding of Rust DWARF emission
#182 by vecchiot-aws was closed Mar 17, 2022
@vecchiot-aws
Unit/regression tests for vtable size and align fields
#176 by avanhatt was closed Jun 15, 2021
1
@avanhatt
Soundness doc v2
#179 by danielsn was closed Jan 24, 2023
@danielsn
Add an rmc_sanity_check function for that flavor of assert
#200 by avanhatt was closed Jun 17, 2021
1
@avanhatt
Standard library function panic::Location::<'a>::caller does not codegen
#205 by danielsn was closed Nov 4, 2021
1
Visualize option requires cbmc-viewer in CI [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#161 by adpaco-aws was closed May 31, 2021
1
@adpaco-aws
GotoCtx and CurrentFnCtx are confusingly intermingled
#196 by danielsn was closed Jun 11, 2021
1
Verify that the standard library regression is running in CI [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#375 by adpaco-aws was closed Nov 4, 2021
1
@celinval
Use Litani to run the reference examples and display the results.
#384 by bdalrhm was closed Aug 9, 2021
1
@bdalrhm
Extract examples from The Nomicon and Unsafe Rust and display them in the dashboard.
#385 by bdalrhm was closed Aug 12, 2021
1
@bdalrhm
Support --gen-symbols in cargo-rmc. T-Good First Issue Good for newcomers
#359 by vecchiot-aws was closed Jul 29, 2021
1
@vecchiot-aws
Peformance measurements for dynamic dispatch [E] Performance Track performance improvement (Time / Memory / CPU)
#383 by avanhatt was closed Nov 23, 2021
@avanhatt
Add questions to semantics office hours
#186 by danielsn was closed Jun 22, 2021
@danielsn
ProTip! Add no:assignee to see everything that’s not assigned.