文件名称：alive2:LLVM优化的自动验证
文件大小：741KB
文件格式：ZIP
更新时间：2024-08-13 00:30:35
llvm verification symbolic-execution model-checking smt
活着2 Alive2 包含多个用于分析和验证 LLVM 代码和转换的库和工具。 Alive2 包括以下库： Alive2 IR 符号执行器 LLVM -> Alive2 IR 转换器 细化检查（又名优化验证器） SMT抽象层 包含的工具： 现场替换 用于 clang 和 LLVM opt翻译验证插件 独立翻译验证工具： alive-tv （） 警告 Alive2 不支持过程间转换。 如果使用此类传递运行，Alive2 可能会崩溃或产生虚假的反例。 先决条件 要构建 Alive2，您需要最新版本的： 制作 海湾合作委员会/铿锵 re2c Z3 LLVM（可选） 建造 mkdir build cd build cmake -GNinja -DCMAKE_BUILD_TYPE=Release .. ninja 如果 CMake 找不到 Z3 包含目录（或找到错误的目录）， -D