`[错误]内部：UnsupportedOperationException类型的未捕获异常（UnsupportedOperationException：null）`答案

【问题标题】：`[Error] Internal: Uncaught exception thrown of type UnsupportedOperationException (UnsupportedOperationException: null)``[错误]内部：UnsupportedOperationException类型的未捕获异常（UnsupportedOperationException：null）`
【发布时间】：2020-04-01 20:47:56
【问题描述】：

我正在尝试使用之前使用 Java 后端编译的 LLVM 后端编译文件，并收到以下警告：

ld: warning: could not create compact unwind for _step: stack subq instruction is too different from dwarf stack size

然后在运行时出现以下错误：

java.lang.UnsupportedOperationException
    at org.kframework.backend.llvm.LLVMRewriter$1.search(LLVMRewriter.java:149)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:54)
    at org.kframework.krun.KRun.run(KRun.java:85)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:95)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
    at org.kframework.main.Main.runApplication(Main.java:118)
    at org.kframework.main.Main.runApplication(Main.java:108)
    at org.kframework.main.Main.main(Main.java:56)
[Error] Internal: Uncaught exception thrown of type
UnsupportedOperationException (UnsupportedOperationException: null)

这些是什么意思？

【问题讨论】：

标签： kframework

【解决方案1】：

llvm 后端（尚）不支持krun --search。当前支持搜索的唯一后端是 Java 和 Haskell 后端。

至于链接器警告，我不完全确定它的含义，但它与调试数据有关，因此您可以忽略它，它不会影响可执行文件的行为。

【讨论】：

我一直在使用 K 通过 Z3 进行符号执行。我探索所有可能的过渡并修剪那些不能满足的过渡。这是否意味着 llvm 后端无法做到这一点？我的理解是 Java 后端将被弃用。会有替代品吗？
haskell 后端本身支持符号执行，并且也进行分支修剪。 LLVM 后端旨在快速执行