Check purity of loop contracts

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

Check purity of loop contracts.

[feliperodri]

the internal mechanics for checking side effects is now available through #6887, but loop contracts need to be ported over to DFCC)

[qinheping]

The purity checks of loop contracts are already implemented.
Invariant clauses: https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/goto_convert.cpp#L877
Decreases clauses: https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/goto_convert.cpp#L891
Assigns clauses: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/c_typecheck_code.cpp#L505