List view

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

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

[F] SoundnessKani failed to detect an issueKani failed to detect an issue

Status: Open.

#297 In model-checking/kani;

· danielsn opened on Jul 6, 2021

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

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

[F] SoundnessKani failed to detect an issueKani failed to detect an issue

Status: Open.

#298 In model-checking/kani;

· danielsn opened on Jul 6, 2021

Audit Vtable generation for dynamic traits

[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.

[F] SoundnessKani failed to detect an issueKani failed to detect an issue

Status: Open.

#299 In model-checking/kani;

· danielsn opened on Jul 6, 2021

Correctness of CBMC Serialization

[F] SoundnessKani failed to detect an issueKani failed to detect an issue

T-CBMCIssue related to an existing CBMC issueIssue related to an existing CBMC issue

Status: Open.

#302 In model-checking/kani;

· danielsn opened on Jul 6, 2021

Linking may not follow Rust rules

[F] SoundnessKani failed to detect an issueKani failed to detect an issue

T-CBMCIssue related to an existing CBMC issueIssue related to an existing CBMC issue

Status: Open.

#303 In model-checking/kani;

· danielsn opened on Jul 6, 2021

Audit Correctness of CBMC backend

[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.

[F] SoundnessKani failed to detect an issueKani failed to detect an issue

Status: Open.

#310 In model-checking/kani;

· danielsn opened on Jul 8, 2021

Object aliasing violations are not detected

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

[E] Unsupported UBUndefined behavior that Kani does not detectUndefined behavior that Kani does not detect

[F] SoundnessKani failed to detect an issueKani failed to detect an issue

Status: Open.

#314 In model-checking/kani;

· danielsn opened on Jul 8, 2021

Global ASM is not supported

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

[E] Unsupported ConstructAdd support to an unsupported constructAdd support to an unsupported construct

[F] SoundnessKani failed to detect an issueKani failed to detect an issue

Status: Open.

#316 In model-checking/kani;

· danielsn opened on Jul 8, 2021

Kani compilation fails when running cargo kani in a proc macro crate with crate-type specified.

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.

Status: Open.

Bug

#2038 In model-checking/kani;

· celinval opened on Dec 23, 2022

Spurious failure on Prost check_duration_roundtrip

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.

T-UserTag user issues / requestsTag user issues / requests

Z-Kani CompilerIssues that require some changes to the compilerIssues that require some changes to the compiler

Status: Open.

Bug

#2178 In model-checking/kani;

· danielsn opened on Feb 2, 2023

Kani doesn't handle system calls

[E] Unsupported ConstructAdd support to an unsupported constructAdd support to an unsupported construct

[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.

T-CBMCIssue related to an existing CBMC issueIssue related to an existing CBMC issue

T-UserTag user issues / requestsTag user issues / requests

Status: Open.

Bug

#2284 In model-checking/kani;

· adpaco-aws opened on Mar 8, 2023

Mutable static variables usage in contract verification trigger UB

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.

Z-ContractsIssue related to code contractsIssue related to code contracts

Status: Open.

Bug

#3298 In model-checking/kani;

· celinval opened on Jun 27, 2024

Confusing coverage result: Uncovered end of block on if statement

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.

[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.

Z-UnstableFeatureIssues that only occur if a unstable feature is enabledIssues that only occur if a unstable feature is enabled

Status: Open.

Bug

#3455 In model-checking/kani;

· adpaco-aws opened on Aug 20, 2024

Confusing coverage result: Uncovered argument for match

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.

[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.

Z-UnstableFeatureIssues that only occur if a unstable feature is enabledIssues that only occur if a unstable feature is enabled

Status: Open.

Bug

#3456 In model-checking/kani;

· adpaco-aws opened on Aug 20, 2024

Some coverage results point to non-existing regions

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.

[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.

Z-UnstableFeatureIssues that only occur if a unstable feature is enabledIssues that only occur if a unstable feature is enabled

Status: Open.

Bug

#3543 In model-checking/kani;

· adpaco-aws opened on Sep 23, 2024

Tracking Issue: Disabling CBMC's NaN checks

[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.

Status: Open.

#3875 In model-checking/kani;

· rajath-mk opened on Feb 5, 2025