如何从LLVM生成代码，然后我想将其作为Z3证明器的输入

Question

我必须从LLVM生成一个中间代码，并且我必须将其作为Z3证明器的输入。这可能吗?

Answer 1

当然可以，但是胆小的人不适合。一种可能的方法见http://rightingcode.org/tutorials/popl20/index.html。