GSAF
====

GSAF is a path-sensitive bug-finding engine over Lotus's guarded value-flow
IR (GVFG).

Run it through the unified checker frontend::

   lotus-check --engine=gsaf --checks=taint,use-after-free input.bc
   lotus-check --engine=gsaf --checks=all --report-json=report.json input.bc

The engine implementation is in ``lib/Checker/GSAF``. Library contracts reuse
``Annotation/APISpec`` and ``Annotation/Taint``. Build the ``GSAF`` library or
``lotus-check`` executable. Run existing component tests with::

   build/bin/tests/checker_tests --gtest_filter='GSAF*'

Organization
------------

Public headers mirror the implementation directories:

* ``API``: vulnerability contracts, traces, registration and annotation model queries.
* ``Engine``: four header/source pairs for the module checker, taint traversal,
  solver and summaries.
* ``Checkers``: the two built-in checks (use after free and taint).
* ``Report``: diagnostic rendering and trace scoring.
* ``Support``: GSAF-specific options, queries, masks and object ordering.

Reusable analyses and reporting primitives live in their respective Lotus
subsystems. Framework diagnostic events and composition extend
``DiagnosticEvent`` and ``CheckerDiagnostic``; all report steps use ``BugReport``.
LLVM/GVFG narrative rendering belongs to GSAF. See ``lib/Checker/GSAF/README.md`` for the dependency boundaries.
The per-function engine is ``Engine/FunctionAnalyzer``. Checker trace containers,
reporting metadata, and the LLVM value-pair representation live in
``Checker/Framework/ValueTrace.h`` and ``Checker/Framework/LLVMValueTrace.h``.
Graph-specific traces and conversion live in ``IR/GVFG``.