Xavier Denis

Inherit trusted attribute from parents

4

Here's a rough prototype of what was proposed to solve #1067. I need to actually add tests here, but it should cover the intended usecase. There's a wrinkle in the...

Rename `ShallowModel` and `DeepModel`

10

With @jhjourdan we talked for years at this point about how we should rename the confusingly named `Shallow` and `DeepModel` traits. Working on Gillian-Rust I was once again confronted by...

Adopt Why3Find

2

Why3 Find is finally public: https://git.frama-c.com/pub/why3find. We should integrate this into creusot to ship a complete CLI driven workflow for verification. Once we have this we should also start producing...

#904 Raised the question of _inherent_ laws, laws which are added to types and are thus brought into scope when that type is used. This would be quite interesting, and...