We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 81fda70 commit 2755a04Copy full SHA for 2755a04
library/kani/src/lib.rs
@@ -136,7 +136,13 @@ pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
136
#[inline(never)]
137
#[allow(dead_code)]
138
fn any_raw_inner<T>() -> T {
139
- unimplemented!("Kani any_raw_inner");
+ // while we could use `unreachable!()` or `panic!()` as the body of this
140
+ // function, both cause Kani to produce a warning on any program that uses
141
+ // kani::any() (see https://github.com/model-checking/kani/issues/2010).
142
+ // This function is handled via a hook anyway, so we just need to put a body
143
+ // that rustc does not complain about. An infinite loop works out nicely.
144
+ #[allow(clippy::empty_loop)]
145
+ loop {}
146
}
147
148
/// Function used to generate panic with a static message as this is the only one currently
0 commit comments