Repository navigation
ICE: "assign statement with unequal types" ; StructTag / StructTag #2237
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
Activity
matthiaskrgr commentedon Feb 25, 2023
[-]ICE: "assign statement with unequal types" [/-][+]ICE: "assign statement with unequal types" ; StructTag / StructTag [/+]zhassan-aws commentedon Feb 25, 2023
Thanks for filing these issues @matthiaskrgr. Are the examples from the Rust compiler unit tests? If so, are you running them manually or through a script? We were interested in including rustc unit tests in our regressions to capture such corner cases.
matthiaskrgr commentedon Feb 25, 2023
Yes, these are rustc tests. 🙂
I've added some cheap kani support to https://github.com/matthiaskrgr/icemaker/ yesterday night and I try to slap kani::proof onto fndefs that I think kani can run and filter out the crashes.
zhassan-aws commentedon Feb 25, 2023
Cool, thanks 🙂
matthiaskrgr commentedon Feb 26, 2023
BTW do you kani folks have by any chance some automatic way to instrument fn parameters with
kani::any()?Would become
and could be tested automatically
zhassan-aws commentedon Feb 26, 2023
Not yet.
matthiaskrgr commentedon Mar 2, 2023
ok, I think I got it to roughly to work :D
https://github.com/matthiaskrgr/icemaker/blob/master/src/run_commands.rs#L940
I noticed some problems where collection types like String or Vec would not impl kani::arbitrary but I try to fall back to
Default::default()instead ofkani::any()in such cases(there may still be a bunch of cases where I just break the code without noticing, but eh... )
zhassan-aws commentedon Mar 2, 2023
Cool! Yeah,
kani::any()is only supported for primitive types at the moment:https://github.com/model-checking/kani/blob/main/library/kani/src/arbitrary.rs
So you might want to do the opposite: provide a list of supported types and default anything else.
matthiaskrgr commentedon Jun 2, 2023
This one is probably related:
matthiaskrgr commentedon Nov 12, 2023
Triage: kani 0.40
original example fixed, #2237 (comment) still crashing
feliperodri commentedon Sep 25, 2026
Triaged against
main(de756c9, nightly-2026-09-23, Kani 0.68.0).kani code.rs→Complete - 1 successfully verified harnesses, 0 failures, 1 total.Closing as no longer reproducible — please reopen if you can still hit it on
main.