https://github.com/NASA-SW-VnV/ikos Skip to content Sign up * Product + Features + Mobile + Actions + Codespaces + Packages + Security + Code review + Issues + Integrations + GitHub Sponsors + Customer stories * Team * Enterprise * Explore + Explore GitHub + Learn and contribute + Topics + Collections + Trending + Learning Lab + Open source guides + Connect with others + The ReadME Project + Events + Community forum + GitHub Education + GitHub Stars program * Marketplace * Pricing + Plans + Compare plans + Contact Sales + Education [ ] * # In this repository All GitHub | Jump to | * No suggested jump to results * # In this repository All GitHub | Jump to | * # In this organization All GitHub | Jump to | * # In this repository All GitHub | Jump to | Sign in Sign up {{ message }} NASA-SW-VnV / ikos Public * Notifications * Fork 111 * Star 1.5k Static analyzer for C/C++ based on the theory of Abstract Interpretation. View license 1.5k stars 111 forks Star Notifications * Code * Issues 42 * Pull requests 2 * Actions * Projects 0 * Wiki * Security * Insights More * Code * Issues * Pull requests * Actions * Projects * Wiki * Security * Insights This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. master Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags 1 branch 5 tags Code Latest commit @guillaume66 @arthaud guillaume66 and arthaud use quoteattr to output messages to prevent problems with quotes insi... ... 71325df Jan 27, 2022 use quoteattr to output messages to prevent problems with quotes insi... ...de the message 71325df Git stats * 423 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time analyzer ar cmake core doc frontend/llvm script test/install .clang-format .clang-tidy .gitignore .travis.yml CMakeLists.txt CONTRIBUTORS.md LICENSE.pdf LICENSE.txt README.md RELEASE_NOTES.md TROUBLESHOOTING.md View code [ ] IKOS Introduction License Contact Release notes Troubleshooting Installation Dependencies Build and Install Tests How to run IKOS Contributors Publications Coding Standards Overview of the source code README.md IKOS Build Status License Release IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation. Introduction IKOS started as a C++ library designed to facilitate the development of sound static analyzers based on Abstract Interpretation. Specialization of a static analyzer for an application or family of applications is critical for achieving both precision and scalability. Developing such an analyzer is arduous and requires significant expertise in Abstract Interpretation. IKOS provides a generic and efficient implementation of state-of-the-art Abstract Interpretation data structures and algorithms, such as control-flow graphs, fixpoint iterators, numerical abstract domains, etc. IKOS is independent of a particular programming language. IKOS also provides a C and C++ static analyzer based on LLVM. It implements scalable analyses for detecting and proving the absence of runtime errors in C and C++ programs. License IKOS has been released under the NASA Open Source Agreement version 1.3, see LICENSE.pdf Contact ikos@lists.nasa.gov Release notes See RELEASE_NOTES.md Troubleshooting See TROUBLESHOOTING.md Installation Dependencies To build and run the analyzer, you will need the following dependencies: * A C++ compiler that supports C++14 (gcc >= 4.9.2 or clang >= 3.4) * CMake >= 3.4.3 * GMP >= 4.3.1 * Boost >= 1.55 * Python 2 >= 2.7.3 or Python 3 >= 3.3 * SQLite >= 3.6.20 * TBB >= 2 * LLVM and Clang 9.0.x * (Optional) APRON >= 0.9.10 * (Optional) Pygments Most of them can be installed using your package manager. Installation instructions for Arch Linux, CentOS, Debian, Fedora, Mac OS X, Red Hat, Ubuntu and Windows are available in the doc/install directory. These instructions assume you have sudo or root access. If you don't, please follow the instructions in doc/install/ROOTLESS.md. Note: If you build LLVM from source, you need to enable run-time type information (RTTI). Once you have all the required dependencies, move to the next section. Build and Install Now that you have all the dependencies on your system, you can build and install IKOS. As you open the IKOS distribution, you shall see the following directory structure: . +-- CMakeLists.txt +-- LICENSE.pdf +-- README.md +-- RELEASE_NOTES.md +-- TROUBLESHOOTING.md +-- analyzer +-- ar +-- cmake +-- core +-- doc +-- frontend +-- script +-- test IKOS uses the CMake build system. You will need to specify an installation directory that will contain all the binaries, libraries and headers after installation. If you do not specify this directory, CMake will install everything under install in the root directory of the distribution. In the following steps, we will install IKOS under /path/to/ikos-install-directory. Here are the steps to build and install IKOS: $ mkdir build $ cd build $ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory .. $ make $ make install Then, add IKOS in your PATH (consider adding this in your .bashrc): $ PATH="/path/to/ikos-install-directory/bin:$PATH" Tests To build and run the tests, simply type: $ make check How to run IKOS Suppose we want to analyze the following C program in a file, called loop.c: 1: #include 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: } To analyze this program with IKOS, simply run: $ ikos loop.c You shall see the following output. IKOS reports two occurrences of buffer overflow at line 8 and 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]); ^ The ikos command takes a source file (.c, .cpp) or a LLVM bitcode file (.bc) as input, analyzes it to find runtime errors (also called undefined behaviors), creates a result database output.db in the current working directory and prints a report. In the report, each line has one of the following status: * safe: the statement is proven safe; * error: the statement always results into an error (or is unreachable); * unreachable: the statement is never executed; * warning may mean three things: 1. the statement results into an error for some executions, or 2. the static analyzer did not have enough information to conclude (check dependent on an external input, for instance), or 3. the static analyzer was not powerful enough to prove the absence of errors; By default, ikos shows warnings and errors directly in your terminal, like a compiler would do. If the analysis report is too big, you shall use: * ikos-report output.db to examine the report in your terminal * ikos-view output.db to examine the report in a web interface Further information: * Analyze a whole project with ikos-scan * Examine a report with ikos-view * Analysis Options + Checks + Numerical abstract domains + Entry points + Multi-threading + Optimization level + Inter-procedural vs Intra-procedural + Fixpoint engine parameters + Partitioning + Hardware addresses + Other analysis options * Report Options + Format + File + Status Filter + Analysis Filter + Verbosity + Other report options * APRON Support * Analysis Assumptions * Analyze an embedded software requiring a cross-compiler * Model library functions to reduce warnings Contributors See CONTRIBUTORS.md Publications * Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur. Deterministic Parallel Fixpoint Computation. In Principles of Programming Languages (POPL 2020), New Orleans, Louisiana (PDF). * Guillaume Brat, Jorge Navas, Nija Shi and Arnaud Venet. IKOS: a Framework for Static Analysis based on Abstract Interpretation. In Proceedings of the International Conference on Software Engineering and Formal Methods (SEFM 2014), Grenoble, France (PDF ). * Arnaud Venet. The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. In Proceedings of Computer Aided Verification (CAV 2012), Berkeley, California, USA 2012. Lecture Notes in Computer Science, pages 139-154, volume 7358, Springer 2012 (PDF). Coding Standards See doc/CODING_STANDARDS.md Overview of the source code See doc/OVERVIEW.md About Static analyzer for C/C++ based on the theory of Abstract Interpretation. Topics static-analysis program-analysis software-verification abstract-interpretation Resources Readme License View license Stars 1.5k stars Watchers 51 watching Forks 111 forks Releases 5 public release version 3.0 Latest Dec 12, 2019 + 4 releases Packages 0 No packages published Contributors 6 * * * * * * Languages * C++ 72.1% * LLVM 16.1% * Python 4.5% * CMake 2.1% * C 1.9% * Shell 1.6% * Other 1.7% * (c) 2022 GitHub, Inc. * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time. You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.