NIKOS v2.4.0

Fixed

• LLVM frontend: the importer recovers pointer element types from the debug
  information (previously every pointer was translated to opaque*, losing
  signedness and layouts), types allocas from llvm.dbg.declare only (a
  llvm.dbg.value on an array made the array a scalar), and handles anonymous
  typedef struct types, class templates, C++ empty bases and
  [[no_unique_address]] members, pointers to members, empty parameters
  dropped by clang, llvm.global_ctors, and glibc symbol aliases. The
  ikos-import regression tests are regenerated from upstream's expectations;
  var-args.ll, vla.ll and virtual-inheritance.ll are no longer skipped.
• ikos-pp lowers sized and aligned operator new/operator delete (default
  in clang 19+, including their 32-bit manglings) so that dfa, boa and
  uaf see them; the std::thread modeling pass no longer crashes on
  invoke instructions, including for pthread_once.
• LLVM frontend: an alloca is no longer typed from the debug information of
  another variable (a reference bound to a temporary made the allocation too
  small, or opaque); classes passed by reference are matched against every
  structure type of the module with the same name, whatever its .<n> suffix.
• Composite scalar domain: the taint component was widened and narrowed twice
  and the taint of assigned integers was forgotten.
• Buffer overflow checker: no more assertion failure on zero-sized element
  types.
• Value analysis: the models of read, gets and fgets wrote a literal zero
  byte into the buffer, hiding bugs from every checker.
• Analysis engine: a pointer to a local variable returned by a function is now
  matched with the result of the call, so use-after-return through return &x
  is detected.
• Taint analysis: tainted memory is tracked per memory location (definitely and
  possibly tainted), taint propagates through operations, unknown functions,
  strdup, strndup, memcpy, memmove and the string functions, sinks
  receiving possibly tainted data are warnings, sources in the configuration
  are honored (including scanf, recv, getline), and -a=taint requires
  a taint configuration. Unknown functions no longer clear the taint of the
  buffers they receive, overwriting a buffer with untainted data (strcpy,
  sprintf, memset) makes it possibly tainted only, string literals and
  other constants are never tainted, and integers loaded from memory carry the
  taint of their cell.
• Concurrency checker: rewritten as a lockset analysis with a thread count; no
  crash on unknown pointers or without pointer analysis; std::mutex and lock
  guards recognized by name (including guards over mutex types with nested
  names); single-threaded code is not reported.
• Use-after-free checker: unknown, null and uninitialized pointers are left to
  the other checkers, use-after-return is only reported for local variables.
• Use-after-move checker: rewritten on top of the value analysis (dereference
  of a null pointer loaded from a moved-from object) instead of a global set of
  moved locations; no hardcoded class names; reassigned objects are not
  reported.
• ikos-report and ikos-view no longer crash on the new check kinds;
  ikos-report -t no longer crashes on a database without timing results; the
  SARIF rules are the check kinds, so that every result refers to a declared
  rule; ikos-view check kind filters work and malformed filters are ignored;
  ikos-serve uses the right columns and reports a missing database at
  startup; ikos-scan --taint keeps the default analyses; the taint
  configuration is only passed to the analyzer when the taint analysis is
  enabled, and ikos warns when --taint-config or --taint-profile is given
  without it.
• script/regen_checks.py: leading output lines are kept, CHECK-LABEL
  lines are regenerated correctly when the label changes, tests without CHECK
  lines are supported, failures to run the tools are reported, and the tools
  can be given with --ikos-import and --file-check.
• Packaging: the python virtual environment is created in the staging
  directory when make install runs with DESTDIR, so the Debian package
  contains it; the package installs under /opt/nikos, links the tools into
  /usr/bin and depends on clang-20 and llvm-20; the continuous
  integration builds, checks and publishes it for tagged releases;
  script/install.sh installs the latest release on Ubuntu 24.04; the Docker
  image builds again (LLVM apt repository in both stages, python3-venv);
  versions taken from the project version; RPM file list matches the install
  tree; LLVM apt repository key handled without apt-key.

Changed

• uaf is no longer part of the default analyses of the ikos driver (boa
  already reports use after free and use after return).
• fastapi and uvicorn are optional (pip install ikos[serve]);
  nikos-bridge summarizes a SARIF report and no longer modifies sources.
• Removed the IKOS 3.0 installation guides, the old distribution Dockerfiles,
  script/bootstrap, the duplicated test/taint directory and the tracked
  build artifacts.
• Documentation rewritten to match the tools.

v2.3.2

Fixes an AR bitcast mapping issue when identically structured types are bitcast due to LLVM 20 opaque pointer inference.

v2.3.1.1: Fix CI build failures (Linux + macOS)

Fixes CI build failures (Linux + macOS) caused by an outdated pip module update and incorrect taint_config.json path.

v2.3.1 — LLVM 20 Regression Test Suite Complete

What's Fixed

All 162 non-skipped regression tests now pass across all three import test suites (no_optimization, basic_optimization, aggressive_optimization). Previously 40+ tests were failing due to AR output differences between LLVM 14 and LLVM 20 that weren't caught locally because the system ikos-import was built against LLVM 14.

Fixed

• no_optimization/ — 37 files: concrete scalar alloca types (allocate opaque → allocate si32/float/etc.), bitcast elimination cascades, struct layout resolution, SSA renumbering
• basic_optimization/ — 3 files: bitfield signedness (ui16 → si16), struct alloca types, PHI node renumbering
• aggressive_optimization/ — 1 file: vtable bitcast chain

Added

• script/regen_checks.py — auto-regenerates ; CHECK: lines in .ll test files from actual ikos-import output. Use this instead of hand-editing after any future LLVM upgrade.
• doc/LLVM20_AR_CHANGES.md — reference guide covering every AR output behavioral change between LLVM 14 and LLVM 20, with before/after examples and a troubleshooting checklist.
• README — new "Working with the Test Suite" section linking to the above.

Full Changelog

See CHANGELOG.md for complete details.

Full diff: v2.3.0...v2.3.1

v2.0.1: Fix CI build failures (Linux + macOS)

Bug Fixes

Linux: Fatal — nlohmann/json.hpp not found

taint_config.cpp uses #include <nlohmann/json.hpp> for parsing taint configuration files, but the dependency was never declared in CMake and the CI never installed the package. This caused a fatal compile error at ~83% of the build.

Fixed by:

• analyzer/CMakeLists.txt: Added find_package(nlohmann_json 3.2.0 QUIET) with a FetchContent fallback (v3.11.3). Linked to ikos-analyzer via the modern CMake target nlohmann_json::nlohmann_json.
• build-linux.yml: Added nlohmann-json3-dev to apt-get install (preferred over FetchContent download).
• build-macos.yml: Added nlohmann-json to brew install.

macOS + Linux: Missing override on taint virtual methods

memory/abstract_domain.hpp defined taint_assign_labeled() and taint_get_labels() without the override specifier, despite overriding virtuals from scalar/abstract_domain.hpp. This produces -Wsuggest-override warnings on GCC and Clang.

Fixed by: Adding override to both methods in core/include/ikos/core/domain/memory/abstract_domain.hpp.

NIKOS v2.0.0

Version 2.0 adds powerful new additions: Taint Analysis, Use-After-Move Detection, Advanced Concurrency Modeling (std::thread), Web APIs, and more built for the Nitpick ecosystem.

NIKOS v1.0.1 (Legacy / Drop-in Replacement)

Official drop-in replacement for NASA IKOS updated for LLVM 20. No extra features, just stability and modern LLVM support.