Skip to content

ICE: "assign statement with unequal types" ; StructTag / StructTag  #2237

@matthiaskrgr

Description

@matthiaskrgr

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.[F] CrashKani crashed

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions