generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 141
Open
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] CrashKani crashedKani crashed
Description
I tried this code:
fn id<'c, 'b>(f: &'c &'b dyn Fn(&i32)) -> &'c &'b dyn Fn(&'static i32) {
f
}
#[kani::proof]
fn main() {
let f: &dyn Fn(&i32) = &|x| {};
id(&f);
}using the following command line invocation:
kani <file>
with Kani version: 0.22.0
I expected to see this happen: explanation
Instead, this happened: explanation
warning: unused variable: `x`
--> issue-47638.rs:7:30
|
7 | let f: &dyn Fn(&i32) = &|x| {};
| ^ help: if this is intentional, prefix it with an underscore: `_x`
|
= note: `#[warn(unused_variables)]` on by default
thread '<unnamed>' panicked at 'assertion failed: `(left == right)`
left: `Pointer { typ: StructTag("tag-_4019304343755080956::FatPtr") }`,
right: `Pointer { typ: StructTag("tag-_11920736723328834979::FatPtr") }`: Error: assign statement with unequal types lhs Pointer { typ: StructTag("tag-_4019304343755080956::FatPtr") } rhs Pointer { typ: StructTag("tag-_11920736723328834979::FatPtr") }', cprover_bindings/src/goto_program/stmt.rs:170:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md
[Kani] current codegen item: codegen_function: id
_RNvCs4Ip2CT9LJTJ_11issue_476382id
[Kani] current codegen location: Loc { file: "/tmp/im/issue-47638.rs", function: None, start_line: 1, start_col: Some(1), end_line: 1, end_col: Some(71) }
warning: 1 warning emitted
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] CrashKani crashedKani crashed