kframework - 编译器：没有为排序 Optional[KVar] 定义新生成器

Question

我正在使用 LLVM 后端进行编译。它可以使用 Java 后端进行编译，但是 LLVM 后端会抛出以下错误： Compiler: No fresh generator defined for sort Optional[KVar]

该错误突出!M显示<abs> ... .Map => (!M |-> (T1 -> T2)) ... </abs>

Answer 1

这是 K 的替换实现中的一个错误，它导致排序 KVar 的新常量仅在 java 后端可用。您可以在此处跟踪问题：https ://github.com/kframework/k/issues/1186

我们将尽快解决该问题，因为它应该很简单。