model-checking/kani issues and pull requests

#1638 - Tracking issue: release docs for Kani proptest

Issue - State: closed - Opened by YoshikiTakashima about 2 years ago

#1637 - Tracking issue: Proptest CI using Kani

Issue - State: closed - Opened by YoshikiTakashima about 2 years ago

#1635 - CBMC keeps unwinding recursion despite unwind bound

Issue - State: closed - Opened by fzaiser about 2 years ago - 4 comments
Labels: [C] Bug

#1612 - Create `--list-harnesses`API

Issue - State: open - Opened by jaisnan about 2 years ago
Labels: Z-IDE Extension

#1609 - Concrete playback requires nightly rustc

Issue - State: open - Opened by celinval about 2 years ago - 7 comments
Labels: [C] Bug

#1608 - Tracking issue for PropTest delivery

Issue - State: closed - Opened by danielsn about 2 years ago

#1603 - Launch Kani on Marketplace

Issue - State: closed - Opened by jaisnan about 2 years ago
Labels: Z-IDE Extension

#1594 - Assertion failure in `struct_expr_from_values`

Issue - State: open - Opened by tedinski about 2 years ago
Labels: [C] Bug, [F] Crash

#1577 - Concrete playback needs tweak for harnesses under `cfg(test)`

Issue - State: open - Opened by zhassan-aws about 2 years ago - 3 comments
Labels: [C] Bug

#1575 - Clean GotoC AST annotations

Issue - State: closed - Opened by giltho about 2 years ago - 4 comments

#1574 - Semantics of ZST dangling pointers: Kani differs from Miri

Issue - State: open - Opened by fzaiser about 2 years ago - 15 comments
Labels: [C] Feature / Enhancement

#1569 - Make "Run Kani" a hovering command over harnesses to allow user to directly call Kani after writing a harness

Issue - State: closed - Opened by jaisnan about 2 years ago
Labels: [C] Feature / Enhancement, Z-IDE Extension

#1564 - Check over-contraining assumptions

Issue - State: open - Opened by tedinski about 2 years ago
Labels: [C] Feature / Enhancement

#1550 - Add tests for function contracts.

Issue - State: closed - Opened by monal over 2 years ago

#1549 - Support quantifiers in function contract clauses.

Issue - State: closed - Opened by monal over 2 years ago - 1 comment

#1547 - Support logical implication in function contract clauses.

Issue - State: closed - Opened by monal over 2 years ago - 2 comments

#1546 - Support references in "modifies" (or "assigns") clause of function contracts.

Issue - State: closed - Opened by monal over 2 years ago
Labels: [C] Feature / Enhancement

#1545 - Interrupted first-time setup procedure cannot resume

Issue - State: closed - Opened by waynexia over 2 years ago - 5 comments
Labels: [C] Bug, [F] Crash, T-User

#1536 - Tracking issue for UX improvements to the concrete playback feature

Issue - State: open - Opened by sanjit-bhat over 2 years ago - 2 comments
Labels: [C] Feature / Enhancement

#1527 - Investigate whether we can use interpreted values rather than byte array values for playback

Issue - State: open - Opened by sanjit-bhat over 2 years ago - 4 comments
Labels: [C] Feature / Enhancement

#1524 - Investigate whether concrete playback works for `lazy_static!`

Issue - State: open - Opened by sanjit-bhat over 2 years ago
Labels: [C] Feature / Enhancement

#1518 - Rename `kani::unwind` (current name can be confused with stack unwinding on panics)

Issue - State: open - Opened by fzaiser over 2 years ago - 1 comment
Labels: [C] Feature / Enhancement

#1517 - Warn if async harness does not have an unwind bound

Issue - State: open - Opened by fzaiser over 2 years ago
Labels: [C] Feature / Enhancement

#1509 - Feature Request - VSCode Extension

Issue - State: closed - Opened by jaisnan over 2 years ago
Labels: [C] Feature / Enhancement

#1503 - Add macro expansion for function contracts.

Issue - State: closed - Opened by monal over 2 years ago

#1501 - Add hooks for pre and post conditions in function contracts.

Issue - State: closed - Opened by monal over 2 years ago - 1 comment

