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.