Static analyzer for C/C++ based on the theory of Abstract Interpretation.
March 2024
This is a maintenance release that addresses bugs related to Python dependencies, the order of passes in the LLVM frontend, and missing imports.
4 issues were closed as part of IKOS 3.3.
The net balance including all files (e.g., code, docs) is that IKOS 3.3 is 4 lines bigger than the previous version.
We had submissions from 1 new author who had never submitted patches to IKOS before.
Full Changelog: https://github.com/NASA-SW-VnV/ikos/compare/v3.2...v3.3
December 2023
This is a maintenance release that addresses bugs related to Python packaging, LLVM 14, IPv6 handling and multi OS support. Other changes focus on the documentation, the software engineering process and leveraging features offered by Github.
There are two notable changes:
-section in call to llvm-objdump by @lojikil (#199).llvm-objdump in LLVM 14 (#203).23 issues were closed as part of IKOS 3.2.
The net balance including all files (e.g., code, docs) is that IKOS 3.2 is 437 lines smaller than the previous version.
We had submissions from 4 new authors who had never submitted patches to IKOS before.
Full Changelog: https://github.com/NASA-SW-VnV/ikos/compare/v3.1...v3.2
October 2016
September 2016
August 2016
branching-opt to optimize all Control Flow Graphs of the AR, before the analysis. The pass detects unreachable paths in the graphs and removes them.June 2016
calloc() correctly. In IKOS 1.0.0, the function call was just ignored.--display-invariants and --display-checks.column to the result tables in the output database, containing the column number in the source code.stmt_uid to the result tables in the output database, containing the UID of the checked statement.The LLVM frontend now supports both LLVM 3.7 and 3.8.
ARBOS now gives the column number in addition to the line number in AR_Source_Location.
May 2016
In this release we upgraded our LLVM frontend from version 2.9 to 3.7.
To have a C/C++ program fully represented in AR, there are several code transformation we had to handle with the frontend's intermediate representation. When using the LLVM framework as the frontend, we transform the following LLVM instructions so they can be expressed in AR:
phi instructiongetelementptr instructioninsertvalue and extractvalue instructionsi/fcmp and select instructionsbr
constantexpr and its subclassesmemset, memcpy, memmove, vastart, vaend, va_arg, and vacopy.In the previous release v0.0.1 we handled all transformation in ARBOS. The previous tool chain architecture defined another intermediate representation, called AIR, that served as a direct translation from the LLVM bitcode to an S-expression format that was fed into ARBOS. ARBOS then parsed and transformed AIR to AR in memory.
This release removes AIR entirely. All transformation are done in LLVMAR, while ABROS only parses the AR and makes it available in memory for ARBOS analysis plugins to traverse and perform analysis on it.
AR_Global_Variable may contain an initializer represented as AR_Code. In the previous release we dedicated an initializer function for each global variable. These initializer functions were individually invoked in main(). In this release, analyzers need to dive into the initializer of an AR_Global_Variable to analyze the initializer code.AR_Type.varags intrinsic calls in the AR. This was not supported in the previous release.December 2022
ikos-scan without an HTTP server, outputting JSON.isAlive.December 2019
August 2019
-I, -D, -W, -w and -m flags to clang.ll