Warnings from purity checks on assertions and assumptions

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

We should at least be checking this, and should report warnings (not errors because it might break too many existing proofs) to users when their assertions / assumptions have side effects.

[feliperodri]

@diffblue/diffblue-opensource

[tautschnig]

Why is this the right thing to do? Conversely, why is it wrong to have side effects in assertions or assumptions? Yes, there is the risk that people have a side effect in assert(expression-with-side-effect) and then compile their code with -DNDEBUG. Is this the potential pitfall that you are trying to address?

More generally, any warnings beyond those produced by a standard compiler cater the risk of breaking build processes.