Skip to main content

errors.VerificationError

A postcondition, or the absence of runtime errors, could not be proved.

Usage

Source

errors.VerificationError(report)

Import it from sverify.errors. The message’s first line counts what is missing; then one line per finding: each needed precondition, each unproved postcondition with what the checker established about it, and each possible runtime error with its hint. report holds the rest.

Attributes

report
The Report of the failed proof.