-
Notifications
You must be signed in to change notification settings - Fork 99
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
ICE: mismatch in number of fields and values. #2680
Comments
Hi @XAMPPRocky. Thanks for reporting this issue. This seems to be the same as #1594. We'll look into it. |
For the record, here are the steps to reproduce the crash:
|
Here is a smaller reproducer involving the
use bitvec::prelude::*;
#[kani::proof]
fn main() {
let five = [0u8; 5];
for _ in five.view_bits::<Msb0>().chunks(5) {}
}
This produces:
|
Thanks it would be good to have a separate issue template for ICEs that includes those steps. |
Here's a stand-alone minimal reproducer: use std::marker::PhantomData;
pub struct Foo<R> {
x: u8,
_t: PhantomData<R>,
}
#[kani::proof]
fn main() {
const C: Foo<usize> = Foo {
x: 0,
_t: PhantomData,
};
assert_eq!(C.x, 0);
}
|
@remi-delmas-3000 any update here? This seems to be causing a crash in a second crate. Thanks |
… also include ZSTs (#2794) This change considers another case for the code generation of scalar data. In particular, when the expected type is an ADT, we previously considered two cases: either there is no field or there is one. But in cases where the ADT includes a ZST, the ADT will contain multiple fields: one associated to the scalar data, and other fields associated to the ZSTs. In those cases, we ended up crashing as in #2680: ```rust error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9: assertion failed: `(left == right)` left: `2`, right: `1`: Error in struct_expr; mismatch in number of fields and values. StructTag("tag-_161424092592971241517604180463813633314") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]. thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9: assertion failed: `(left == right)` left: `2`, right: `1`: Error in struct_expr; mismatch in number of fields and values. StructTag("tag-_161424092592971241517604180463813633314") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }] ``` With the changes in this PR, that's no longer the case. Resolves #2364 Resolves #2680
I tried this code:
tests/kani.rs
using the following command line invocation:
with Kani version:
I expected to see this happen: it works
Instead, this happened:
The text was updated successfully, but these errors were encountered: