Static analysis

NIKOS

NIKOS is a static analyzer for C and C++ based on abstract interpretation. It is a fork of IKOS, developed by the NASA Ames Research Center, with additional checkers.

The licence is NOSA 1.3.

Source Code

                # Analyze a C file

                ikos example.c

                # Render the results

                ikos-report output.db

Analysis and reports

The driver compiles C or C++ to LLVM bitcode and runs the analysis pipeline.

Results are stored in an SQLite database.

Checkers

NIKOS adds taint, concurrency, use-after-free and use-after-move checkers to the IKOS set.

Reports

ikos-report renders text, JSON, SARIF, JUnit and CSV. ikos-view renders HTML.

Limits

The concurrency checker uses intraprocedural lockset analysis and reports warnings. See the precise semantics and limitations of each checker.