Adds the option to automatically detect contradictions in specifications (we call this smoke detection), which lead to the verifier being able to prove anything (even false). This is done by inserting refute false at various locations in the code; if one of them fails, the specification is unsound. More specifically, these refute statements are added
at the end of each method body (to catch unsatisfiable preconditions),
at the end of each loop body,
at the end of each if/else body,
before each goto statement and
after each assume and inhale statement (for more fine-grained error reporting; in theory, this would not be necessary).
In order to avoid false positives, this pull request also introduces the unreachable statement, which is used to mark pieces of code as not reachable. As a result, no refute false statements are inserted inside of an unreachable branch. To illustrate the problem, consider the following example:
method test(a: Bool)
requires a
{
if (!a)
{
assume false
}
}
Here, the smoke detection plugin would raise an error because false can be proven inside of the body of the if statement. However, since the precondition requires that a is true, the body of the if statement is not reachable. Hence, in order to avoid getting the error, one can add an unreachable statement inside of the if branch:
method test(a: Bool)
requires a
{
if (!a)
{
unreachable
assume false
}
}
The unreachable statement marks the current branch in the control flow as not reachable. This holds until the next join point - in this case, until the end of the body of the if branch. When verifying this example with smoke detection enabled, the plugin reports no errors.
Smoke detection is disabled by default and can be enabled by providing the option --enableSmokeDetection.
Adds the option to automatically detect contradictions in specifications (we call this smoke detection), which lead to the verifier being able to prove anything (even
false
). This is done by insertingrefute false
at various locations in the code; if one of them fails, the specification is unsound. More specifically, theserefute
statements are addedgoto
statement andassume
andinhale
statement (for more fine-grained error reporting; in theory, this would not be necessary).In order to avoid false positives, this pull request also introduces the
unreachable
statement, which is used to mark pieces of code as not reachable. As a result, norefute false
statements are inserted inside of an unreachable branch. To illustrate the problem, consider the following example:Here, the smoke detection plugin would raise an error because
false
can be proven inside of the body of theif
statement. However, since the precondition requires thata
istrue
, the body of theif
statement is not reachable. Hence, in order to avoid getting the error, one can add anunreachable
statement inside of theif
branch:The
unreachable
statement marks the current branch in the control flow as not reachable. This holds until the next join point - in this case, until the end of the body of theif
branch. When verifying this example with smoke detection enabled, the plugin reports no errors.Smoke detection is disabled by default and can be enabled by providing the option
--enableSmokeDetection
.