Commit 0560b33
martin
Convert the assertions in std_expr.h to invariants as a demonstration.
Many of these are split into two invariants are there is the specific
precondition (before calling to_div_expr it is your responsibility to
check you have an exprt with id() == ID_div) and a general data structure
invariant (all ID_div exprts should have exactly two operands).
A few invariants are commented out as I believe they hold but they are
not currently enforced. This commit should not change the functionality
of the code.1 parent 0a60788 commit 0560b33
1 file changed
+394
-123
lines changed
0 commit comments