# 0.9 -- 2024-08-30
* Add support for GHC 9.8
* The type signatures in `Crux.LLVM.Overrides` now use fewer type parameters in the `OverrideTemplates` that they return, in accordance with downstream changes from `crucible-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-llvm` which 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 `cvc5` SMT solver.
* Added support for getting abducts during online goal solving. With
the `--get-abducts n` option, `crux-llvm` returns `n` abducts for
each goal that the SMT solver found to be `sat`. An abduct is a formula
that makes the goal `unsat` (would help the SMT solver prove the goal).
This feature only works with the `cvc5` SMT solver.
* Support LLVM versions up to 16.
# 0.6
## New features
* Improved support for translating LLVM debug metadata when the
`debug-intrinsics` option 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-llvm` treats these as uninterpreted
functions, so `crux-llvm` is 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 `--help` and `--version` respect the `--no-colors` flag.
## Library changes
* `LLVMConfig` now has an `indeterminateLoadBehavior` flag to control the
`MemOptions` option of the same name. Refer to the `crucible-llvm` changelog
for more details.
* A `?memOpts :: MemOptions` constraint has been added to
`Crux.LLVM.Simulate.checkFun`.