Tools

  • cargo-verify: a tool for compiling a crate and either verifying main/tests or for fuzzing main/tests. (Use the --backend flag to select which.)

    cargo-verify uses similar command-line flags to the standard cargo-test tool. The --script=PATH flag generates a list of all the commands executed by cargo-verify.

    The source code is here.

  • rvt-patch-llvm: a tool for preprocessing LLVM bitfiles before verification. (Used by cargo-verify.)

    This fixes problems in LLVM bitfiles that are designed to be used for compilation or execution including

    • --features causes all processor feature test functions to return false. This is useful for disabling hand-vectorized code.

      See Using FFI for details.

    • --initializers causes main to call all initializers before it runs. This is useful for programs that use std::env::args() to access the command line arguments.

      See Using ARGV for details.

    • --seahorn fixes various problems that affect the SeaHorn backend.

    The source code is here.

  • rust2calltree: a tool for fixing (demangling) function names in kcachegrind profile files.

    See Profiling Rust for usage.

    The source code is here.

Libraries