Daniel Schwartz-Narbonne

So, I don't think this needs to be addressed by this PR (or ever), but it's somewhat weird to me this "config"/"receiver_config"/"metadata" split right now. All three are always required...

Why is it that the emission of some data is immediately followed by a flush operation sometimes, but not always? _Originally posted by @sanchda in https://github.com/DataDog/libdatadog/pull/541#discussion_r1687011188_

- [x] Cast/cast_abstract_args_to_concrete.rs (fixed in #2999) - [ ] FatPointers/boxmuttrait.rs - [ ] FatPointers/boxslice1.rs - [ ] Variadic/main.rs

We currently need to support this for the standard library. We're doing the standard `to_pointer` cast in CBMC, but haven't confirmed this is correct

Requested feature: Enable verification of code that uses C-FFI Use case: Any code that has mixed language calls, and the user wants to verify Link to relevant documentation (Rust reference,...

Unexpected failure: "Function `mmap` with missing definition is unreachable"

1

I tried this code: https://github.com/danielsn/kani/tree/kani-1743 using the following command line invocation: ``` cd memory_model cargo kani ``` with Kani version: 0.11 I expected to see this happen: Kani verified the...

Audit Vtable generation for dynamic traits

5

RMC handles dynamic traits by making a vtable for each trait, which maps virtual calls to the function pointer that implements the call. As of 2021-09-01, our implementation of dynamic...

Feature request: detect when Rustc hides UB (undefined behavior) when generating MIR

1

RMC operates at the MIR level. It is possible that the MIR generated by Rustc may make implementation decisions that hide UB. ## Likelihood: We do not have data on...