Description
CBMC version: 5.67.0
Operating system: N/A
The Ask
Implement a vacuity check for function contracts
Background
It is easy to write a function contract that embodies a contradiction:
- requires *x > 10
- assigns *y
- ensures *x < 10
This contract is impossible to satisfy. Perhaps the author meant assigns *x?
When writing a proof of a program we may proceed from the root of the proof toward the leaves. We may never get to some leaves because of the amount of available time, or perhaps some proofs are just not feasible with the technology we have.
Our CI infrastructure should highlight all function contracts used in a proof but not yet proved. That tells us what assumptions we are relying on. But what if some of those assumptions are tantamount to assuming false because we've relied on a broken contract like the one above. We need a vacuity check mechanism that can be used to find these.