#1496 - Support `__CPROVER_r_ok`

Issue - State: closed - Opened by danielsn over 2 years ago - 5 comments
Labels: [C] Feature / Enhancement

#1495 - Soundness documentation

Issue - State: open - Opened by danielsn over 2 years ago
Labels: [C] Feature / Enhancement, [C] Documentation

#1481 - Tracking Issue: Concrete playback

Issue - State: open - Opened by celinval over 2 years ago - 1 comment
Labels: T-TrackingIssue

#1465 - Does `TagEncoding::Direct` need to worry about generators

Issue - State: closed - Opened by danielsn over 2 years ago

#1449 - Consider moving our copyright etc checks to use repolinter

Issue - State: closed - Opened by danielsn over 2 years ago

#1432 - Messages based on results should be printed as regular messages

Issue - State: closed - Opened by adpaco-aws over 2 years ago - 1 comment
Labels: [I] Refactoring / Clean Up, [C] Internal

#1394 - Improvements needed for the 'kani' library

Issue - State: open - Opened by tedinski over 2 years ago - 3 comments
Labels: [C] Feature / Enhancement

#1393 - Tracking issue for async/await in Kani (feature `async-lib`)

Issue - State: open - Opened by fzaiser over 2 years ago
Labels: [C] Feature / Enhancement, T-TrackingIssue

#1376 - Create a benchmark workflow

Issue - State: open - Opened by celinval over 2 years ago - 3 comments
Labels: [E] Performance, [C] Internal

#1375 - Our `std` library cannot properly handle different editions

Issue - State: open - Opened by celinval over 2 years ago - 2 comments
Labels: [C] Bug

#1367 - Buid Kani on arm linux

Issue - State: closed - Opened by tedinski over 2 years ago - 12 comments
Labels: [C] Feature / Enhancement, T-User

#1365 - Audit function signature codegen

Issue - State: closed - Opened by fzaiser over 2 years ago - 5 comments
Labels: [C] Bug

#1350 - Type in symbol table sometimes differs from what `codegen_function_sig` returns

Issue - State: closed - Opened by fzaiser over 2 years ago - 6 comments
Labels: [C] Bug

#1342 - Sinf/Cosf not being correctly evaluated

Issue - State: open - Opened by ssoudan over 2 years ago - 5 comments
Labels: [C] Bug, T-User, T-CBMC

#1341 - Kani failed to detect unaligned access to N-ZST pointers

Issue - State: closed - Opened by giltho over 2 years ago - 2 comments
Labels: [C] Feature / Enhancement, [E] Unsupported UB

#1325 - Consider using CBMC's json input interface instead of commandline

Issue - State: open - Opened by danielsn over 2 years ago
Labels: T-CBMC

#1314 - Stubbing plan document

Issue - State: closed - Opened by danielsn over 2 years ago - 1 comment

#1313 - Plan for unbounded verification

Issue - State: closed - Opened by danielsn over 2 years ago

#1304 - How to verify mmio access?

Issue - State: open - Opened by zpzigi754 over 2 years ago - 5 comments
Labels: [C] Feature / Enhancement, T-User

#1286 - MPSC Channel test case times out.

Issue - State: closed - Opened by YoshikiTakashima over 2 years ago - 3 comments
Labels: [E] Performance

#1276 - Investigate unrolling regression: Arc<AtomicBool>::compare_and_swap

Issue - State: closed - Opened by tedinski over 2 years ago - 1 comment

#1258 - To use dev-dependencies, you need to guard with `cfg(all(kani, test))`

Issue - State: closed - Opened by tedinski over 2 years ago - 6 comments
Labels: [C] Feature / Enhancement, [E] User Experience

#1255 - Kani should print out the version when its run

Issue - State: closed - Opened by danielsn over 2 years ago - 1 comment

#1233 - `offset` intrinsic doesn't check that pointers stay within bounds

Issue - State: open - Opened by adpaco-aws over 2 years ago - 2 comments
Labels: [C] Bug, [F] Spurious Failure

#1222 - CBMC API doc

Issue - State: open - Opened by danielsn over 2 years ago - 1 comment
Labels: T-CBMC

#1194 - Cleanup Kani's output

