intAbs

讀書我

該存儲庫是關於通過採用優先信息的線程模塊化抽象解釋（使用圍裙庫），用於中斷驅動的程序。

源代碼是https://github.com/markus-kusano/watts的修改版本

目前，所有文件均未清理，包括測試文件。

但是，由於某些輸出文件已上傳，因此可以打印結果表的子集。

引用intabs

 @inproceedings{DBLP:conf/kbse/SungKW17,
  author    = {Chungha Sung and
               Markus Kusano and
               Chao Wang},
  title     = {Modular verification of interrupt-driven software},
  booktitle = {Proceedings of the 32nd {IEEE/ACM} International Conference on Automated
               Software Engineering, {ASE} 2017, Urbana, IL, USA, October 30 - November
               03, 2017},
  pages     = {206--216},
  year      = {2017},
  crossref  = {DBLP:conf/kbse/2017},
  url       = {https://doi.org/10.1109/ASE.2017.8115634},
  doi       = {10.1109/ASE.2017.8115634},
  timestamp = {Fri, 01 Dec 2017 22:44:10 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/kbse/SungKW17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

建築

該程序是LLVM Opt Pass。它是使用cmake構建的。由於我們正在使用CMAKE，因此可能需要LLVM版本3.6.0

修改cmakelists文件變量apron_prefix是安裝圍裙的位置

假設您的LLVM庫文件位於標準位置（以下更多內容），請簡單：

 mkdir build
cd build
cmake ../
make

構建過程的結果是.so文件，libworklistai.so

如果您需要告訴CMAKE LLVM居住在哪裡，則需要添加選項-dllvm_dir，例如

cmake -dllvm_dir =/home/chungha/src/share/llvm/cmake ../

傳遞給llvm_dir的目錄應為LLVM CMAKE文件所在的位置（例如，llvm-config.cmake）。

您可能還需要將-dz3_inc和-dz3_lib設置為include目錄，並分別為z3設置庫文件。

測試路徑

您需要修改LLVM路徑並在src/test/export.sh文件中構建路徑，以便測試程序，例如llvm_prefix，worklist_so，z3_bin。

主張用法

如果您想使用斷言檢查程序的不變性，則必須以這種方式使用。

if (a != 1) { assert(0); }而不是使用assert(a==1) ，而是必須寫下。 if (a != 1) { assert(0); } 。

由於後統治者的關係，我需要實施我的工具來僅支持這種情況（斷言使該程序無法到達，因此丟失了一些後統治者關係）。

目錄說明

• ICBMC：這是我從date15紙上測試ICBMC二進製文件的目錄。

• SRC：它包含主要實現（Worlist-ai，Utils，cmakelists.txt）和一個測試目錄（test）

• SRC/TEST：它包含用於運行測試和基準程序的腳本文件。另外，結果文件包含在每個目錄中。