Add support for type invariants (#197)
* Cleanup a bit Ir_of_gospel.state function
* Add some new functions to Builder
Mostly add `list_or` and `enot` that will soon be needed, but take the
opportunity to move `qualify` and redefine some functions that where
worngfully using `evar` on qualified names.
* Add invariants in intermediate representation
* Translate invariants and check them in postcond
This will guarantee preservation of type invariants for `sut`
* Check type invariants in `init_state` and add some tests
* Update Changelog
3e211f
-
Mar 13 15:10 +00:00