generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 135
Closed
Labels
[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.
Description
The handling of MIR's storage markers (StorageLive and StorageDead) introduced in #3063 causes spurious failures.
For example, on tests/kani/Spurious/storage_fixme.rs, the following failures are reported:
** 33 of 305 failed (272 undetermined)
Failed Checks: rust_dealloc must be called on an object whose allocated size matches its layout
File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 86, in __rust_dealloc
Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment
File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: explicit panic
File: "src/main.rs", line 300, in NodeRef::<marker::Dying, marker::Leaf>::force
Failed Checks: called `Option::unwrap()` on a `None` value
File: "/home/ubuntu/.rustup/toolchains/nightly-2024-03-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs", line 1985, in std::option::unwrap_failed
Failed Checks: attempt to add with overflow
File: "src/main.rs", line 336, in Handle::<NodeRef<marker::Dying, marker::Leaf>, marker::KV>::right_edge
Failed Checks: assertion failed: idx <= node.len()
File: "src/main.rs", line 344, in Handle::<NodeRef<marker::Dying, marker::Leaf>, marker::Edge>::new_edge
Failed Checks: free argument must be NULL or valid pointer
File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 88, in __rust_dealloc
Failed Checks: free argument must be dynamic object
File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 88, in __rust_dealloc
Failed Checks: free argument has offset zero
File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 88, in __rust_dealloc
Failed Checks: double free
File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 88, in __rust_dealloc
Failed Checks: dereference failure: pointer NULL
File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: pointer invalid
File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: deallocated dynamic object
File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: dead object
File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: pointer outside object bounds
File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: invalid integer address
File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: deallocated dynamic object
File: "/home/ubuntu/.rustup/toolchains/nightly-2024-03-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs", line 142, in std::alloc::Layout::align
Failed Checks: dereference failure: deallocated dynamic object
File: "/home/ubuntu/.rustup/toolchains/nightly-2024-03-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs", line 129, in std::alloc::Layout::size
Failed Checks: dereference failure: pointer NULL
File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: pointer invalid
File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: deallocated dynamic object
File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: dead object
File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: pointer outside object bounds
File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: invalid integer address
File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: deallocated dynamic object
File: "src/main.rs", line 159, in NodeRef::<marker::Dying, marker::Leaf>::as_leaf_ptr
Failed Checks: dereference failure: deallocated dynamic object
File: "src/main.rs", line 180, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: pointer NULL
File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: pointer invalid
File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: deallocated dynamic object
File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: dead object
File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: pointer outside object bounds
File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: invalid integer address
File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: unwinding assertion loop 0
File: "src/main.rs", line 527, in Handle::<NodeRef<marker::Dying, marker::Leaf>, marker::Edge>::deallocating_end
Metadata
Metadata
Assignees
Labels
[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.