search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
839 stars 262 forks source link

Warnings from purity checks on assertions and assumptions #7189

Open feliperodri opened 2 years ago

feliperodri commented 2 years ago

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 commented 2 years ago

@diffblue/diffblue-opensource

tautschnig commented 2 years ago

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.