model-checking/kani issues and pull requests

#2299 - Option that causes verification to fail for uncoverable cover statements

Issue - State: open - Opened by adpaco-aws over 1 year ago - 1 comment
Labels: [C] Feature / Enhancement, [E] User Experience, T-User

#2296 - Add flag to generate GOTO program

Issue - State: open - Opened by feliperodri over 1 year ago - 2 comments
Labels: [C] Feature / Enhancement

#2293 - Upgrade toolchain to nightly-2023-03-09

Pull Request - State: closed - Opened by qinheping over 1 year ago - 1 comment

#2284 - Kani doesn't handle system calls

Issue - State: open - Opened by adpaco-aws over 1 year ago - 5 comments
Labels: [F] Spurious Failure, T-User, [E] Unsupported Construct, T-CBMC

#2277 - Add a CI pass for pull requests that detects perfomance regressions compared to HEAD

Issue - State: closed - Opened by karkhaz over 1 year ago

#2275 - Develop a more reliable mechanism for overriding `std` macros

Issue - State: open - Opened by zhassan-aws over 1 year ago
Labels: [C] Internal, Z-Kani Compiler

#2266 - ICE: `internal error: entered unreachable code: Should have generated a fat pointer`

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2265 - va_arg is currently not supported by kani

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug

#2264 - Projection mismatch when declaring array-based SIMD

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 3 comments
Labels: [C] Bug, [E] Unsupported Construct, Z-Kani Compiler

#2262 - ICE unreachable!(): operand.rs

Issue - State: closed - Opened by matthiaskrgr over 1 year ago - 2 comments
Labels: [C] Bug

#2261 - ICE: control character found while parsing a string

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 4 comments
Labels: [C] Bug, [F] Crash

#2260 - ICE: Function call does not type check: #![feature(unboxed_closures/tuple_trait)]

Issue - State: closed - Opened by matthiaskrgr over 1 year ago - 3 comments
Labels: [C] Bug, [F] Crash

#2259 - ICE: prev_args.len() == 1

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2258 - ICE: `assertion failed: value <= (0xFFFF_FF00 as usize`

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2256 - ICE: Can't apply .member operation to ...

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2255 - ICE: `Function should've been declared before usage`, was: `Can't take address of Expr`

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2254 - ICE: Error in struct_expr; mismatch in number of fields and values

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2253 - ICE: place: Unexpected type mismatch in projection:

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 2 comments
Labels: [C] Bug, [F] Crash

#2252 - ICE: 'assertion failed: typ.is_numeric()', cprover_bindings/src/goto_program/typ.rs:1201:9

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2245 - Build M1-bundle in release script

Issue - State: open - Opened by karkhaz over 1 year ago
Labels: [I] CI / Infrastructure

#2244 - add kani sanity checks to release script

Issue - State: open - Opened by karkhaz over 1 year ago
Labels: [C] Internal

#2243 - Create script to update CBMC-version upon manual trigger

Issue - State: closed - Opened by karkhaz over 1 year ago - 2 comments
Labels: [I] CI / Infrastructure

#2242 - ICE: unequal types: subslice, but only mir-opt-level <2

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 3 comments
Labels: [C] Bug, [F] Crash, Z-Kani Compiler

#2241 - ICE: unequal types TypeDef / StructTag

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash, Z-Kani Compiler

#2240 - ICE: `Generating a slice fat pointer to Tuple([i32, [Foo]])`, `feature(unsized_tuple_coercion)`

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2239 - ICE: `feature(trivial_bounds)`

Issue - State: closed - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2238 - ICE: `Tried to insert symbol which already existed`

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 1 comment
Labels: [C] Bug, [F] Crash

#2237 - ICE: "assign statement with unequal types" ; StructTag / StructTag

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 10 comments
Labels: [C] Bug, [F] Crash

#2236 - ICE: failed to get layout for, too big for arch

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 2 comments
Labels: [C] Bug, [F] Crash, T-User

#2235 - hangs on string.repeat() ?

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 6 comments
Labels: [C] Bug, [E] Performance, T-User, T-CBMC

#2233 - RUSTC_WRAPPER handling could be improved

Issue - State: open - Opened by matthiaskrgr over 1 year ago - 3 comments
Labels: [C] Bug, T-User

#2226 - Loop-contracts synthesizer is not compatible with ```kani::cover```

Issue - State: open - Opened by qinheping over 1 year ago - 1 comment
Labels: [C] Bug

#2215 - RFC: Loop-contract synthesis

Pull Request - State: open - Opened by qinheping almost 2 years ago - 3 comments
Labels: T-RFC

#2209 - Make AnySlice::new() loop free

Issue - State: closed - Opened by feliperodri almost 2 years ago - 1 comment
Labels: [E] Performance

#2203 - Autocomplete feature for CLI options

Issue - State: open - Opened by adpaco-aws almost 2 years ago - 2 comments
Labels: [C] Feature / Enhancement

#2197 - Review documentation regarding platform support

