Module bytecode::inconsistency_check
source · Expand description
Instrument assert false;
in strategic locations in the program such that if proved, signals
an inconsistency among the specifications.
The presence of inconsistency is a serious issue. If there is an inconsistency in the
verification assumptions (perhaps due to a specification mistake or a Prover bug), any false
post-condition can be proved vacuously. The InconsistencyCheckInstrumentationProcessor
adds
an assert false
before
- every
return
and - every
abort
(if theunconditional-abort-as-inconsistency
option is set). In this way, if the instrumentedassert false
can be proved, it means we have an inconsistency in the specifications.
A function that unconditionally abort might be considered as some form of inconsistency as well.
Consider the function fun always_abort() { abort 0 }
, it might seem surprising that the prover
can prove that spec always_abort { ensures 1 == 2; }
. If this function aborts unconditionally,
any post-condition can be proved. Checking of this behavior is turned-off by default, and can
be enabled with the unconditional-abort-as-inconsistency
flag.