From 90fc2b36319ece0e8d000bad11307f21f001cec9 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 21 Dec 2022 16:10:52 -0800 Subject: [PATCH] Eliminate source of caller_location warnings in kani library --- library/kani/src/lib.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 70c407d3607b..d39e3062ce9e 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -136,7 +136,13 @@ pub(crate) unsafe fn any_raw_internal() -> T { #[inline(never)] #[allow(dead_code)] fn any_raw_inner() -> T { - unimplemented!("Kani any_raw_inner"); + // while we could use `unreachable!()` or `panic!()` as the body of this + // function, both cause Kani to produce a warning on any program that uses + // kani::any() (see https://github.com/model-checking/kani/issues/2010). + // This function is handled via a hook anyway, so we just need to put a body + // that rustc does not complain about. An infinite loop works out nicely. + #[allow(clippy::empty_loop)] + loop {} } /// Function used to generate panic with a static message as this is the only one currently