Issue - State: open - Opened by danielsn almost 2 years ago - 1 comment
Labels: [C] Documentation

#2187 - Issue finding `debug_assert` in `no_std` crates when std enabled

Issue - State: closed - Opened by cameron1024 almost 2 years ago - 4 comments
Labels: [C] Bug, T-High Priority, T-User, Z-Kani Compiler

#2178 - Spurious failure on Prost check_duration_roundtrip

Issue - State: open - Opened by danielsn almost 2 years ago
Labels: [C] Bug, [F] Spurious Failure, T-User, Z-Kani Compiler

#2176 - Tracking issue for: Fix issue Kani detected on Prost

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

#2175 - Reevaluate Kani on Prost

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

#2163 - Concrete playback should support all kind of property failures

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

#2157 - Complete 3/5 shard proofs

Issue - State: closed - Opened by remi-delmas-3000 almost 2 years ago
Labels: [C] Internal

#2155 - Migrate loop contracts to dynamic frames in CBMC

Issue - State: closed - Opened by remi-delmas-3000 almost 2 years ago - 2 comments
Labels: [C] Internal

#2153 - C-FFI: support build of C files using build.rs

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

#2152 - C-FFI: Support conversion of `Option<&T>` to `T*` in the CBMC linker

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

#2151 - C-FFI: Support for void vs unit return type in CBMC linker

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

#2150 - C-FFI: Set of test-cases for FFI linking

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

#2141 - Add documentation for performance comparison tool

Pull Request - State: closed - Opened by karkhaz almost 2 years ago - 3 comments
Labels: T-RFC

#2131 - Add support to `simd_bitmask` intrinsic

Issue - State: closed - Opened by celinval almost 2 years ago - 10 comments
Labels: [C] Feature / Enhancement, [E] Unsupported Construct, Z-Kani Compiler

#2129 - Remove `--function` option

Issue - State: closed - Opened by celinval almost 2 years ago - 5 comments
Labels: [I] Refactoring / Clean Up, [C] Internal, Z-Kani Compiler

#2121 - Kani crashes when an intrinsic call using ZST is invalid

Issue - State: closed - Opened by celinval almost 2 years ago - 7 comments
Labels: [C] Bug, [F] Crash

#2119 - Print all the stubs that were exercised in a harness

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

#2107 - Tracking issue: common unsupported features

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

#2096 - Implement stub-sets

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

#2086 - How to verify a target different to the host environment?

Issue - State: closed - Opened by zpzigi754 almost 2 years ago - 9 comments
Labels: [C] Feature / Enhancement

#2069 - Create run comparison & dashboard generator

Issue - State: closed - Opened by karkhaz almost 2 years ago - 1 comment

#2068 - Enable verification of code that uses C-FFI

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

#2066 - Spurious "memcpy source region readable" error

Issue - State: closed - Opened by zhassan-aws almost 2 years ago - 2 comments
Labels: [C] Bug, [F] Spurious Failure

#2048 - Visualize incorrectly reports all lines covered

Issue - State: closed - Opened by zhassan-aws almost 2 years ago - 2 comments
Labels: [C] Bug

#2035 - Stabilize `Arbitrary` trait?

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

#2022 - Slow verification with multiple insertions in a `BTreeSet`

Issue - State: closed - Opened by zhassan-aws almost 2 years ago - 4 comments
Labels: [E] Performance, [C] Feature / Enhancement

#2015 - Poor performance scaling for a simple program involving String push/pop

Issue - State: open - Opened by zhassan-aws almost 2 years ago - 1 comment
Labels: [E] Performance, [C] Feature / Enhancement, T-CBMC

#2007 - Address validation of stubs with mismatched lifetimes

Issue - State: open - Opened by aaronbembenek-aws almost 2 years ago
Labels: [C] Feature / Enhancement, [E] User Experience

#1997 - Resolve trait methods during stubbing

Issue - State: open - Opened by aaronbembenek-aws almost 2 years ago - 10 comments
Labels: [C] Feature / Enhancement, [E] User Experience, T-User

#1982 - Different enum layouts result in 10x difference in verification time

Issue - State: closed - Opened by aaronbembenek-aws almost 2 years ago - 4 comments
Labels: [E] Performance, [C] Feature / Enhancement

#1971 - Improve codegen performance

Issue - State: open - Opened by celinval almost 2 years ago
Labels: [E] Performance, [C] Feature / Enhancement

#1970 - `simd_div` and `simd_rem` don't check for overflow cases

Issue - State: closed - Opened by adpaco-aws almost 2 years ago - 2 comments
Labels: [E] Unsupported UB

#1963 - `simd_shl` and `simd_shr` don't check overflow cases

Issue - State: closed - Opened by adpaco-aws almost 2 years ago
Labels: [E] Unsupported UB

#1960 - `simd_shuffle*` doesn't check that `indexes` contains constant values which are within expected bounds