Issue - State: open - Opened by celinval over 2 years ago - 7 comments
Labels: [C] Feature / Enhancement, [E] User Experience

#1174 - clang-format is doing weird things to library/kani/stubs/C/vec/vec.c

Issue - State: closed - Opened by danielsn over 2 years ago

#1168 - Investigate what to do with `align` when doing alloc

Issue - State: open - Opened by danielsn over 2 years ago - 4 comments
Labels: [C] Internal

#1163 - Restore and audit remaining intrinsics

Issue - State: open - Opened by adpaco-aws over 2 years ago
Labels: [C] Internal

#1092 - Revisit how we codegen dereferencing fat pointers

Issue - State: closed - Opened by celinval over 2 years ago - 1 comment
Labels: [C] Internal

#1067 - Reminder issue: code signing on macos-arm

Issue - State: closed - Opened by tedinski over 2 years ago

#989 - Integrate a subset of the rustc tests

Issue - State: open - Opened by zhassan-aws over 2 years ago
Labels: [C] Internal

#957 - Kani should make use of CBMC's internal consistency checks.

Issue - State: open - Opened by tautschnig over 2 years ago - 13 comments
Labels: [C] Internal, T-MLP Should Have

#942 - Design Machine Readable Output - RFC

Issue - State: open - Opened by jaisnan over 2 years ago
Labels: T-RFC

#937 - Clear documentation of Kani TCB

Issue - State: open - Opened by danielsn over 2 years ago
Labels: [C] Feature / Enhancement

#897 - Kani trace includes wrong variable initializaton

Issue - State: closed - Opened by celinval over 2 years ago - 2 comments
Labels: [C] Bug, T-MLP Should Have

#896 - Add better support for `MaybeUninit`

Issue - State: open - Opened by celinval over 2 years ago
Labels: [C] Feature / Enhancement, T-MLP Need Triage

#836 - Support for quantifiers in asserts and assumes

Issue - State: open - Opened by nchong-at-aws over 2 years ago
Labels: [C] Feature / Enhancement

#810 - Unimplemented intrinsic: `frem_fast`

Issue - State: open - Opened by adpaco-aws almost 3 years ago - 1 comment
Labels: [C] Feature / Enhancement, [E] Unsupported Construct

#809 - Some fast math results cannot be practically compared

Issue - State: open - Opened by adpaco-aws almost 3 years ago
Labels: [E] Performance, T-CBMC

#723 - `HashMap::new` fails to verify: `syscall` undefined

Issue - State: open - Opened by zhassan-aws almost 3 years ago - 8 comments
Labels: [C] Bug, T-MLP Should Have

#701 - cargo-rmc tracking issue

Issue - State: closed - Opened by tedinski almost 3 years ago - 1 comment
Labels: [C] Internal

#697 - Abstraction options not working

Issue - State: closed - Opened by zhassan-aws almost 3 years ago - 1 comment
Labels: [C] Bug

#640 - Boogie backend

Issue - State: closed - Opened by HKalbasi about 3 years ago - 4 comments
Labels: [C] Feature / Enhancement

#598 - Organize the output from Kani to make it more user friendly

Issue - State: open - Opened by zhassan-aws about 3 years ago - 2 comments
Labels: [C] Feature / Enhancement

#560 - Structure mismatch in "Generics - Phantom type parameters" example

Issue - State: closed - Opened by adpaco-aws about 3 years ago - 2 comments
Labels: [C] Bug, [F] Crash, T-MLP Should Have

#555 - Fix regression tests that require "rmc-flags: --no-undefined-function-checks"

Issue - State: open - Opened by danielsn about 3 years ago
Labels: [C] Bug

#450 - Rethink naming for external C libraries

Issue - State: open - Opened by avanhatt about 3 years ago
Labels: [C] Bug

#444 - Fix code generation for SIMD types

Issue - State: closed - Opened by vecchiot-aws about 3 years ago - 3 comments

#440 - Find if there is a better stub for POINTER_OBJECT

Issue - State: open - Opened by vecchiot-aws about 3 years ago
Labels: [C] Internal, T-CBMC

#410 - Add a new option to run visualize without coverage

Issue - State: closed - Opened by zhassan-aws over 3 years ago - 3 comments
Labels: [C] Feature / Enhancement

