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：它包含用于运行测试和基准程序的脚本文件。另外，结果文件包含在每个目录中。