Issue - State: open - Opened by adpaco-aws almost 2 years ago - 1 comment
Labels: [C] Feature / Enhancement

#1954 - Windows support

Issue - State: open - Opened by Timmmm almost 2 years ago - 3 comments
Labels: [C] Feature / Enhancement, T-User

#1953 - Allow generic parameter names to differ while validating function/method stubs

Issue - State: open - Opened by aaronbembenek-aws almost 2 years ago
Labels: [C] Feature / Enhancement, [E] User Experience

#1926 - Invalid projection on firecracker regression with the 2022-11-20 rust toolchain

Issue - State: closed - Opened by zhassan-aws almost 2 years ago - 15 comments
Labels: [C] Feature / Enhancement, T-User, [E] Unsupported Construct, Z-Kani Compiler

#1866 - Resolve names during stubbing

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

#1861 - Split tests for function/method stubbing into multiple harnesses

Issue - State: open - Opened by aaronbembenek-aws about 2 years ago
Labels: [I] Refactoring / Clean Up, [C] Internal

#1855 - Per-harness code generation

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

#1842 - Integrate function/method stubbing and concrete playback

Issue - State: closed - Opened by aaronbembenek-aws about 2 years ago - 1 comment
Labels: [C] Feature / Enhancement, [E] User Experience

#1841 - Remove `--harness` argument from `kani-compiler`

Issue - State: open - Opened by aaronbembenek-aws about 2 years ago - 3 comments
Labels: T-High Priority, [I] Refactoring / Clean Up, [C] Internal

#1835 - Kani fails to compile tokio: unable to find field 0 for type StructTag(...)

Issue - State: open - Opened by fzaiser about 2 years ago - 3 comments
Labels: [C] Bug, [F] Crash, Z-Kani Compiler

#1831 - `kani-driver` argument parsing needs restructuring

Issue - State: open - Opened by tedinski about 2 years ago - 1 comment
Labels: [C] Internal

#1819 - New unsupported features table for assess

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

#1809 - Tracking issue for function and method stubbing

Issue - State: open - Opened by aaronbembenek-aws about 2 years ago
Labels: T-RFC, Z-Kani Compiler

#1808 - Specify finer-grained unwinding values

Issue - State: open - Opened by zpzigi754 about 2 years ago - 1 comment
Labels: [C] Feature / Enhancement, T-User

#1781 - function call: parameter "pthread_key_create::destructor" type mismatch when hitting `thread::current()`

Issue - State: closed - Opened by roypat about 2 years ago - 6 comments
Labels: [C] Bug, [F] Crash, T-User

#1777 - Generate LCOV coverage

Issue - State: open - Opened by JonathanWoollett-Light about 2 years ago
Labels: [C] Feature / Enhancement, T-User

#1743 - Unexpected failure: "Function `mmap` with missing definition is unreachable"

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

#1712 - Writing harnesses under e.g. rust-analyzer gives a poor experience

Issue - State: open - Opened by tedinski about 2 years ago - 3 comments
Labels: [C] Bug, [E] User Experience

#1710 - Allow disabling unwinding assertions for specific harnesses

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

#1707 - first-steps-v2 coverage shows many uncovered lines

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

#1706 - Generate GCOV coverage output from `cargo kani`

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

#1693 - Verification time increased by 7X on an s2n-quic harness

Issue - State: closed - Opened by zhassan-aws about 2 years ago - 6 comments
Labels: [C] Bug, T-High Priority, [E] Performance, T-User

#1690 - RFC: New default output for Kani

Issue - State: open - Opened by tedinski about 2 years ago - 4 comments
Labels: T-RFC

#1685 - Replace manual spawning code in test case by kani::spawn library once it's merged

Issue - State: open - Opened by fzaiser about 2 years ago - 2 comments
Labels: [I] Refactoring / Clean Up

#1679 - Tracking: #1669 turns off test case b/c `expect_fail` is not working.

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

#1663 - Adding async verification examples to the Kani test suite

Issue - State: open - Opened by fzaiser about 2 years ago
Labels: [C] Internal, [I] CI / Infrastructure

#1662 - Kani unexpectedly panicked during compilation.

Issue - State: closed - Opened by nano-o about 2 years ago - 3 comments
Labels: T-High Priority, T-User

#1661 - Allow specifying the scheduling strategy in #[kani_proof] for async functions

Pull Request - State: closed - Opened by fzaiser about 2 years ago - 4 comments

#1659 - Add kani::spawn and an executor to the Kani library

Pull Request - State: open - Opened by fzaiser about 2 years ago - 31 comments
Labels: Z-Async Blocker

#1647 - Use Clap Derive API instead of Builder API in `kani-compiler`

Issue - State: closed - Opened by celinval about 2 years ago - 4 comments
Labels: [I] Refactoring / Clean Up

#1640 - Tracking issue: Proptest dependencies removed to avoid Kani ICE

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

#1639 - Tracking issue: when KaniLib is released, use that.

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

GitHub / model-checking/kani issues and pull requests