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