#368 - Running `--visualize` still includes unnecessary CBMC checks in coverage run

Issue - State: closed - Opened by vecchiot-aws over 3 years ago - 3 comments
Labels: [E] Performance, [C] Feature / Enhancement

#364 - Re-add method name to vtable field name

Issue - State: closed - Opened by avanhatt over 3 years ago
Labels: [C] Internal

#343 - Test `src/test/cbmc/Serde/main_fail.rs` doesn't compile.

Issue - State: closed - Opened by vecchiot-aws over 3 years ago - 2 comments

#340 - Test `src/test/cbmc/Slice/drop_in_place_fail.rs` doesn't compile.

Issue - State: closed - Opened by vecchiot-aws over 3 years ago - 1 comment

#313 - Add support to concurrency

Issue - State: closed - Opened by danielsn over 3 years ago
Labels: [C] Feature / Enhancement, [E] Unsupported Construct

#311 - Add support verification of unbounded structures and loops

Issue - State: closed - Opened by danielsn over 3 years ago - 3 comments
Labels: [C] Feature / Enhancement, [E] User Experience

#303 - Linking may not follow Rust rules

Issue - State: open - Opened by danielsn over 3 years ago - 2 comments
Labels: T-CBMC

#302 - Correctness of CBMC Serialization

Issue - State: open - Opened by danielsn over 3 years ago
Labels: T-CBMC

#301 - Missing check for object correctness invariants

Issue - State: closed - Opened by danielsn over 3 years ago - 1 comment
Labels: [E] Unsupported UB

#299 - Audit Vtable generation for dynamic traits

Issue - State: open - Opened by danielsn over 3 years ago - 5 comments
Labels: [C] Internal

#298 - Feature request: detect when Rustc hides UB (undefined behavior) when generating MIR

Issue - State: open - Opened by danielsn over 3 years ago - 1 comment
Labels: [C] Feature / Enhancement

#297 - Feature request: check for possible UB due to non-determinstic layouts

Issue - State: open - Opened by danielsn over 3 years ago - 1 comment
Labels: [C] Feature / Enhancement

#296 - Feature request: detect when object layouts may not faithfully follow Rustc layouts

Issue - State: closed - Opened by danielsn over 3 years ago - 2 comments
Labels: [C] Feature / Enhancement

#267 - Unimplemented: `catch_unwind` intrinsic

Issue - State: open - Opened by danielsn over 3 years ago - 3 comments
Labels: [C] Feature / Enhancement, [E] Unsupported Construct

#185 - Figure out missing source location for vtable initializers.

Issue - State: closed - Opened by vecchiot-aws over 3 years ago - 3 comments
Labels: [C] Bug, [E] User Experience

#136 - Places with missing Location.

Issue - State: closed - Opened by vecchiot-aws over 3 years ago
Labels: [C] Feature / Enhancement, [E] User Experience

#131 - Viewer support for RMC output

Issue - State: closed - Opened by markrtuttle over 3 years ago - 3 comments

#127 - Add accurate source locations as needed in RMC

Issue - State: closed - Opened by adpaco-aws over 3 years ago - 1 comment
Labels: [C] Feature / Enhancement, [E] User Experience

#90 - Spurious failure when calling `vec!` with a size of zero

Issue - State: open - Opened by adpaco-aws over 3 years ago - 3 comments
Labels: [C] Bug, [F] Spurious Failure

#87 - Bad pointer deref in `SizeAndAlignOfDst/main_fail.rs`

Issue - State: closed - Opened by markrtuttle over 3 years ago - 5 comments
Labels: [C] Bug

#77 - Support for negative test: Pointers out of scope

Issue - State: closed - Opened by adpaco-aws over 3 years ago
Labels: [C] Bug

#72 - Support for variadic `extern` function calls

Issue - State: open - Opened by adpaco-aws over 3 years ago - 2 comments
Labels: [C] Bug

#63 - Maintain a map from functions to integers to generate fresh variables

Issue - State: open - Opened by adpaco-aws over 3 years ago
Labels: [I] Refactoring / Clean Up, [C] Internal

GitHub / model-checking/kani issues and pull requests