ikos
Public release 3.4
基於抽象解釋理論，IKO（開放靜態分析儀的推理內核）是C/C ++的靜態分析儀。
IKO最初是C ++庫，旨在基於抽象的解釋來促進聲音靜態分析儀的開發。將靜態分析儀用於應用或應用程序家族的靜態分析儀對於實現精度和可擴展性至關重要。開發這種分析儀非常艱鉅，需要在抽象解釋方面具有重要的專業知識。
IKO提供了最先進的抽象解釋數據結構和算法的通用實現，例如控制流圖，fixpoint迭代器，數值抽象域等。 IKOS與特定的編程語言無關。
IKO還基於LLVM提供了C ++靜態分析儀。它實施了可擴展的分析，用於檢測和證明C和C ++程序中缺乏運行時錯誤。
IKO已根據NASA開源協議1.3版發布，請參閱LICEND.PDF
請參閱版本。
請參閱故障排除
要在Linux或MacOS上安裝IKO，我們建議使用自製。
首先，按照以下說明來安裝自製。
然後，只需運行：
$ brew install nasa-sw-vnv/core/ikos
對於Windows，請考慮將Windows子系統用於Linux。
假設我們要在文件中分析以下C程序，稱為loop.c ：
1 : #include <stdio.h>
2 : int a [ 10 ];
3 : int main ( int argc , char * argv []) {
4 : size_t i = 0 ;
5 : for (; i < 10 ; i ++ ) {
6 : a [ i ] = i ;
7 : }
8 : a [ i ] = i ;
9 : printf ( "%i" , a [ i ]);
10 : }要使用IKO分析此程序，只需運行：
$ ikos loop.c
您將看到以下輸出。 IKO報告了在第8和9行中的兩次緩衝區溢出。
[*] Compiling loop.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'
# Time stats:
clang : 0.037 sec
ikos-analyzer: 0.023 sec
ikos-pp : 0.007 sec
# Summary:
Total number of checks : 7
Total number of unreachable checks : 0
Total number of safe checks : 5
Total number of definite unsafe checks: 2
Total number of warnings : 0
The program is definitely UNSAFE
# Results
loop.c: In function 'main':
loop.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
a[i] = i;
^
loop.c: In function 'main':
loop.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
printf("%i", a[i]);
^
ikos命令將源文件（ .c ， .cpp ）或LLVM BitCode文件（ .bc ）作為輸入進行分析以查找運行時錯誤（也稱為未定義的行為），在當前工作目錄中創建結果數據庫output.db並打印報告。
在報告中，每行具有以下狀態之一：
默認情況下，IKO直接在您的終端顯示警告和錯誤，就像編譯器一樣。
如果分析報告太大，則應使用：
ikos-report output.db檢查終端中的報告ikos-view output.db在Web界面中檢查報告更多信息：
以下是從源構建IKO的說明。這僅適用於想要將IKO打包用於操作系統或嘗試使用代碼庫的高級用戶。否則，請按照上述說明進行操作。
要構建和運行分析儀，您將需要以下依賴項：
可以使用軟件包管理器安裝其中大多數。
注意：如果您從源構建LLVM，則需要啟用運行時類型信息（RTTI）。
現在，您擁有對系統的所有依賴關係，可以構建和安裝IKO。
當您打開IKOS分發時，您將看到以下目錄結構：
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
IKO使用CMAKE構建系統。您需要指定一個安裝目錄，該目錄將包含安裝後所有二進製文件，庫和標頭。如果您不指定此目錄，則CMAKE將install在分佈的根目錄中的所有內容。在以下步驟中，我們將在/path/to/ikos-install-directory安裝IKOS。
這是構建和安裝ikos的步驟：
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
然後，在您的路徑中添加ikos（請考慮在.bashrc中添加它）：
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
要構建和運行測試，只需鍵入：
$ make check
參見貢獻者
Sung Kook Kim，Arnaud J. Venet，Aditya V. Thakur。確定性並行固定點計算。路易斯安那州新奧爾良（PDF）的編程語言原理（POPL 2020） 。
Guillaume Brat，Jorge Navas，Nija Shi和Arnaud Venet。 IKO：基於抽象解釋的靜態分析框架。在法國格勒諾布爾（PDF）的國際軟件工程與正式方法會議論文集（SEFM 2014） 。
Arnaud Venet。量規域：線性不平等不變的可擴展分析。在計算機輔助驗證論文集（CAV 2012） ，美國加利福尼亞州伯克利，2012年。計算機科學的講義，第139-154頁，第7358卷，Springer 2012（PDF）。
請參閱doc/coding_standards.md
請參閱doc/overview.md
