Support drop_in_place (needed for tokio)
If you clone the tokio repository and run cargo kani, you get a lot of warnings about unsupported features, one of them is drop_in_place, example:
warning: Found the following unsupported constructs:
- Rvalue::ThreadLocalRef (7)
- drop_in_place for drop_unimplemented__RINvNtCs4YygHDVoDdI_4core3ptr13drop_in_placeNtNtNtCsfcET2xiHyR1_3std2io5error5ErrorECs9FYAfFSAVYQ_3mio (1)
- try (1)
The lack of ThreadLocalRef and try can be worked around by disabling certain functions in functions.rs:
name if name.contains("metadata") => true,
name if name.contains("std::sync::atomic::AtomicPtr") => true,
name if name.contains("runtime::task::harness::Harness") => true,
name if name.contains("runtime::task::core::Cell") => true,
But even if we do this, we get an error codegen'ing std::ptr::drop_in_place::<runtime::task::core::Cell<runtime::blocking::task::BlockingTask<std::boxed::Box<[closure@tokio/src/io/blocking.rs:152:52: 152:59]>>, runtime::blocking::schedule::NoopSchedule>>. The assertion failure happens in https://github.com/model-checking/kani/blob/16f10e9a0f40e4e50a1869b09361c280ae840d21/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs#L178.
It is important to fix this bug to support tokio