Documentation

Fields

• colorOptions :: ColorOptions
   
• printFailures :: Bool

  Print errors regarding failed verification goals

• printSymbolicVars :: Bool

  Print values assigned to symbolic variables when printing failed verification goals

• simVerbose :: Int

  Level of verbosity for the symbolic simulation

• quietMode :: Bool

  If true, produce minimal output

Fields

• inputFiles :: [FilePath]

  the files to analyze

• outDir :: FilePath

  Write results in this location. If empty, then do not produce any analysis results.

• bldDir :: FilePath

  Directory for writing files generated from the inputFiles set (e.g. building C sources into LLVM bitcode files) for analysis.

• checkPathSat :: Bool

  Should we enable path satisfiability checking?

• profileCrucibleFunctions :: Bool
   
• profileSolver :: Bool
   
• branchCoverage :: Bool
   
• pathStrategy :: PathStrategy
   
• globalTimeout :: Maybe NominalDiffTime
   
• goalTimeout :: Maybe DiffTime
   
• profileOutputInterval :: NominalDiffTime
   
• loopBound :: Maybe Word64

  Should we artifically bound the number of loop iterations

• recursionBound :: Maybe Word64

  Should we artifically bound the number of recursive calls to functions?

• makeCexes :: Bool

  Should we construct counter-example executables

• unsatCores :: Bool

  Should we attempt to compute unsatisfiable cores for successful proofs?

• getNAbducts :: Maybe Word64

  How many abducts should we get from the solver for sat results? Only works with cvc5

• solver :: String

  Solver to use to discharge proof obligations

• pathSatSolver :: Maybe String

  A separate solver to use for path satisfiability checking if that feature is enabled and if the path satisfiability checking solver should differ from the solver used to discharge proof obligations (default: use the proof obligation solver)

• forceOfflineGoalSolving :: Bool

  Force goals to be verified using an offline solver instance, even if it would have been possible to use the same solver in online mode

• pathSatSolverOutput :: Maybe FilePath

  The file to store the interaction session between the path satisfiability checker and the solver (if path satisfiability checking is enabled)

• onlineSolverOutput :: Maybe FilePath

  The file to store the interaction with the online goal solver (if solving is being performed online)

• offlineSolverOutput :: Maybe FilePath

  A template to use for files to store interactions with offline goal solvers (if solving is being performed offline).

• yicesMCSat :: Bool

  Should the MC-SAT Yices solver be enabled (disables unsat cores; default: no)

• floatMode :: String

  Tells the solver which representation to use for floating point values.

• proofGoalsFailFast :: Bool

  If true, stop attempting to prove goals as soon as one is disproved

• skipReport :: Bool

  Don't produce the HTML reports that describe the verification task

• skipSuccessReports :: Bool

  Skip reporting on successful proof obligations

• skipIncompleteReports :: Bool

  Skip reporting on goals that arise from resource exhaustion

• hashConsing :: Bool

  Turn on hash-consing in the symbolic expression backend

• onlineProblemFeatures :: ProblemFeatures

  Problem Features to force in online solvers

• outputOptions :: OutputOptions

  Output options grouped together for easy transfer to the logger