Static analyzer for C/C++ based on the theory of Abstract Interpretation.

Overview

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

[email protected]

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 <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: }

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:

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

Comments
  • Questions about the algorithm of the analysis

    Questions about the algorithm of the analysis

    Code: #include <stdio.h>

    int a = 100; int size = 16; char array1[16];

    int fun(int x) { int y=0; if (x < size) { y = array1[x]; } return y; }

    int main() { fun(a); return 0; }

    I tried to stop the liveness analysis by ikos --no-liveness test.c But still got the warning unreachable: code is dead y = array1[x]; ^ I want to see if ikos can give the buffer overflow warning if I can stop the liveness analysis.

    Please tell me how I can get the buffer overflow warning from this c code from ikos.

    C-question 
    opened by arnab-security 51
  • ikos-analyzer stuck and/or running out of memory

    ikos-analyzer stuck and/or running out of memory

    When analyzing the suricata code base (~300k lines of C), the ikos-analyzer uses excessive memory and appears to get stuck in some kind of loop.

    Analyze src/suricata? [Y/n]
    [*] Running ikos src/suricata.bc -o src/suricata.db
    [*] Running ikos preprocessor
    [*] Running ikos analyzer
    [*] Translating LLVM bitcode to AR
    [*] Running liveness analysis
    [*] Running fixpoint profile analysis
    [*] Running interprocedural value analysis
    [*] Analyzing entry point: main
    

    I killed it at 30G of memory use to avoid the OOM killer kicking in and disrupting other processes on this box.

    The way I set up this test:

    docker run -it ubuntu:18.10 /bin/bash
    apt update && apt upgrade -y && apt -y install clang-7 libpcre3 libpcre3-dbg libpcre3-dev build-essential autoconf automake libtool libpcap-dev libnet1-dev libyaml-0-2 libyaml-dev pkg-config zlib1g zlib1g-dev libcap-ng-dev libcap-ng0 make libmagic-dev libjansson-dev libboost-dev libboost-atomic1.67-dev libboost-date-time1.67-dev libboost-iostreams1.67-dev libboost-graph1.67-dev libboost-filesystem1.67-dev libboost-numpy1.67-dev libboost-python1.67-dev libboost-random1.67-dev libboost-thread1.67-dev libboost1.67-tools-dev libboost-test1.67-dev build-essential git cmake libgmp-dev libsqlite3-dev libapron-dev
    
    git clone https://github.com/NASA-SW-VnV/ikos
    cd ikos/
    mkdir build
    cd build/
    cmake -DLLVM_CONFIG_EXECUTABLE=/usr/bin/llvm-config-7 ../
    make
    make install
    export PATH=/ikos/install/bin/:$PATH
    cd /
    git clone https://github.com/OISF/suricata
    cd suricata/
    git clone https://github.com/OISF/libhtp
    bash autogen.sh 
    ikos-scan ./configure --disable-shared --disable-gccmarch-native
    ikos-scan make
    

    When running ikos with verbose output, I noticed that some functions were analyzed a lot of times. I'm not sure if that is normal.

    # ikos -v src/suricata.bc &> debug.log
    ... killed when process uses 10G of mem ...
    # cat debug.log | sort | uniq -c | sort -nr |head -n25
      11929 [.] Analyzing function: SCMapEnumValueToName
      11928 [.] Analyzing function: SCLocalTime
       5868 [.] Analyzing function: SCErrorToString
       3003 [.] Analyzing function: strlcpy
       2982 [.] Analyzing function: SCLogMessageJSON
       2982 [.] Analyzing function: SCLogMessageGetBuffer
       2982 [.] Analyzing function: CreateIsoTimeString
       2981 [.] Analyzing function: json_decref.8298
       2930 [.] Analyzing function: SCLogMatchFGFilter
       1987 [.] Analyzing function: SCLogPrintToStream
       1465 [.] Analyzing function: SCLogMatchFGFilterWL
       1465 [.] Analyzing function: SCLogMatchFGFilterBL
       1465 [.] Analyzing function: SCLogMatchFDFilter
        994 [.] Analyzing function: SCLogReopen
        994 [.] Analyzing function: SCLogPrintToSyslog
        994 [.] Analyzing function: SCLogMapLogLevelToSyslogLevel
        514 [.] Analyzing function: SCLogMessage
         45 [.] Analyzing function: ConfNodeLookupChild
         43 [.] Analyzing function: ConfNodeNew
         29 [.] Analyzing function: RunModeRegisterNewRunMode
         29 [.] Analyzing function: RunModeGetCustomMode
         14 [.] Analyzing function: ConfSetFinal
         14 [.] Analyzing function: ConfNodeFree
         14 [.] Analyzing function: ConfGetNodeOrCreate
          8 [.] Analyzing function: LiveRegisterDeviceName
    

    Some of the functions in this list are called from a lot of locations in the code (sometimes through macros), not sure if that is relevant. Not all of them are though. E.g. SCLogReopen is just directly called from one location, but that is from SCLogMessage, which is called for a lot of locations.

    opened by victorjulien 23
  • ikos-scan fails: error: unknown argument: '-faddrsig'

    ikos-scan fails: error: unknown argument: '-faddrsig'

    ikos fails on a very simple C++ make project:

    $ ikos-scan make 
    ikos-scan-c++ -O2 -c tsne.cpp
    error: unknown argument: '-faddrsig'
    *** Error code 1
    

    FreeBSD 11.2 amd64

    -faddrsig doesn't appear in the Makefile.

    C-bug A-ikos-scan 
    opened by yurivict 21
  • Crashed on my codebase

    Crashed on my codebase

    Just tried this static analyser on my codebase ( https://github.com/ttsiodras/renderer/ ) - and sadly, got a crash:

      CXX      renderer-BVH.o
      CXX      renderer-Loader.o
      CXX      renderer-Raytracer.o
      CXXLD    renderer
      CXX      showShadowMap-showShadowMap.o
      CXX      showShadowMap-Keyboard.o
      CXXLD    showShadowMap
    make[2]: Leaving directory '/home/ttsiod/Github/renderer/src'
    make[1]: Leaving directory '/home/ttsiod/Github/renderer/src'
    make[1]: Entering directory '/home/ttsiod/Github/renderer'
    make[1]: Nothing to be done for 'all-am'.
    make[1]: Leaving directory '/home/ttsiod/Github/renderer'
    Analyze lib3ds-1.3.0/tools/3dsdump? [Y/n] n
    Analyze src/renderer? [Y/n] Y
    [*] Running ikos src/renderer.bc -o src/renderer.db
    [*] Running ikos preprocessor
    [*] Running ikos analyzer
    [*] Translating LLVM bitcode to AR
    ikos-analyzer: /tmp/ikos-j60gqc4k/renderer.pp.bc: error: unexpected null pointer in llvm::DICompositeType with DW_TAG_structure_type or DW_TAG_class_type tag
    ikos: error: a run-time error occured
    

    The code is available in my GitHub repo, so the bug is easy to reproduce.

    C-bug 
    opened by ttsiodras 20
  • Header files not found

    Header files not found

    When I try running the example loop.c code in the Readme,

    #include <stdio.h>
    int a[10];
    int main(int argc, char *argv[]) {
            size_t i = 0;
            for (;i < 10; i++) {
                    a[i] = i;
            }
            a[i] = i;
            printf("%i", a[i]);
    }
    

    I receive the following error:

    $ ikos loop.c
    [*] Compiling loop.c
    loop.c:1:10: fatal error: 'stdio.h' file not found
    #include <stdio.h>
             ^~~~~~~~~
    1 error generated.
    ikos: error while compiling loop.c, abort.
    

    Is there any argument in ikos that we can attach header files (if this is the problem)? Thanks.

    C-bug 
    opened by strboul 17
  • Detect dynamic uninitialized variables with debug info optional

    Detect dynamic uninitialized variables with debug info optional

    1. Fix a problem in the tracking of the values of dynamically-allocated memory so that use of uninitialized dynamically-allocated memory is detected.

    2. Allow analysis of programs without debug information. This is important for the case where the LLVM comes from a binary lifter where no debug information may be available. Without debug information the name of the function with a problem is reported but file and line number information is not available.

    opened by richardlford 15
  • Failed to get it working

    Failed to get it working

    Hi,

    I failed to get it working. Here is my frustrating list of what I have tried:

    • Failed to build on Ubuntu 18.10 x64 using Clang 7 and GCC 7.3
    • Failed to install on macOS Mojave using brew install
    • Failed to build from source on macOS Mojave using clang++-7 installed using brew
    • Failed to build from source on macOS Mojave using Apple clang
    • Failed to build from source on macOS Mojave using GCC-8

    I am an expert C/C++ user, it is very rare that I fail to build any C/C++ project!

    Below are 2 error messages I encountered:

    1. The first error message is from brew install.
    2. The second error message is from building ikos from source on macOS Mojave using clang++-7.
    $ brew install nasa-sw-vnv/core/ikos
    Updating Homebrew...
    ==> Auto-updated Homebrew!
    Updated 1 tap (homebrew/core).
    ==> Updated Formulae
    mutt
    
    ==> Tapping nasa-sw-vnv/core
    Cloning into '/usr/local/Homebrew/Library/Taps/nasa-sw-vnv/homebrew-core'...
    remote: Enumerating objects: 7, done.
    remote: Counting objects: 100% (7/7), done.
    remote: Compressing objects: 100% (7/7), done.
    remote: Total 7 (delta 0), reused 5 (delta 0), pack-reused 0
    Unpacking objects: 100% (7/7), done.
    Tapped 2 formulae (34 files, 32.5KB).
    ==> Installing ikos from nasa-sw-vnv/core
    ==> Installing dependencies for nasa-sw-vnv/core/ikos: ppl and apron
    ==> Installing nasa-sw-vnv/core/ikos dependency: ppl
    ==> Downloading https://homebrew.bintray.com/bottles/ppl-1.2.mojave.bottle.1.tar.gz
    ==> Downloading from https://akamai.bintray.com/59/59aa81dbfdc59de055e528724282fb0a1f7c627fc4bbc2f6b2d026e0
    ######################################################################## 100.0%
    ==> Pouring ppl-1.2.mojave.bottle.1.tar.gz
    🍺  /usr/local/Cellar/ppl/1.2: 1,882 files, 43.4MB
    ==> Installing nasa-sw-vnv/core/ikos dependency: apron
    ==> Downloading http://apron.cri.ensmp.fr/library/apron-0.9.10.tgz
    ######################################################################## 100.0%
    ==> Patching
    patching file ppl/ppl_user.cc
    patching file products/Makefile
    ==> make APRON_PREFIX=/usr/local/Cellar/apron/0.9.10 GMP_PREFIX=/usr/local/opt/gmp MPFR_PREFIX=/usr/local/o
    🍺  /usr/local/Cellar/apron/0.9.10: 125 files, 8.8MB, built in 1 minute 40 seconds
    ==> Installing nasa-sw-vnv/core/ikos
    ==> Downloading https://github.com/nasa-sw-vnv/ikos/releases/download/v2.1/ikos-2.1.tar.gz
    ==> Downloading from https://github-production-release-asset-2e65be.s3.amazonaws.com/107311216/92e8fc00-fc91-11e8-9865-791f35ccb369?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=AKIAIWNJYA
    ######################################################################## 100.0%
    ==> Downloading https://files.pythonhosted.org/packages/4e/8b/75469c270ac544265f0020aa7c4ea925c5284b23e445cf3aa8b99f662690/virtualenv-16.1.0.tar.gz
    ######################################################################## 100.0%
    ==> python -c import setuptools... --no-user-cfg install --prefix=/private/tmp/ikos--homebrew-virtualenv-20181212-90845-13xpewv/target --install-scripts=/private/tmp/ikos--homebrew-virtualenv-
    Last 15 lines from /Users/kim/Library/Logs/Homebrew/ikos/01.python:
    -c
    import setuptools, tokenize
    __file__ = 'setup.py'
    exec(compile(getattr(tokenize, 'open', open)(__file__).read()
      .replace('\r\n', '\n'), __file__, 'exec'))
    --no-user-cfg
    install
    --prefix=/private/tmp/ikos--homebrew-virtualenv-20181212-90845-13xpewv/target
    --install-scripts=/private/tmp/ikos--homebrew-virtualenv-20181212-90845-13xpewv/target/bin
    --single-version-externally-managed
    --record=installed.txt
    
    /System/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/distutils/dist.py:267: UserWarning: Unknown distribution option: 'python_requires'
      warnings.warn(msg)
    error in virtualenv setup command: 'extras_require' must be a dictionary whose values are strings or lists of strings containing valid project/version requirement specifiers.
    
    If reporting this issue please do so at (not Homebrew/brew or Homebrew/core):
    https://github.com/nasa-sw-vnv/homebrew-core/issues
    
    /usr/local/Homebrew/Library/Homebrew/utils/github.rb:245:in `raise_api_error': GitHub Must specify two-factor authentication OTP code.:The GitHub credentials in the macOS keychain may be invalid. (GitHub::AuthenticationFailedError)
    Clear them with:
      printf "protocol=https\nhost=github.com\n" | git credential-osxkeychain erase
    Or create a personal access token:
      https://github.com/settings/tokens/new?scopes=gist,public_repo&description=Homebrew
    echo 'export HOMEBREW_GITHUB_API_TOKEN=your_token_here' >> ~/.bash_profile
    	from /usr/local/Homebrew/Library/Homebrew/utils/github.rb:206:in `open_api'
    	from /usr/local/Homebrew/Library/Homebrew/utils/github.rb:324:in `search'
    	from /usr/local/Homebrew/Library/Homebrew/utils/github.rb:257:in `search_issues'
    	from /usr/local/Homebrew/Library/Homebrew/utils/github.rb:270:in `issues_for_formula'
    	from /usr/local/Homebrew/Library/Homebrew/exceptions.rb:372:in `fetch_issues'
    	from /usr/local/Homebrew/Library/Homebrew/exceptions.rb:368:in `issues'
    	from /usr/local/Homebrew/Library/Homebrew/exceptions.rb:422:in `dump'
    	from /usr/local/Homebrew/Library/Homebrew/brew.rb:127:in `rescue in <main>'
    	from /usr/local/Homebrew/Library/Homebrew/brew.rb:17:in `<main>'
    
    $ CXX=/usr/local/opt/llvm@7/bin/clang++ CC=/usr/local/opt/llvm@7/bin/clang cmake .. -DLLVM_CONFIG_EXECUTABLE="$(brew --prefix)/opt/llvm@7/bin/llvm-config"
    -- The C compiler identification is Clang 7.0.0
    -- The CXX compiler identification is Clang 7.0.0
    -- Check for working C compiler: /usr/local/opt/llvm@7/bin/clang
    -- Check for working C compiler: /usr/local/opt/llvm@7/bin/clang -- works
    -- Detecting C compiler ABI info
    -- Detecting C compiler ABI info - done
    -- Detecting C compile features
    -- Detecting C compile features - done
    -- Check for working CXX compiler: /usr/local/opt/llvm@7/bin/clang++
    -- Check for working CXX compiler: /usr/local/opt/llvm@7/bin/clang++ -- works
    -- Detecting CXX compiler ABI info
    -- Detecting CXX compiler ABI info - done
    -- Detecting CXX compile features
    -- Detecting CXX compile features - done
    -- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
    -- Including core
    -- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
    -- Found Boost: /usr/local/include (found version "1.68.0")
    -- Found the following Boost libraries:
    --   unit_test_framework
    -- Found GMP: /usr/local/include  
    -- Found MPFR: /usr/local/include (Required is at least version "1.0.0") 
    -- Found PPL: /usr/local/Cellar/ppl/1.2/include  
    -- Found APRON: /usr/local/include  
    -- Performing Test CXX_SUPPORTS_CXX14
    -- Performing Test CXX_SUPPORTS_CXX14 - Success
    -- Performing Test CXX_SUPPORTS_FVISIBILITY_INLINES_HIDDEN
    -- Performing Test CXX_SUPPORTS_FVISIBILITY_INLINES_HIDDEN - Success
    -- Performing Test CXX_SUPPORTS_WALL
    -- Performing Test CXX_SUPPORTS_WALL - Success
    -- Performing Test CXX_SUPPORTS_WEXTRA
    -- Performing Test CXX_SUPPORTS_WEXTRA - Success
    -- Performing Test CXX_SUPPORTS_WEVERYTHING
    -- Performing Test CXX_SUPPORTS_WEVERYTHING - Success
    -- Performing Test CXX_SUPPORTS_WNO_SWITCH_ENUM
    -- Performing Test CXX_SUPPORTS_WNO_SWITCH_ENUM - Success
    -- Performing Test CXX_SUPPORTS_WNO_PADDED
    -- Performing Test CXX_SUPPORTS_WNO_PADDED - Success
    -- Performing Test CXX_SUPPORTS_WNO_CXX98_COMPAT
    -- Performing Test CXX_SUPPORTS_WNO_CXX98_COMPAT - Success
    -- Performing Test CXX_SUPPORTS_WNO_CXX98_COMPAT_PEDANTIC
    -- Performing Test CXX_SUPPORTS_WNO_CXX98_COMPAT_PEDANTIC - Success
    -- Performing Test CXX_SUPPORTS_WNO_C99_EXTENSIONS
    -- Performing Test CXX_SUPPORTS_WNO_C99_EXTENSIONS - Success
    -- Performing Test CXX_SUPPORTS_WNO_COVERED_SWITCH_DEFAULT
    -- Performing Test CXX_SUPPORTS_WNO_COVERED_SWITCH_DEFAULT - Success
    -- Performing Test CXX_SUPPORTS_WNO_EXIT_TIME_DESTRUCTORS
    -- Performing Test CXX_SUPPORTS_WNO_EXIT_TIME_DESTRUCTORS - Success
    -- Performing Test CXX_SUPPORTS_WNO_GLOBAL_CONSTRUCTORS
    -- Performing Test CXX_SUPPORTS_WNO_GLOBAL_CONSTRUCTORS - Success
    -- Performing Test CXX_SUPPORTS_WNO_WEAK_VTABLES
    -- Performing Test CXX_SUPPORTS_WNO_WEAK_VTABLES - Success
    -- Performing Test CXX_SUPPORTS_WNO_DISABLED_MACRO_EXPANSION
    -- Performing Test CXX_SUPPORTS_WNO_DISABLED_MACRO_EXPANSION - Success
    -- Found Doxygen: /usr/local/bin/doxygen (found version "1.8.14") found components:  doxygen dot 
    -- Including ar
    -- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
    -- Found Boost: /usr/local/include (found version "1.68.0")
    -- Including frontend/llvm
    -- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
    -- Found Boost: /usr/local/include (found version "1.68.0")
    -- Found the following Boost libraries:
    --   filesystem
    --   system
    -- Found LLVM: /usr/local/Cellar/llvm/7.0.0_1 (found version "7.0.0") 
    -- Performing Test LLVM_NO_OLD_LIBSTDCXX
    -- Performing Test LLVM_NO_OLD_LIBSTDCXX - Success
    -- Performing Test C_SUPPORTS_FPIC
    -- Performing Test C_SUPPORTS_FPIC - Success
    -- Performing Test CXX_SUPPORTS_FPIC
    -- Performing Test CXX_SUPPORTS_FPIC - Success
    -- Building with -fPIC
    -- Performing Test SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG
    -- Performing Test SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG - Success
    -- Performing Test C_SUPPORTS_WERROR_DATE_TIME
    -- Performing Test C_SUPPORTS_WERROR_DATE_TIME - Success
    -- Performing Test CXX_SUPPORTS_WERROR_DATE_TIME
    -- Performing Test CXX_SUPPORTS_WERROR_DATE_TIME - Success
    -- Performing Test C_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW
    -- Performing Test C_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW - Success
    -- Performing Test CXX_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW
    -- Performing Test CXX_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW - Success
    -- Performing Test CXX_SUPPORTS_CXX11
    -- Performing Test CXX_SUPPORTS_CXX11 - Success
    -- Linker detection: ld64
    -- Including analyzer
    -- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
    -- Found Boost: /usr/local/include (found version "1.68.0")
    -- Found the following Boost libraries:
    --   filesystem
    --   system
    -- Found SQLite3: /Library/Frameworks/Mono.framework/Headers  
    -- Found PythonInterp: /usr/bin/python (found version "2.7.10") 
    -- Building with -fPIC
    -- Linker detection: ld64
    -- Found Clang: /usr/local/Cellar/llvm/7.0.0_1/bin/clang (found version "7.0.0") 
    -- Performing Test CXX_SUPPORTS_WNO_UNUSED_LOCAL_TYPEDEFS
    -- Performing Test CXX_SUPPORTS_WNO_UNUSED_LOCAL_TYPEDEFS - Success
    -- Configuring done
    -- Generating done
    -- Build files have been written to: /Users/kim/Downloads/ikos-master/build
    Delphines-MBP:build kim$ time make -j8
    Scanning dependencies of target ikos-python
    Scanning dependencies of target ikos-llvm-to-ar
    Scanning dependencies of target ikos-pp-lib
    Scanning dependencies of target ikos-ar
    [  1%] Generating python/ikos/settings/__init__.py
    [  1%] Generating python/build/lib/ikos/__init__.py
    [  3%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/initialize.cpp.o
    [  5%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/lower_cst_expr.cpp.o
    [  5%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/mark_internal_inline.cpp.o
    [  5%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/lower_select.cpp.o
    [  6%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/mark_no_return_function.cpp.o
    [  6%] Built target ikos-python
    [  6%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/name_values.cpp.o
    [  8%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/bundle.cpp.o
    [ 10%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/dot.cpp.o
    [ 10%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/constant.cpp.o
    [ 10%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/namer.cpp.o
    [ 11%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/data_layout.cpp.o
    [ 13%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/text.cpp.o
    [ 13%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/exception.cpp.o
    [ 15%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/remove_printf_calls.cpp.o
    [ 15%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/add_loop_counters.cpp.o
    [ 15%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/remove_unreachable_blocks.cpp.o
    [ 16%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/name_values.cpp.o
    [ 18%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/function.cpp.o
    [ 18%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/pass.cpp.o
    [ 20%] Linking CXX static library libikos-pp.a
    [ 20%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/importer.cpp.o
    [ 20%] Built target ikos-pp-lib
    [ 21%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/simplify_cfg.cpp.o
    [ 23%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/library_function.cpp.o
    Scanning dependencies of target ikos-pp
    [ 23%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/unify_exit_nodes.cpp.o
    [ 25%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp.dir/src/ikos_pp.cpp.o
    [ 25%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/source_location.cpp.o
    [ 26%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/type.cpp.o
    [ 28%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/simplify_upcast_comparison.cpp.o
    [ 28%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/bundle.cpp.o
    [ 30%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/code.cpp.o
    [ 30%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context.cpp.o
    [ 31%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context_impl.cpp.o
    [ 31%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/data_layout.cpp.o
    [ 33%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/function.cpp.o
    [ 33%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/intrinsic.cpp.o
    [ 35%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/statement.cpp.o
    [ 35%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/type.cpp.o
    [ 35%] Linking CXX executable ikos-pp
    [ 36%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/value.cpp.o
    [ 36%] Built target ikos-pp
    [ 36%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/frontend.cpp.o
    [ 38%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/type.cpp.o
    [ 38%] Linking CXX static library libikos-llvm-to-ar.a
    [ 38%] Built target ikos-llvm-to-ar
    [ 38%] Linking CXX static library libikos-ar.a
    [ 38%] Built target ikos-ar
    Scanning dependencies of target ikos-import
    Scanning dependencies of target ikos-analyzer
    [ 40%] Building CXX object frontend/llvm/CMakeFiles/ikos-import.dir/src/ikos_import.cpp.o
    [ 40%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/call_context.cpp.o
    [ 41%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/ikos_analyzer.cpp.o
    [ 43%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/fixpoint_profile.cpp.o
    [ 43%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/hardware_addresses.cpp.o
    [ 45%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/literal.cpp.o
    [ 45%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/liveness.cpp.o
    [ 46%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/memory_location.cpp.o
    /Users/kim/Downloads/ikos-master/analyzer/src/analysis/call_context.cpp:60:16: error: no member named 'try_emplace' in 'llvm::DenseMap<std::__1::pair<ikos::analyzer::CallContext *,
          ikos::ar::CallBase *>, std::__1::unique_ptr<ikos::analyzer::CallContext, std::__1::default_delete<ikos::analyzer::CallContext> >,
          llvm::DenseMapInfo<std::__1::pair<ikos::analyzer::CallContext *, ikos::ar::CallBase *> > >'
        this->_map.try_emplace({parent, call},
        ~~~~~~~~~~ ^
    1 error generated.
    make[2]: *** [analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/call_context.cpp.o] Error 1
    make[2]: *** Waiting for unfinished jobs....
    In file included from /Users/kim/Downloads/ikos-master/analyzer/src/analysis/memory_location.cpp:47:
    In file included from /Users/kim/Downloads/ikos-master/analyzer/include/ikos/analyzer/util/source_location.hpp:50:
    In file included from /Users/kim/Downloads/ikos-master/frontend/llvm/include/ikos/frontend/llvm/import/source_location.hpp:50:
    In file included from /usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:26:
    In file included from /usr/local/Cellar/llvm/7.0.0_1/include/llvm/BinaryFormat/Dwarf.h:28:
    /usr/local/Cellar/llvm/7.0.0_1/include/llvm/Support/FormatVariadicDetails.h:66:20: error: no template named 'SameType'
      static char test(SameType<Signature_format, &U::format> *);
                       ^
    In file included from /Users/kim/Downloads/ikos-master/analyzer/src/analysis/memory_location.cpp:47:
    In file included from /Users/kim/Downloads/ikos-master/analyzer/include/ikos/analyzer/util/source_location.hpp:50:
    In file included from /Users/kim/Downloads/ikos-master/frontend/llvm/include/ikos/frontend/llvm/import/source_location.hpp:50:
    /usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:72:9: error: unknown type name 'Metadata'
      const Metadata *MD = nullptr;
            ^
    /usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:79:33: error: unknown type name 'Metadata'
      explicit TypedDINodeRef(const Metadata *MD) : MD(MD) {
                                    ^
    /usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:90:12: error: unknown type name 'Metadata'
      operator Metadata *() const { return const_cast<Metadata *>(MD); }
               ^
    /usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:98:34: error: unknown type name 'DINode'; did you mean 'MDNode'?
    using DINodeRef = TypedDINodeRef<DINode>;
                                     ^
    /Library/Frameworks/Mono.framework/Headers/llvm/IR/Metadata.h:126:7: note: 'MDNode' declared here
    class MDNode : public Value, public FoldingSetNode {
          ^
    In file included from /Users/kim/Downloads/ikos-master/analyzer/src/analysis/memory_location.cpp:47:
    In file included from /Users/kim/Downloads/ikos-master/analyzer/include/ikos/analyzer/util/source_location.hpp:50:
    In file included from /Users/kim/Downloads/ikos-master/frontend/llvm/include/ikos/frontend/llvm/import/source_location.hpp:50:
    /usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:99:35: error: use of undeclared identifier 'DIScope'
    using DIScopeRef = TypedDINodeRef<DIScope>;
    ...
    
    C-compiler-error 
    opened by kimwalisch 15
  • Problem with narrowing strategy for nonmonotonic transformation function

    Problem with narrowing strategy for nonmonotonic transformation function

    int count = 10;
    int main() {
      int i;
      for (i = 0; i < 10; i++) {
        count = count >> 1;
      }
      return 0;
    }
    

    it seems having problem with narrowing strategy for nonmonotonic transformation function. like code upon, using interval domain, the analyzer can not stop.

    C-bug L-c 
    opened by wutianba 14
  • Assertion failed: (ar_cst), function translate_constant, file frontend/llvm/src/import/constant.cpp, line 200

    Assertion failed: (ar_cst), function translate_constant, file frontend/llvm/src/import/constant.cpp, line 200

    The following code: https://github.com/myfreeweb/soad/blob/ef9b4e93ad02f66825c4174de4e38fc3174ee29b/soad.c

    Apparently has some kind of integer constant ikos doesn't like:

    (lldb) p *cst
    error: ikos-analyzer 0x02dedb51: DW_TAG_inheritance failed to resolve the base class at 0x02dedbd3 from enclosing type 0x02dedb48.
    Please file a bug and attach the file at the start of this error message
    (llvm::Constant) $0 = {
      llvm::User = {
        llvm::Value = {
          VTy = 0x00000008017c96c8
          UseList = 0x00000008017dfc90
          SubclassID = '\r'
          HasValueHandle = '\0'
          SubclassOptionalData = '\0'
          SubclassData = 0
          NumUserOperands = 0
          IsUsedByMD = 0
          HasName = 0
          HasHungOffUses = 0
          HasDescriptor = 0
        }
      }
    }
    (lldb) p *cst->VTy
    (llvm::Type) $1 = {
      Context = 0x00007fffffffc7f0
      ID = IntegerTyID
      SubclassData = 32
      NumContainedTys = 0
      ContainedTys = 0x0000000000000000
    }
    

    (or maybe this is caused by other weird bugs.. running on FreeBSD 13-current with system llvm70, most programs are causing failures)

    C-bug C-upstream 
    opened by valpackett 12
  • error: unexpected tag for union member of llvm::DICompositeType

    error: unexpected tag for union member of llvm::DICompositeType

    Thanks for a very impressive tool!

    I've successfully tried ikos against various small programs. I really like it!

    When giving it a try against the Bitcoin Core project I encountered an error which I'm unable to resolve:

    $ git clone https://github.com/bitcoin/bitcoin bitcoin-ikos
    $ cd bitcoin-ikos/
    $ ./autogen.sh
    $ ikos-scan ./configure --disable-wallet --disable-hardening --disable-asm --disable-zmq --with-gui=no --without-miniupnpc --disable-bench --enable-debug
    $ ikos-scan make
    …
    make[1]: Leaving directory '/root/build-bitcoin/bitcoin-ikos'
    Analyze src/bitcoin-cli? [Y/n]
    [*] Running ikos src/bitcoin-cli.bc -o src/bitcoin-cli.db
    [*] Running ikos preprocessor
    [*] Running ikos analyzer
    [*] Translating LLVM bitcode to AR
    ikos-analyzer: /tmp/ikos-BQBQ4G/bitcoin-cli.pp.bc: error: unexpected tag for union member of llvm::DICompositeType
    ikos: error: a run-time error occured
    

    What can I do to try to resolve it? :-)

    C-bug L-c++ 
    opened by practicalswift 12
  • Remove mention of AUR helpers

    Remove mention of AUR helpers

    AUR helpers are fully unsupported by the Arch Linux development team. Besides my statement as a Trusted User, see the following links:

    https://bbs.archlinux.org/viewtopic.php?pid=828310#p828310 https://wiki.archlinux.org/index.php/AUR_helpers https://bugs.archlinux.org/task/56602#comment164090

    Besides these considerations, the AUR itself has in 2015 adopted git, making these helpers for simple tasks such as these (one package and one dependency) obsolete. Users can easily keep track of updates by enabling email notifications on the AUR website.

    opened by AladW 12
  • error: unsupported llvm instruction fneg

    error: unsupported llvm instruction fneg

    Hi,

    I have got a strange behaviour of the ikos analyzer with the following C++ class of a simple vector. I get the error:

    > ikos vector.cpp 
    [*] Compiling vector.cpp
    [*] Running ikos preprocessor
    [*] Running ikos analyzer
    [*] Translating LLVM bitcode to AR
    ikos-analyzer: /tmp/ikos-5o9i8j4_/vector.pp.bc: error: unsupported llvm instruction fneg [2]
    ikos: error: a run-time error occurred
    

    However, if I change the line

    vector.m_vector[i] = -m_vector[i];      // This doesn't !
    

    into

    vector.m_vector[i] = 0.-m_vector[i];  // This works
    

    everything works fine. I also got similar behaviours with other expressions using the binary "-" operator when self-defined classes are involved...

    any help would be really appreciated.

    Here comes an extract of my sample program vector.cpp

    KR

    Ingo

    #define VEC_MAX_DIM 10
    
    namespace linmath 
    {
        typedef float        TLMFloat;
        typedef unsigned int TLMUInt;
        
        class CVector 
        {
        public:
            CVector(TLMUInt dimension=1,TLMFloat value=0.) noexcept;
            CVector operator- () const;
    
        protected:
            // Vector dimension
            TLMUInt m_dimension;
            // Storage to store the vector elements
            TLMFloat m_vector[VEC_MAX_DIM];
        };
        
    CVector::CVector(TLMUInt dimension,TLMFloat value) noexcept
    {
        m_dimension = dimension;
        for (TLMUInt i=0;i<dimension;i++)
        {
            m_vector[i] = value;
        }    
    }
    
    CVector CVector::operator-() const
    {
        CVector vector(m_dimension);
        for (TLMUInt i=0;i<m_dimension;i++)
        {
    //        vector.m_vector[i] = 0.-m_vector[i];  // This works
            vector.m_vector[i] = -m_vector[i];      // This doesn't !
        }    
        return vector;
    }
    
    }; 
    
    int main(int argc,char **argv=0)
    {
        return 0;
    }
    
    opened by ingoahrns 0
  • Bogus warning 'expression xx might be uninitialized'

    Bogus warning 'expression xx might be uninitialized'

    In this program:

    #include <stdio.h>
    
    int a[10];
    int main(int argc, char *argv[]) {
        int i = 0;
        for (; i < 10; ++i)
            a[i] = i;
        printf("%i", a[i - 10]);
    }
    

    a[i-10] is initialized in the end, but ikos complains that it isn't initialized.

    # Results
    loop.c: In function 'main':
    loop.c:8:5: warning: expression 'a[(int64_t)(i - 10)]' might be uninitialized
        printf("%i", a[i - 10]);
        ^
    

    Version: 3.1 FreeBSD 13.1

    opened by yurivict 1
  • Replace conditional assignment to a variable with an if expression

    Replace conditional assignment to a variable with an if expression

    Change Description

    This PR aims to replace several conditional assignments to a variable by if expressions.

    Rationale

    The ternary operator is represented by the conditional expression syntax of Python. This is a significant improvement in the case where the conditional expression is :

    • short and can be written on a single line

    • not difficult (no nested expressions or long boolean strings).

    opened by ThibFrgsGmz 2
  • ikos crashes during preprocessing

    ikos crashes during preprocessing

    I was running ikos using a bitcode file compiled from clang-9.

    The command is:

    ikos -a=boa redis-cli.bc 2>&1 | tee log
    

    The stack trace is:

    #0  0x000055bb668ab98d in ikos::frontend::import::FunctionImporter::translate_phi_l
    ate(ikos::frontend::import::BasicBlockTranslation*, llvm::PHINode*) ()
    #1  0x000055bb668ac136 in ikos::frontend::import::FunctionImporter::translate_phi_n
    odes(ikos::frontend::import::BasicBlockTranslation*, llvm::BasicBlock*) ()
    #2  0x000055bb668b27b1 in ikos::frontend::import::FunctionImporter::translate_phi_n
    odes() ()
    #3  0x000055bb668b4d55 in ikos::frontend::import::FunctionImporter::translate_contr
    ol_flow_graph() ()
    #4  0x000055bb668b4d75 in ikos::frontend::import::FunctionImporter::translate_body(
    ) ()
    #5  0x000055bb668a21a1 in ikos::frontend::import::BundleImporter::translate_functio
    n_body(llvm::Function*) ()
    #6  0x000055bb66892cdb in ikos::frontend::import::Importer::import(llvm::Module&, i
    kos::ar::Flags<ikos::frontend::import::Importer::ImportOption>) ()
    #7  0x000055bb665b95d1 in main ()
    

    The bitcode file is attached for your reference. redis-cli.zip

    opened by yiyuaner 0
  • Support for building on Ubuntu 22.04

    Support for building on Ubuntu 22.04

    ikos currently requires llvm 9 which is no longer available in Ubuntu 22.04.

    LLVM 11, 12, 13, and 14 are all packaged in 22.04. As a side note, Debian Bullseye (the current stable release) provides LLVM 11 and 13 but not 12 and 14 was not yet released.

    It looks like the pending work on LLVM 10 has stalled https://github.com/NASA-SW-VnV/ikos/pull/162. Looking at the above release coverage, 13 would probably the next version to target in order to build on current (and likely at least one future) releases of Debian and Ubuntu.

    opened by nuclearsandwich 0
Owner
NASA - Software V&V
NASA - Software Verification and Validation
NASA - Software V&V
Qt-oriented static code analyzer based on the Clang framework

WARNING: master is the development branch. Please use the v1.10 branch. clazy v1.11 clazy is a compiler plugin which allows clang to understand Qt sem

KDE GitHub Mirror 555 Jan 8, 2023
A static analyzer for Java, C, C++, and Objective-C

Infer Infer is a static analysis tool for Java, C++, Objective-C, and C. Infer is written in OCaml. Installation Read our Getting Started page for det

Facebook 13.8k Jan 4, 2023
Static code checker for C++

cpplint - static code checker for C++ Cpplint is a command-line tool to check C/C++ files for style issues following Google's C++ style guide. Cpplint

null 1.2k Jan 7, 2023
Pharos Static Binary Analysis Framework

Automated static analysis tools for binary programs

Software Engineering Institute 1.3k Dec 18, 2022
CITL's static analysis engine for native code artifacts

citl-static-analyzer Fast binary hardening analysis tooling. Building on Linux The build process varies by Linux distribution, owing to differences be

Cyber Independent Testing Lab 18 Aug 30, 2022
ELF static analysis and injection framework that parse, manipulate and camouflage ELF files.

elfspirit elfspirit is a useful program that parse, manipulate and camouflage ELF files. It provides a variety of functions, including adding or delet

null 21 Dec 21, 2022
A static analysis tool that helps security researchers scan a list of Windows kernel drivers for common vulnerability patterns in drivers (CVE makers!)

Driver Analyzer A static analysis tool that helps security researchers scan a list of Windows kernel drivers for common vulnerability patterns in driv

BehroozAbbassi 44 Sep 3, 2022
Static analysis of C/C++ code

Cppcheck GitHub Actions Linux Build Status Windows Build Status OSS-Fuzz Coverity Scan Build Status License About the name The original name of this p

Daniel Marjamäki 4.5k Dec 30, 2022
Static analyzer for C/C++ based on the theory of Abstract Interpretation.

IKOS IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation. Introduction IKO

NASA - Software V&V 1.8k Dec 28, 2022
Legacy stepper motor analyzer - A DYI minimalist hardware stepper motor analyzer with graphical touch screen.

Simple Stepper Motor Analyzer NOTE: This is the legacy STM32 based design which was replaced by the single board, Raspberry Pi Pico design at https://

Zapta 160 Dec 26, 2022
✔️The smallest header-only GUI library(4 KLOC) for all platforms

Welcome to GUI-lite The smallest header-only GUI library (4 KLOC) for all platforms. 中文 Lightweight ✂️ Small: 4,000+ lines of C++ code, zero dependenc

null 6.6k Jan 8, 2023
A LLVM-based static analyzer to produce PyTorch operator dependency graph.

What is this? This is a clone of the deprecated LLVM-based static analyzer from the PyTorch repo, which can be used to produce the PyTorch operator de

Jiakai Liu 5 Dec 15, 2021
Qt-oriented static code analyzer based on the Clang framework

WARNING: master is the development branch. Please use the v1.10 branch. clazy v1.11 clazy is a compiler plugin which allows clang to understand Qt sem

KDE GitHub Mirror 555 Jan 8, 2023
A static analyzer for Java, C, C++, and Objective-C

Infer Infer is a static analysis tool for Java, C++, Objective-C, and C. Infer is written in OCaml. Installation Read our Getting Started page for det

Facebook 13.8k Jan 4, 2023
Yggdrasil Decision Forests (YDF) is a collection of state-of-the-art algorithms for the training, serving and interpretation of Decision Forest models.

Yggdrasil Decision Forests (YDF) is a collection of state-of-the-art algorithms for the training, serving and interpretation of Decision Forest models. The library is developed in C++ and available in C++, CLI (command-line-interface, i.e. shell commands) and in TensorFlow under the name TensorFlow Decision Forests (TF-DF).

Google 268 Jan 9, 2023
Based on the spatial resection theory, the algorithm solves the camera position by solving the homography matrix.

Based on the spatial resection theory, the algorithm solves the camera position by solving the homography matrix.

null 1 Nov 13, 2021
Source code for pbrt, the renderer described in the third edition of "Physically Based Rendering: From Theory To Implementation", by Matt Pharr, Wenzel Jakob, and Greg Humphreys.

pbrt, Version 3 This repository holds the source code to the version of pbrt that is described in the third edition of Physically Based Rendering: Fro

Matt Pharr 4.4k Jan 7, 2023
Repository for material related to the Programming Languages Virtual Meetup coverage of the Category Theory for Programmers book.

CTfP-2021 This is the material (code and presentation slide decks) that correspond to the Programming Languages Virtual Meetup course that is covering

Conor Hoekstra 119 Dec 5, 2022
A command line tool for numerically computing Out-of-time-ordered correlations for N=4 supersymmetric Yang-Mills theory and Beta deformed N=4 SYM.

A command line tool to compute OTOC for N=4 supersymmetric Yang–Mills theory This is a command line tool to numerically compute Out-of-time-ordered co

Gaoli Chen 1 Oct 16, 2021
BSAL(Bluetooth Stack Abstract Layer)软件包是由 RT-Thread 针对不同 蓝牙协议栈接口实现的,目前支持的 协议栈有:nimble,realtek 等协议栈

BSAL (Bluetooth Stack Abstract Layer)软件包是由 RT-Thread 针对不同 蓝牙协议栈接口实现的,目前支持的 协议栈有:nimble,realtek 等协议栈。

The packages repositories of RT-Thread. 14 Sep 19, 2022