Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / model-checking/kani issues and pull requests

#2668 - Encapsulate KaniAttributes

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

#2667 - Automatic toolchain upgrade to nightly-2023-08-05

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

#2666 - Bump Kani version to 0.34.0

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

#2665 - Update dependencies

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

#2664 - Avoid unnecessary allocations in MIR passes

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

#2663 - Fix codegen of constant byte slices

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

#2662 - bump cbmc to v5.89.0

Pull Request - State: closed - Opened by remi-delmas-3000 over 1 year ago
Labels: Z-BenchCI

#2661 - Update toolchain to nightly 2023-08-04

Pull Request - State: closed - Opened by remi-delmas-3000 over 1 year ago - 1 comment
Labels: Z-BenchCI

#2660 - Fix SIMD field access

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

#2659 - ICE: Kani crashes when there's an access to SIMD field in a generic context

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

#2658 - Support for stubbing out foreign functions

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

#2657 - Fix broken benchcomp link to point to right location

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

#2656 - Calling `Vec::extend` with a constant slice yields false-positive failures

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

#2655 - Function Contracts: Support for defining and checking `requires` and `ensures` clauses

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

#2654 - Change default solver to CaDiCal

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

#2653 - Change Kani's default solver

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

#2652 - Feature Request: Function Contracts

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

#2651 - Add support to simd_bitmask intinsic #2131

Issue - State: closed - Opened by rahulku over 1 year ago - 1 comment

#2650 - Spurious failure on harness from s2n-quic

Issue - State: closed - Opened by zhassan-aws over 1 year ago - 5 comments
Labels: [C] Bug, T-High Priority, [F] Spurious Failure, T-User, T-CBMC

#2649 - Kani `concrete-playback --json-ui` gives a non-json response

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

#2648 - Kani does not lock access to build artifacts, leading to crashes if executed concurrently

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

#2647 - Add ability to run proofs in parallel

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

#2646 - [Feature Request] Ability to stub out function on primitive types (such as `[T]`)

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

#2645 - Add integer overflow checking for simd_div and simd_rem

Pull Request - State: closed - Opened by reisnera over 1 year ago - 13 comments

#2644 - Include temporary test files to gitgnore

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

#2643 - Propogate backend options into goto-synthesizer

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

#2642 - Investigate how coverage checks affect performance

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

#2641 - Create a tool for aggregating coverage results

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

#2640 - Report source-based coverage results

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

#2639 - Avoid confusing results in coverage reports

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

#2638 - Export coverage results to a well-supported output

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

#2637 - Improve benchcomp documentation

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

#2636 - Create user-friendly output for coverage

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

#2635 - Improve tests for coverage

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

#2634 - Proof with `AnySlice` does not terminate, memory grows unbounded

Issue - State: closed - Opened by arctic-alpaca over 1 year ago - 11 comments
Labels: [C] Bug, T-High Priority, [E] Performance, T-User

#2633 - Add support to array-based SIMD

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

#2632 - Implement `simd_reduce_all`

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

#2631 - ICE: Intrinsic `simd_add` crashes when using float vector

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

#2630 - Add unchecked/SIMD bitshift checks and disable CBMC flag

Pull Request - State: closed - Opened by reisnera over 1 year ago - 1 comment
Labels: Z-BenchCI

#2629 - How does kani ensure memory safety?

Issue - State: closed - Opened by kiyoakii over 1 year ago - 6 comments

#2628 - Delay writing metadata file (no UX impact)

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

#2627 - Publish documentation for library component (e.g. `kani::any()` et al) to docs.rs

Issue - State: closed - Opened by roypat over 1 year ago - 5 comments
Labels: [C] Feature / Enhancement, [C] Documentation

#2626 - Kani crates aren't forced to have the same version

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

#2625 - Bump Kani version

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

#2624 - Bump dependencies

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

#2623 - Bump CBMC version

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

#2622 - Investigate more efficient ways to encode enums

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

#2621 - Stubbing with Contracts

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

#2620 - RFC Function Contracts

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

#2619 - Print Kani version

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

#2617 - Print Kani development version info

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

#2616 - Upgrade Rust toolchain to nightly-2023-07-01

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

#2615 - Upgrade Rust toolchain to nightly-2023-6-26

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

#2614 - Bump CBMC version to 5.88.0

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

#2613 - Update dependencies

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

#2612 - RFC: Line Coverage

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

#2611 - [CI check] Add coverage output

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

#2610 - Coverage option that does not require `cbmc-viewer`

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

#2609 - Line coverage reports

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

#2608 - Add coverage test suite

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

#2607 - Add a script to measure build performance

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

#2606 - Automate running benchmarks in PRs that are more likely to impact performance

Issue - State: closed - Opened by celinval over 1 year ago - 3 comments
Labels: [C] Internal, [I] CI / Infrastructure

#2605 - Add new options to compiletest

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

#2604 - Do not run benchcomp in every PR

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

#2603 - Automatic toolchain upgrade to nightly-2023-06-25

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

#2602 - Bump Kani version to 0.32.0

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

#2601 - Adds posix_memalign to the list of supported builtins

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

#2600 - Automatic toolchain upgrade to nightly-2023-06-24

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

#2597 - Avoiding naming clashes for `result` in function contracts

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

#2596 - Unstable gating for function contracts

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

#2593 - Generate `benchcomp.yaml` documentation from schema

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

#2592 - Create schema for benchcomp.yaml

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

#2591 - Automatic toolchain upgrade to nightly-2023-06-23

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

#2590 - ICE: Kani compiler crashes when initializing a SIMD struct

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

#2589 - Invalid stub cause different ICE while monomorphizing the code

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

#2587 - Stub of extern functions including C-FFI

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

#2585 - Add test coverage for coverage information

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

#2584 - Automatic toolchain upgrade to nightly-2023-06-22

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

#2577 - Basic, Explicit Contract Checking Workflow

Issue - State: closed - Opened by JustusAdam over 1 year ago - 1 comment

#2574 - RFC: Output - Reduce reported checks/properties

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

#2573 - RFC: Output - Harness listing/enumeration

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

#2572 - RFC: Output - Other tool versions

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

#2570 - Output - Kani version

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

#2567 - Generated unit test does not contain enough values

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

#2565 - Create a Boogie AST crate

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

#2562 - RFC: Output - Alternative check format

Issue - State: open - Opened by adpaco-aws over 1 year ago - 3 comments
Labels: [C] Feature / Enhancement, T-RFC

#2559 - Tracking issue for Kani's unstable async library, feature `async-lib`

Issue - State: open - Opened by fzaiser over 1 year ago - 1 comment
Labels: T-TrackingIssue

#2557 - Adds support for sysconf

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

#2555 - Support for requires and ensures clauses

Pull Request - State: closed - Opened by JustusAdam over 1 year ago - 15 comments

#2546 - Quantifiers for function contracts

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

#2545 - Implement `old()` function for contracts

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

#2539 - Documentation doesn't discuss solver tradeoffs and ways to speed up verification

Issue - State: open - Opened by adpaco-aws over 1 year ago
Labels: T-User, [C] Documentation

#2524 - [Stubbing] Stubbing of trait method results in "unable to find `<...>` inside struct `<...>`"

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

#2520 - Create schema for suite.yaml and result.yaml

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

#2517 - Memory blows up on a deterministic BTreeSet harness

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