Changelog for crux-llvm-0.11.0.0
0.11 -- 2025-11-09
- Sync the version number with
crux-mir-0.11as part of the overall Crux 0.10 release.
0.10 -- 2025-03-24
- Sync the version number with
crux-mir-0.10as part of the overall Crux 0.10 release.
0.9.1 -- 2025-03-21
- Add support for the Bitwuzla SMT solver in the test suite.
- Add
--debugoption for starting the Crucible debugger. - Emit a warning when parsing an LLVM bitcode metadata record that
crux-llvmdoes not support. (Previously,crux-llvmwould throw a fatal error if this occurred, so this change makescrux-llvmmore permissive with respect to unsupported LLVM versions.)
0.9 -- 2024-08-30
- Add support for GHC 9.8
- The type signatures in
Crux.LLVM.Overridesnow use fewer type parameters in theOverrideTemplatesthat they return, in accordance with downstream changes fromcrucible-llvm.
0.8 -- 2024-02-05
- Add support for LLVM bitcode files generated by Apple Clang on macOS.
0.7 -- 2023-06-26
New features
-
When loading bitcode to execute, we now make use of a new feature of
crucible-llvmwhich delays the translation of the LLVM bitcode until functions are actually called. This should speed up startup times and reduce memory usage for verification tasks where a small subset of functions in a bitcode module are actually executed. -
Added support for the
cvc5SMT solver. -
Added support for getting abducts during online goal solving. With the
--get-abducts noption,crux-llvmreturnsnabducts for each goal that the SMT solver found to besat. An abduct is a formula that makes the goalunsat(would help the SMT solver prove the goal). This feature only works with thecvc5SMT solver. -
Support LLVM versions up to 16.
0.6
New features
-
Improved support for translating LLVM debug metadata when the
debug-intrinsicsoption is enabled, including metadata that defines metadata nodes after they are used. -
Add overrides for certain floating-point operations such as
sin,cos,tan, etc. At the solver level,crux-llvmtreats these as uninterpreted functions, socrux-llvmis limited to reasoning about them up to basic, syntactic equivalence checking. -
Certain error messages now print the call stack of functions leading up to the error.
Bug fixes
- Make
--helpand--versionrespect the--no-colorsflag.
Library changes
LLVMConfignow has anindeterminateLoadBehaviorflag to control theMemOptionsoption of the same name. Refer to thecrucible-llvmchangelog for more details.- A
?memOpts :: MemOptionsconstraint has been added toCrux.LLVM.Simulate.checkFun.