Handle const generics in stubbing code (#4323)

The recent support for stubbing trait impls #4250 assumed that generic
args must be types which caused a crash when they're not. This PR takes
into account that case.

Resolves #4322 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: zhassan-aws

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

tests/expected/stubbing-const-generics/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

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<const C: usize> {
+    _a: [i32; C],
+    x: bool,
+}
+
+impl<const C: usize> Foo<C> {
+    fn foo(&self) -> bool {
+        self.x
+    }
+}
+
+pub fn bar<const C: usize>(x: &Foo<C>) -> bool {
+    false
+}
+
+#[kani::proof]
+#[kani::stub(Foo::foo, bar)]
+fn main() {
+    let f = Foo { _a: [1, 2, 3], x: true };
+    assert!(!f.foo());
+}