Closed moralismercatus closed 9 years ago
xmm/sse registers aren't translated by the Bitcode translator at this point.
For now, compile target binaries with flags that disable the use of those registers.
This has been resolved for some time. The helper functions are now exported to Klee and the translator works with them (It was a problem of signatures not matching).
If you attempt to test echo using include-all-but-necessary-functions, for filtering options, llvm-link will fail due to problems relating to xmm registers.
It seems that the helper functions for xmm registers are missing.
Once libc and ld were excluded, the testing proceeded.