intAbs

readme

이 저장소는 우선 순위 정보를 채택하여 인터럽트 중심 프로그램에 대한 스레드 모듈 식 추상 해석 (앞치마 라이브러리 사용)에 관한 것입니다.

소스 코드는 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 Pass입니다. CMAKE를 사용하여 제작되었습니다. CMAKE를 사용하고 있으므로 LLVM 버전 3.6.0이 필요할 수 있습니다.

cmakelists 파일 변수 Apron_prefix를 앞치마가 설치된 위치로 수정하십시오.

LLVM 라이브러리 파일이 표준 위치에 있다고 가정하면 (아래에 자세히 설명).

 mkdir build
cd build
cmake ../
make

빌드 프로세스의 결과는 .so 파일, libworklistai.so입니다.

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의 라이브러리 파일로 설정해야 할 수도 있습니다.

테스트 경로

LLVM PATH를 수정하고 src/test/export.sh 파일에서 LLVM_PREFIX, WorkList_SO, Z3_BIN과 같은 테스트 프로그램에 구축해야합니다.

사용법을 주장합니다

Assert를 사용하여 프로그램의 불변을 확인하려면 이런 식으로 사용해야합니다.

assert(a==1) 사용하는 대신 if (a != 1) { assert(0); } .

Post Dominator 관계로 인해이 사례 만 지원하기 위해 도구를 구현해야합니다 (Assert는 프로그램을 도달 할 수 없도록하여 일부 지배자 관계가 손실됩니다).

디렉토리 설명

• ICBMC : 이것은 벤치 마크와 함께 Date15 용지에서 ICBMC 이진 파일을 테스트 한 디렉토리입니다.

• SRC : 주요 구현 (Worlist-Ai, Utils, Cmakelists.txt) 및 테스트 디렉토리 (테스트)가 포함되어 있습니다.

• SRC/TEST : 테스트 및 벤치 마크 프로그램을 실행하기위한 스크립트 파일이 포함되어 있습니다. 또한 결과 파일은 각 디렉토리에 포함되어 있습니다.