alive2

Alive2 包括多个库和工具,用于分析和验证 LLVM 代码和转换。Alive2 包括以下库:

• Alive2 IR
• 符号执行器
• LLVM → Alive2 IR 转换器
• 精化检查(又称优化验证器)
• SMT 抽象层 包含的工具:
• Alive 替换插件
• 适用于 clang 和 LLVM opt 的翻译验证插件
• 独立的翻译验证工具: alive-tv (在线)
• 具有翻译验证的 clang 替换插件(alivecc 和 alive++)
• 一个 LLVM IR 解释器,精确到无界限错误(alive-exec)

警告------- Alive2 不支持过程间转换。如果使用此类步骤运行 Alive2,可能会产生虚假的反例。

前提条件

Alive2 的 opt 和 clang 翻译验证需要使用已开启 RTTI 和异常的 LLVM 版本进行构建。Alive2 的最新版本始终是针对最新版本进行构建的。