Documentation

Fields

• verbosity :: Verbosity

  How much output the verifier should produce.

• assumePartialSideConds :: Bool

  If True, the verifier will determine the conditions under which a Copilot specification's partial operations are well defined and add these side conditions as assumptions. As a result, even if the generated C code performs a partial operation, the verification will succeed if this partial operation coincides with a corresponding operation on the Copilot side.

  If False, the verifier will not assume any side conditions related to partial operations in the Copilot specification. As a result, any use of a partial operation in the generated C code will cause verification to fail unless the user adds their own assumptions.

• logSmtInteractions :: Bool

  If True, create log files corresponding to the SMT solver interactions used to discharge each proof goal. The file will be named step-number-solver.smt2, where:

  • step will be either initial-step or transition-step, depending on which step of the proof the goal corresponds to.
  • number will be the number of the goal, starting at 0 and counting up. Note that each step of the proof has its own goal numbers. This means that there can be both an initial-step-0-solver.smt2 and a transition-step-0-solver.smt2, and similarly for other numbers.
  • solver is the name of the SMT solver used to discharge the proof goal. Currently, this will always be z3, although we might make this configurable in the future.
• smtSolver :: Solver

  Which SMT solver to use when solving proof goals.

• smtFloatMode :: FloatMode

  How the verifier should interpret floating-point operations when translating them to SMT.

  By default, the verifier will treat all floating-point operations as uninterpreted functions (FloatUninterpreted). This allows the verifier to perform some limited reasoning about floating-point operations that SMT solvers do not have built-in operations for (sin, cos, tan, etc.), but at the expense of not being able to verify C code in which the compiler optimizes floating-point expressions. One can also opt into an alternative mode where floating-point values are treated as IEEE-754 floats (FloatIEEE), but this comes with the drawback that the verifier will not be able to perform any reasoning about sin, cos, tan, etc.