sys
1.0.0
如果您有兴趣，请在此处查看（非常非常）新的重新成真！
如果您想在本地安装系统：
--shared选项。请参阅该文件中的build()和package()函数，以此作为如何在克隆之后安装boolector的示例。在Arch Linux上，您只需从AUR安装boolector-git即可。另外，您可以使用Ralf-Philipp Weinmann的Dockerfile。
一旦安装了所有依赖项，您就应该能够构建该工具：
stack build
构建工具后，您可以通过以下方式构建和运行我们的测试：
stack test
这将运行我们的测试套件的完整版本，以及我们在论文中列出的每个错误的回归测试。该套件在笔记本电脑上花费了两分钟以上，带有64GB的RAM和8个线程。所有测试都具有一个例外---一个错误，我们在追踪的错误都应该通过。如果其他任何事情失败，请尝试重新运行测试；求解器可能已经超时了（这没有在我们的机器上发生，但是由于我们无法给您登录名，因此它可能会在您的机器上发生）。
如果您只想复制论文结果，而其他任何内容都没有运行：
stack test --ta '-p End-to-end'
构建工具后，您现在可以使用它来查找错误！
stack exec sys
该工具采用几个选项：
-d DIR --libdir=DIR directory (or file) to analyze
-e EXTN --extn=EXTN file extension
-c CHECK --check=CHECK checker to run
-d选项用于指定目录（包含LLVM文件）或单个LLVM文件。-e选项用于指定要检查的文件的扩展。当使用不同的优化级别构建项目时，这很有用（例如，使用-O0和.ll-O0_p .ll-O0 O0_P用于生产的.LL-O0）。ll匹配所有*.ll文件O0匹配所有*.ll-O0和*.ll-O0_p文件O1匹配所有*.ll-O1和*.ll-O1_p文件O2匹配所有*.ll-O2和*.ll-O2_p文件O3匹配所有*.ll-O3和*.ll-O3_p文件Og匹配所有*.ll-Og和*.ll-Og_p文件Os匹配所有*.ll-Os和*.ll-Os_p文件Oz匹配所有*.ll-Oz和*.ll-Os_z文件prod匹配所有*_p文件any匹配所有文件-c选项用于指定要运行的检查器，其中之一是：uninit ：非初始化的内存检查器heapoob ：Malloc OOB检查器concroob ：负索引OOB检查器userinput ：用户输入检查器要找到我们工具在Firefox的Prio库中发现的非初始化的内存访问错误：
$ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p
该工具标记两个错误。让我们首先看一下：
Stack uninit bug
Name "serial_read_mp_array_73"
in
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]
如果检查serial_read_mp_array（）函数，则buggy块路径为%4 （第一个块）至%71 ，我们使用[ %73 ]。
除了Arch Linux，我们还没有在Arch Linux上测试（可能不会测试）系统。我们很乐意整合补丁，以增加对其他OS的支持并构建系统！
├── app -- Executable used to run the checkers
├── src
│ ├── Checkers -- Static and symbolic checkers
│ ├── Control -- Logging helpers
│ ├── LLVMAST -- LLVM AST interface
│ ├── InternalIR -- Internal IR used to represent paths for both static and symex
│ ├── Static -- Static checker DSL
│ └── Symex -- Symbolic DSL and execution engine
├── community -- Community files
└── test -- Tests
