Sacha Ayoun

Oh god... I just realised what happened. There was a interleaved alternation of modifying the `kani-fixme/...` file and the `kani/...` file, only the second one should be modified... I ended...

Doesn't solve @celinval's question: should this be added to the repo?

This is due to the fact that Kani encodes rust str constants into string constants for CBMC However, CBMC automatically null-terminates C strings, and therefore, this is indeed not out-of-bound...

> Can you please explain why that should be the default? I'm not convinced that's the case. Writing code that depends on the memory layout should be considered a developer...

> Here is an example of a bad user experience in my mind Very good point, it's very dangerous for tests to be non-reproducible. > For the record, there is...

There's an argument for a fixed seed which is "yes it's fixed, but it's possibly different from the standard compiler choice". Also, note that in general, even without any randomization,...

> One more question about this one. What about the std library? I'm assuming this option wouldn't randomize the std library structures, right? Or are we planning to rebuild std?...

I looked into how to get the seed, and actually... It looks like the randomization is already deterministic 😆 `-Zrandomize-layout` isn't really random at all, but allows you to change...

1. True! It's a bit annoying that the user will not be able to use the LSP interface to rerun the tests, since it wouldn't set that param correctly :(...

Fixed according to discussion and rebased on main