crux-llvm-0.10: CHANGELOG.md

# 0.10 -- 2025-03-24

* Sync the version number with `crux-mir-0.10` as 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 `--debug` option for starting the Crucible debugger.
* Emit a warning when parsing an LLVM bitcode metadata record that `crux-llvm`
  does not support. (Previously, `crux-llvm` would throw a fatal error if this
  occurred, so this change makes `crux-llvm` more permissive with respect to
  unsupported LLVM versions.)

# 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`.