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
