Feature request: annotate loop unwinding bounds in source code

[tautschnig]

It would be nice to have pragmas or the likes available to specify loop unwinding bounds directly in the source code. (Kani already supports this.)