@hackage crux-llvm0.9.1

This tool (and corresponding C library) are intended for verifying C programs using verification specifications embedded in the input source files (i.e. it allows for writing Crucible specifications by using C as the specification language).

This tool provides:

• a Haskell library with the core functionality,

• a crux-llvm executable used to run the verification when given one or more C or C++ source files

• a set of supplemental C source files, include files, and LLVM runtime library bitcode files to use for building the input C files into verifiable LLVM BC files.

• a crux-llvm-svcomp executable that is designed to run verification of challenge inputs for the SV-COMP competition, generating results tailored to the format that SV-COMP expects.