Statically check parts of the RTS code with Frama-C

[nomeata]

In particular, that all IDL memory access is within bounds.

Also splits rts.c into several files.

[crusso]

A pro-forma LGTM

[nomeata]

Thanks for the approval. I should at least add a section to the README explaining the setup and what is checked etc.

[nomeata]

Hmm, might not actually work for dynamic arrays the way I would want it to… (asked question at https://stackoverflow.com/q/57168439/946226). I should look into the other options too.

[chenyan-dfinity]

Can we use Rust for RTS code for IDL? Most of the memory issues will be gone with rust's type system.

[nomeata]

Can we use Rust for RTS code for IDL? Most of the memory issues will be gone with rust's type system.

I tried that first, but the toolchain wasn’t up to creating dynamic Wasm modules yet.

And I don’t think the memory issues will go away: We’d still be interfacing with the completely unsafe RTS parts written in WebAssembly directly, and thus can’t use the the Rust type checker for most stuff at the interface.

That said, I would still prefer to be able to write this in Rust… Eventually, I guess.

[nomeata]

Probably not master material