It would be nice to also support statement contracts, as defined in ACSL, I think they are not supported?
They are like function contracts but over individual statements (which may be a block of multiple statement). It would be useful for modularising verification for large functions.