From 9f2d97b3325aa5009f28dc323f83e4acec65af1b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Dec 2023 08:43:08 +0000 Subject: [PATCH] validate_instance: make sure we actually have a body --- kani-compiler/src/kani_middle/stubbing/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 03298456c522..41ee18c80efc 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -51,7 +51,7 @@ pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool { checker.visit_body(&item.body()); checker.is_valid() } else { - true + instance.body().is_some() } }