add ability to check user-supplied invariants in src code

[nguyenthanhvuh]

e.g., support the syntax

// code ... vcheck(x > y);