intAbs
1.0.0
このリポジトリは、優先情報を採用することにより、割り込み駆動型プログラムのスレッドモジュラー抽象解釈（エプロンライブラリを使用）に関するものです。
ソースコードは、https：//github.com/markus-kusano/wattsの変更されたバージョンです
現在、すべてのファイルはテストファイルを含めてクリーンアップされていません。
ただし、一部の出力ファイルがアップロードされるため、結果テーブルのサブセットを印刷できます。
@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パスです。 Cmakeを使用して構築されています。 cmakeを使用しているため、これにはLLVMバージョン3.6.0が必要になる可能性があります
cmakelistsファイルの変数Apron_Prefixを変更して、エプロンが設置されている場所になります
LLVMライブラリファイルが標準的な場所にあると仮定します（詳細については、以下）。
mkdir build
cd build
cmake ../
make
ビルドプロセスの結果は、.soファイル、libworklistai.sです。
LLVMがどこに住んでいるかをcmakeに伝える必要がある場合は、オプション-dllvm_dirを追加する必要があります。
cmake -dllvm_dir =/home/chungha/src/share/llvm/cmake ../
llvm_dirに渡されたディレクトリは、LLVM Cmakeファイルがある場所である必要があります（llvm-config.cmakeなど）。
また、-DZ3_INCと-DZ3_LIBをそれぞれZ3のDirectoryとライブラリファイルに設定する必要がある場合があります。
LLVMパスを変更し、src/test/export.shファイルでパスを構築し、LLVM_PREFIX、WorkList_SO、Z3_BINなどのテストプログラムをテストする必要があります。
ASSERTを使用してプログラムの侵略を確認する場合は、この方法で使用する必要があります。
assert(a==1)を使用する代わりにif (a != 1) { assert(0); } 。
ポストドミネーターの関係により、このケースのみをサポートするためにツールを実装する必要があります（アサートはプログラムを到達できないため、ポストドミネーターの関係が失われます）。
ICBMC：これは、ベンチマークを使用して日付15ペーパーからICBMCバイナリファイルをテストしたディレクトリです。
SRC：メインの実装（Worlist-AI、Utils、cmakelists.txt）とテストディレクトリ（テスト）が含まれています
SRC/テスト：テストおよびベンチマークプログラムを実行するためのスクリプトファイルが含まれています。また、結果ファイルは各ディレクトリに含まれています。
