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.

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.

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.

Status: Open.

#299 In model-checking/kani;

· danielsn opened on Jul 6, 2021

Correctness of CBMC Serialization

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

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.

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

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

Status: Open.

#316 In model-checking/kani;

· danielsn opened on Jul 8, 2021

Soundness documentation

[C] DocumentationAdditions and improvements to our documentationAdditions and improvements to our documentation

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

Status: Open.

#1495 In model-checking/kani;

· danielsn opened on Aug 11, 2022