model-checking/kani issues and pull requests

#2516 - RFC: Global Conditions

Pull Request - State: closed - Opened by adpaco-aws over 1 year ago - 8 comments
Labels: T-RFC

#2502 - `None ` in typ.rs, binding to type dyn trait

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

#2501 - None in codegen_cprover_gotoc/codegen/statement.rs

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

#2499 - ICE `Function `{func}` should've been declared before usage`

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

#2498 - assertion failure: ref to enum static

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

#2497 - ICE: `Argument doesn't check` / `Function call does not type check`

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

#2493 - Finish refactoring on how we handle the metadata file for Tests and PubFns

Issue - State: closed - Opened by celinval over 1 year ago - 2 comments
Labels: [C] Internal, Z-Kani Compiler

#2467 - Playback subcommand should respect Cargo.toml configuration

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

#2458 - Automatic toolchain upgrade to nightly-2023-04-30

Pull Request - State: open - Opened by github-actions[bot] over 1 year ago

#2457 - Slow down and higher memory usage with 2023-04-30 rust toolchain

Issue - State: open - Opened by zhassan-aws over 1 year ago - 1 comment
Labels: [C] Bug, [E] Performance

#2456 - Upgrade rust toolchain to 2023-04-30

Pull Request - State: open - Opened by zhassan-aws over 1 year ago - 1 comment

#2455 - False verification failures since version 0.28.0

Issue - State: open - Opened by arctic-alpaca over 1 year ago - 4 comments
Labels: [C] Bug, T-High Priority, [F] Spurious Failure, T-User

#2454 - Fix regression on concrete playback inplace

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

#2453 - Concrete playback not working for `Result<T, E>` when `T` is `()`

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

#2452 - Update rust toolchain to 2023-04-29

Pull Request - State: closed - Opened by zhassan-aws over 1 year ago - 5 comments

#2451 - Update rust toolchain version to nightly-2023-04-30

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

#2450 - Concrete Playback=inplace produces unit test inside the harness

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

#2449 - Move common arguments to their own structure

Pull Request - State: closed - Opened by celinval over 1 year ago - 3 comments

#2448 - Automatic toolchain upgrade to nightly-2023-04-17

Pull Request - State: closed - Opened by github-actions[bot] over 1 year ago - 1 comment

#2447 - Fix symtab json file removal and reduce regression scope

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

#2446 - Fix link in CHANGELOG.md

Pull Request - State: closed - Opened by zhassan-aws over 1 year ago

#2445 - Synthesized GOTO program will be bypassed with option `--no-default-check'

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

#2444 - Bump Kani version to 0.28.0

Pull Request - State: closed - Opened by zhassan-aws over 1 year ago

#2443 - Bump Kani dependencies

Pull Request - State: closed - Opened by zhassan-aws over 1 year ago

#2442 - Measure compiler performance and overall execution time as part of our benchmarks

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

#2441 - Bump CBMC version to 5.83.0

Pull Request - State: closed - Opened by zhassan-aws over 1 year ago

#2440 - Create a command to play a counter example

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

#2439 - Perform reachability analysis on a per-harness basis

Pull Request - State: closed - Opened by celinval over 1 year ago - 7 comments

#2438 - Remove unnecessary dependency

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

#2437 - Cleanup redundant logic

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

#2436 - Fix the order of operands for generator structs

Pull Request - State: closed - Opened by zhassan-aws over 1 year ago

#2435 - Use InternedString in other parts of our code (such as Metadata)

Issue - State: open - Opened by celinval over 1 year ago
Labels: [I] Refactoring / Clean Up, [C] Internal

#2434 - Kani 0.27 unexpectedly panicked during compilation

Issue - State: closed - Opened by ytakano over 1 year ago - 2 comments
Labels: [C] Bug, T-User

#2433 - Add a few options to dump the reachability graph (debug only)

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

#2432 - Cannot checkout this repo on windows because of `:` character in path

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

#2431 - Remove unneeded unwinds from unbounded benchmarks

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

#2430 - `_tlv_atexit` definition is missing

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

#2429 - Use same perf tests for benchcomp in CI

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

#2428 - Limit FFI calls by default to explicitly supported ones

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

#2427 - Get rid of the legacy mode

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

#2426 - Kani should verify the existance of clashing C functions

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

#2425 - The unstable `--c-lib` option now requires `-Z c-ffi` to enable C-FFI support

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

#2424 - Adding a performance regression breaks perf-benchcomp CI workflow

Issue - State: closed - Opened by zhassan-aws over 1 year ago - 2 comments
Labels: [C] Bug, [C] Internal

#2423 - Add proper support to C-FFI calls

Issue - State: open - Opened by celinval over 1 year ago - 12 comments
Labels: [C] Feature / Enhancement, T-User

#2422 - Add a new perf test

Pull Request - State: closed - Opened by zhassan-aws over 1 year ago - 2 comments

#2421 - Update s2n-quic submodule

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

#2420 - Print compilation stats about the MIR that was codegened in verbose mode

Pull Request - State: closed - Opened by celinval over 1 year ago - 2 comments

#2419 - Bump Kani version 0.27.0

Pull Request - State: closed - Opened by adpaco-aws over 1 year ago

#2418 - Update dependencies

Pull Request - State: closed - Opened by adpaco-aws over 1 year ago

#2417 - Bump CBMC version to 5.82.0

Pull Request - State: closed - Opened by adpaco-aws over 1 year ago

#2416 - Spurious failure for enum with array data

Issue - State: open - Opened by zhassan-aws over 1 year ago - 1 comment
Labels: [C] Bug, [F] Spurious Failure

