diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 947ef745a97a..12f96ff3dc67 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -59,7 +59,9 @@ fn generic_args_len_without_self(args: &GenericArgs) -> usize { return len; } let has_self = args.0.iter().any(|arg| { - if let TyKind::Param(param_ty) = arg.expect_ty().kind() { + if let Some(ty) = arg.ty() + && let TyKind::Param(param_ty) = ty.kind() + { param_ty.name == "Self" } else { false diff --git a/tests/expected/stubbing-const-generics/expected b/tests/expected/stubbing-const-generics/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/stubbing-const-generics/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/stubbing-const-generics/main.rs b/tests/expected/stubbing-const-generics/main.rs new file mode 100644 index 000000000000..7a7dbdcc8a1e --- /dev/null +++ b/tests/expected/stubbing-const-generics/main.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z stubbing +//! Check that Kani supports stubbing methods for structs with const generics. +//! This was previously crashing: +//! https://github.com/model-checking/kani/issues/4322 + +struct Foo { + _a: [i32; C], + x: bool, +} + +impl Foo { + fn foo(&self) -> bool { + self.x + } +} + +pub fn bar(x: &Foo) -> bool { + false +} + +#[kani::proof] +#[kani::stub(Foo::foo, bar)] +fn main() { + let f = Foo { _a: [1, 2, 3], x: true }; + assert!(!f.foo()); +}