pub fn block_on<T>(fut: impl Future<Output = T>) -> T
Expand description
A very simple executor: it polls the future in a busy loop until completion
This is intended as a drop-in replacement for futures::block_on
, which Kani cannot handle.
Whereas a clever executor like block_on
in futures
or tokio
would interact with the OS scheduler
to be woken up when a resource becomes available, this is not supported by Kani.
As a consequence, this function completely ignores the waker infrastructure and just polls the given future in a busy loop.
Note that spawn
is not supported with this function. Use block_on_with_spawn
if you need it.