#2415 - Add extra_column to benchcomp markdown visualizer

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

#2414 - Implement CSV visualization for benchcomp

Issue - State: open - Opened by karkhaz over 1 year ago
Labels: [C] Feature / Enhancement, Z-Benchcomp

#2413 - Add markdown_results_table benchcomp visualization

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

#2412 - Refactor slow benchcomp regression tests

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

#2411 - Make bookrunner job use latest pages-deploy-action

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

#2410 - Add #VCCs and #program steps benchcomp metrics

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

#2409 - Add --only and --exclude to benchcomp visualize

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

#2408 - Explicitly pass out_file to benchcomp visualizers

Pull Request - State: closed - Opened by karkhaz over 1 year ago - 2 comments

#2407 - Define different function for concrete playback (no user impact)

Pull Request - State: closed - Opened by celinval over 1 year ago - 3 comments

#2406 - Upgrade the toolchain to nightly-2023-04-16

Pull Request - State: closed - Opened by celinval over 1 year ago - 10 comments

#2405 - Use optimized overflow operation everywhere

Pull Request - State: closed - Opened by celinval over 1 year ago - 3 comments

#2404 - Implement `kani::Arbitrary` for `Box<T>`

Pull Request - State: closed - Opened by adpaco-aws over 1 year ago

#2403 - Feature request: Implement `kani::Arbitrary` for `Box<T>`

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

#2402 - Command-line flag to change model target or environment

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

#2401 - Dump full benchcomp YAML results in CI

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

#2400 - Make all visualizations that write to stdout accept an out_file argument

Issue - State: open - Opened by karkhaz over 1 year ago
Labels: [C] Feature / Enhancement, Z-Benchcomp

#2399 - Allow excluding packages from verification with `--exclude`

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

#2398 - Make cargo build-dev produce a proper exit code

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

#2397 - Install system-provided autopep8 where available

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

#2396 - Override std::ptr::align_offset

Pull Request - State: open - Opened by tautschnig over 1 year ago - 1 comment

#2395 - Add size_of annotation to help CBMC's allocator

Pull Request - State: closed - Opened by tautschnig over 1 year ago - 4 comments

#2394 - Avoid global path conditions in Kani's library

Pull Request - State: open - Opened by tautschnig over 1 year ago - 1 comment
Labels: Z-BenchCI

#2393 - Bump Kani version to 0.26.0

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

#2392 - Integrate benchcomp solver comparison with VSCode Extension

Issue - State: open - Opened by karkhaz over 1 year ago - 1 comment
Labels: [C] Feature / Enhancement

#2391 - Update workspace dependencies

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

#2390 - Fix error_on_regression only using last check

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

#2389 - Fix benchcomp path to Kani binary

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

#2388 - Bump CBMC version

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

#2387 - Compare proposed release performance with previous release

Issue - State: open - Opened by karkhaz over 1 year ago
Labels: [C] Feature / Enhancement, Z-Benchcomp

#2386 - Enforce unstable APIs can only be used if the related feature is enabled

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

#2385 - Automatic toolchain upgrade to nightly-2023-02-19

Pull Request - State: closed - Opened by github-actions[bot] over 1 year ago - 1 comment

#2384 - Upgrade Rust toolchain to nightly-2023-02-18

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

#2383 - Update rust toolchain version to nightly-2023-04-16

Issue - State: closed - Opened by celinval over 1 year ago
Labels: Z-Sync Upstream

#2382 - Run benchcomp unit and regression tests in CI

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

#2375 - Feature request: exclude crates from workspace at build time

Issue - State: closed - Opened by andreeaflorescu over 1 year ago
Labels: [C] Feature / Enhancement, [E] User Experience, T-User

#2374 - Unexpected failed check for negative left shift operand

Issue - State: closed - Opened by reisnera over 1 year ago - 12 comments
Labels: [C] Bug, [F] Spurious Failure, T-User

#2370 - Add performance regression comparison in CI

Pull Request - State: closed - Opened by karkhaz over 1 year ago - 5 comments

#2364 - Kani panics during Goto translation for code using bitvec

Issue - State: closed - Opened by weaversa over 1 year ago - 2 comments
Labels: [C] Bug, T-High Priority, [F] Crash, T-User

#2363 - Improve symbolic execution performance when running against concrete values

Issue - State: open - Opened by celinval over 1 year ago - 9 comments
Labels: [E] Performance, [C] Feature / Enhancement, T-CBMC

#2357 - Add unstable attribute to tag experimental APIs

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

#2346 - Make parsers self-documenting

Issue - State: open - Opened by karkhaz over 1 year ago
Labels: Z-Benchcomp

#2345 - Create getting started documentation

Issue - State: open - Opened by karkhaz over 1 year ago
Labels: Z-Benchcomp

#2325 - Automate release

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

#2322 - Run "slow" tests as part of pull request checks

Pull Request - State: open - Opened by tautschnig over 1 year ago - 3 comments

#2314 - Remove duplicated CBMC Viewer version string

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

#2313 - Add scripts to automate dependencies

Pull Request - State: closed - Opened by jaisnan over 1 year ago - 2 comments

#2312 - internal compiler error: assertion failed: `(left == right)`

Issue - State: closed - Opened by nano-o over 1 year ago - 2 comments
Labels: [C] Bug, T-High Priority, [F] Crash, T-User, Z-Kani Compiler

#2302 - Memory blows up on a small program involving String split

Issue - State: open - Opened by zhassan-aws over 1 year ago - 2 comments
Labels: [C] Bug, [E] Performance, T-CBMC

#2300 - Add support for non-deterministic pointer

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

GitHub / model-checking/kani issues and pull requests