Crux v0.6
New features
-
[LLVM] Improved support for translating LLVM debug metadata when the
debug-intrinsics
option is enabled, including metadata that defines metadata nodes after they are used. -
[LLVM] Add overrides for certain floating-point operations such as
sin
,cos
,tan
, etc. At the solver level,crux-llvm
treats these as uninterpreted functions, socrux-llvm
is limited to reasoning about them up to basic, syntactic equivalence checking. -
[LLVM] Certain error messages now print the call stack of functions leading up to the error.
Bug fixes
-
[LLVM] Make
--help
and--version
respect the--no-colors
flag. -
[MIR]
Any
-typed local variables are no longer initialized to a default value, which prevents spurious assertion failures if these variables become involved in symbolic branches in certain cases.