From 5d0edb8e696c91be80a62f403d41d7e9fac3d5f5 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 20 Sep 2024 19:29:22 -0400 Subject: [PATCH] check explicitly that fn resolves --- kani-compiler/src/kani_middle/list.rs | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/kani_middle/list.rs b/kani-compiler/src/kani_middle/list.rs index 9d61aeb4a554..5d03bb86cb20 100644 --- a/kani-compiler/src/kani_middle/list.rs +++ b/kani-compiler/src/kani_middle/list.rs @@ -53,12 +53,13 @@ fn count_contracts(tcx: TyCtxt, check_body: &Body) -> usize { if let TerminatorKind::Call { ref func, .. } = bb.terminator.kind { let fn_ty = func.ty(check_body.locals()).unwrap(); if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = fn_ty.kind() { - let instance = Instance::resolve(fn_def, &args).unwrap(); - // For each precondition or postcondition, increment the count - if matches_function(tcx, instance.def, "KaniAssume") - || matches_function(tcx, instance.def, "KaniAssert") - { - count += 1; + if let Ok(instance) = Instance::resolve(fn_def, &args) { + // For each precondition or postcondition, increment the count + if matches_function(tcx, instance.def, "KaniAssume") + || matches_function(tcx, instance.def, "KaniAssert") + { + count += 1; + } } } }