Announcing the Release of Crux 0.6

We are pleased to announce the release of Crux 0.6. Crux is a tool for verifying programs containing inline specifications. Crux works with both C/C++ code (via Crux-LLVM) and Rust code (via Crux-MIR).

This release brings a variety of improvements, including:

  • Crux-LLVM now has improved support for LLVM debug metadata when the debug-intrinsics option is enabled, including metadata that defines metadata nodes after they are used.
  • Crux-LLVM now has very limited support for certain floating-point operations, such as sin, cos, tan, etc.
  • Certain error messages in Crux-LLVM now print the call stack of functions leading up to the error.

Binary distributions and source distributions can be downloaded from here. This download page also contains a more detailed changelog. We also provide Docker images for Crux-LLVM and Crux-MIR:

     docker pull ghcr.io/galoisinc/crux-llvm:0.6
     docker pull ghcr.io/galoisinc/crux-mir:0.6

If you encounter any issues with Crux, feel free to file an issue here.