search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.12k stars 83 forks source link

Integrate `mmap` model from CBMC #2543

Open feliperodri opened 1 year ago

feliperodri commented 1 year ago

Currently, we have harnesses blocked by unsupported libc libraries. Current blockers:

We should rely on CBMC C Library models while make sure that customers can create their own stubs of these models in Kani as well.

feliperodri commented 1 year ago

We are unable to fully support mmap due to the following issue https://github.com/diffblue/cbmc/issues/7773.

celinval commented 1 year ago

I think we need a better mechanism to import these functions to Kani. In the meantime, we might want to keep doing this by demand.

roypat commented 1 year ago

For what its worth with the mmap one, firecracker only uses MAP_ANONYMOUS without MAP_FIXED, which if I read CBMC code correctly wont run into the deprecation issue you linked.