check explicitly that fn resolves

model-checking · Sep 20, 2024 · 5d0edb8 · 5d0edb8
1 parent e41c2b6
commit 5d0edb8
Showing 1 changed file with 7 additions and 6 deletions.
diff --git 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;
+ }
  }
  }
  }