Sacha Ayoun

@tjbell Onivim will (or maybe already does) support vscode extensions. I've started writing a [vscode extension](https://github.com/giltho/comby-vscode). There are a lot of choices I don't like, but vscode doesn't allow to...

Would be great to do that. When I wrote the "extension" (very much in quote since it's barely a proof of concept...), such custom panels weren't possible. I think it...

It turns out that Kani's own test suite has undefined behaviour that isn't really caught because of that, with a mix of that and the `any_raw` issue, pointed out [there](https://github.com/model-checking/kani/issues/1394)...

I'm ok with that, but it means actively taking the decision to get stmt.rs and cbmc out of sync and so I went with a softer solution first But happy...

Replacing the Nondet expression with Deinit does raise one question: what happens with the [NondetTransformer](https://github.com/model-checking/kani/blob/main/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs#L56-L66) ? 1) I don't understand if and when it's called. If it was, I would...

Ok fixed the various comments from @danielsn That being said, after rereading my PR with a fresh post-weekend mind, I'm a bit unhappy with a Poison expression. ## The argument...

Note that this behaviour of expliciting the value of padding might create discrepancies between C and GotoC. Take the following example ```c struct S { u8 x; [24 bit padding]...

Updated to a deinit statement. This is not ready to be merged for two reasons: - [x] First I need to sync my Kanillian branch with it to make sure...

~I have one broken test in the regression test suite, I'll try to figure out what's wrong, but I'm not sure how to approach that~ That was a local nonsense

> i.e., offsets that go out-of-bounds, are frequently used Do you have an example of that? The stdlib is tested with MIRI I believe, and MIRI detects creating OOB pointers...