From 505700aa8c4605187cc07919830991cbe6075762 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 6 Dec 2023 11:30:18 -0800 Subject: [PATCH] Work around issue with is_foreign_item --- kani-compiler/src/kani_middle/reachability.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 216feb66fb87..9e35e273bb66 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -485,7 +485,10 @@ fn to_fingerprint(tcx: TyCtxt, item: &InternalMonoItem) -> Fingerprint { /// Return whether we should include the item into codegen. fn should_codegen_locally(instance: &Instance) -> bool { - !instance.is_foreign_item() + // TODO: This should only check is_foreign_item() or even `has_body()`. + // We need https://github.com/rust-lang/rust/pull/118681 to land first. + //!instance.is_foreign_item() + instance.body().is_some() } fn collect_alloc_items(alloc_id: AllocId) -> Vec {