带stp的Klee和其他卫星解算器的Klee

Question

Klee使用STP作为约束求解器，但理论上可以改变其求解器。STP不允许浮点操作。如果我们决定用另一个约束求解器代替STP，比如z3，klee是否能够生成浮点约束？

流程是:C代码-> llvm bitcode -> klee -> stp子句-> klee ->输出

如果klee得到浮点指令，它能解释它们吗？它是在smt语言中生成fp约束，stp不能处理这些约束，还是根本不生成fp约束？

如能提供你的答复，我将不胜感激。

Answer 1

这个链接包含有浮点支持的克利叉子。不过，我不知道它有多成熟。