#LunaFlow

#Features

• A funnel, not a mode switch
  --level 1|2|3 is cumulative and --funnel runs all three. L1 deduplicates its findings, L2 splits its results into confirmed and new, and L3 is applied only to functions with an L1/L2 finding plus every function that already carries a contract. Functions escalated without a contract are reported as specification gaps — the funnel's explicit to-do list. When a target has no annotations, L3 reports 0 VCs and the gaps, not invented proofs.

• A control-flow graph you can argue with
  The CFG is built from the parsed statement tree: branch nodes with true and false edges, loop heads with back edges, merge points, and dead nodes for statements after an unconditional exit. Execution paths come from the trace and are rendered beside the diagram. Dead code and unreachable nodes are static findings; non-termination is a static + dynamic finding; path coverage is dynamic and exact only for the executed trials. Each finding carries its method and confidence.

• Taint with stated rules
  Sources are entry-function parameters (and @env.args when the frontend sees it). Propagation follows recorded definitions and the variables each statement read; array reads inherit container taint; length() inherits receiver taint; a tainted loop condition taints the numeric loop counters (implicit flow). Sinks are array indices and allocation sizes. The rules and their imprecision — field- and index-insensitive, no alias analysis, depth-6 calls, unsupported match arms — are printed in every report.

• Values at every point
  L1 records every def event keyed by function, source line and variable, so report §6.1 is a per-program-point value table and the JSONL trace has the full stream. L2 adds may-ranges from the abstract fixpoint. The distinction is explicit: observed samples are not a proof, and the abstract interval is an over-approximation at widening.

• Slices over the trace
  The dynamic dependence graph is built from def/cond/index/call events. Backward slicing walks to sources, forward slicing walks to sinks and returns. Criteria are <var>@<fn>, <fn>:<line> or a bare <var>. A slice is exact for the recorded trace, not a static closure; --function ensures the target function is executed before slicing.

• Contracts that admit ignorance
  Specifications are MoonBit comments: //@ requires, //@ ensures, //@ invariant, //@ assigns. L3 generates WP-style verification conditions for index bounds, allocation sizes, division, assertions and postconditions at every return and tail expression. Each VC is proved, failed or unknown; unknown is an honest third state, not a failure. This is a three-state interval prover, not an SMT-backed WP.

• Finding families that state their own limits
  Every finding kind has a code (DEAD-CODE, TAINT-INDEX, …) and a contract: the property it asserts, the assumption under which that is sound, and what it does not cover. --explain-all prints the roster, --explain <code> prints one contract, and --families / --exclude-families select by code. --metrics prints the ADEQUACY block — what was read, what was understood, what was entered, what was found — and every line in it carries its own coverage.

• An evolved value analysis, and the memory-safety classes it reaches
  The value analysis asks what a value's range is; the evolved value analysis asks what happens when the value is used. It finds the index that escapes its array, the divisor that may be zero, the integer operation that leaves its type's range, the Option that may be None where it is unwrapped, the element read before it was written, and the conversion that saturates silently. Each class was mapped onto what MoonBit actually does by running the real toolchain — and MoonBit's integer arithmetic wraps instead of trapping, so an overflow there is a silent wrong value rather than a crash. The classes MoonBit's type system makes impossible — use after free, pointer arithmetic, memory leaks, format strings — are in the roster as RESERVED families whose contracts say why they never fire.

• A memory layout model, in the terms the language actually has
  MoonBit has no addresses: no pointer type, no address space, no size_of, and the byte order is spelled out in the API rather than inherited from the machine. So the model is not a smaller hardware model — it is the placement question. The global region is evaluated once, in dependency order, because MoonBit resolves top-level bindings by dependency and not by file order. Every allocation site is classified as global, frame, heap or foreign by a static escape analysis, so the answer does not depend on which inputs a run sampled. And --stability re-samples the analysis and says, row by row, which findings depend on the sample — the abstract ones do not, and the observed ones do, and the report says so instead of letting a reader assume otherwise.

• A foreign address space, and the isolation between the two
  The C boundary is where an address appears, and it appears on the other side of it: MoonBit has no pointer type, so the foreign address space is not something the language has. The analyzer therefore models two spaces — the MoonBit one and the foreign one — and says, per parameter and per return value, which side it lands on: a value is copied, a heap pointer is the address of a MoonBit object, and an #external type is an address the C side owns. The set of pointer types is not guessed; it is the set the toolchain's own ownership diagnostic fires for, measured one type at a time. Six families then report what the boundary costs — a C symbol declared with two signatures, an object given away and then used, a calling convention that relies on a default the toolchain says will change, a declaration the published target cannot build, an address that cannot be named, and a constant that reaches two different C symbols. The first two are defects the compiler does not catch, and both were confirmed against the real toolchain.

• Markdown is the UI
  Reports use flowchart TD for CFGs and slices, flowchart LR for taint and the funnel. Labels are sanitized, node counts are capped (8 CFGs, 90 nodes per diagram, 40 taint/slice nodes), and every node and table row carries a file:line. The artifacts are diff-friendly and render on GitHub, GitLab and VS Code.

• Version pinning you can reproduce
  A bare coordinate or @latest is resolved once by moon fetch, then pinned: the report records the resolved version, the source root (.repos/<author>/<module>/<version>) and the declared target. The analyzer never compiles the target, so heavy modules are analyzable without their dependencies. The optional Cobertura bridge is the only path that needs a buildable target.

#What you get

#Install

moon add riantr/LunaFlow@0.1.14

import {
  "riantr/LunaFlow@0.1.14",
}

///|
import {
  "riantr/LunaFlow/src/app",
}

Cannot find import 'riantr/LunaFlow/src/app@0.1.0' in my/app/src/thing@0.1.0

///|
import {
  "riantr/LunaFlow/src/app" @lf,
}

moon run src/cli -- analyze <author>/<module>[@<version>|@latest]

moonx riantr/LunaFlow@latest riantr/LunaFlow@latest

moonx riantr/LunaFlow@latest riantr/LunaFlow@latest   # the bare coordinate IS the target
moon run src/cli -- riantr/LunaFlow@latest              # the same thing, locally
moonx riantr/LunaFlow@latest .                         # a path IS the target too
moonx riantr/LunaFlow@latest                            # no target at all: the current directory

#What the release was checked on

moon run . --target wasm -- analyze riantr/moonbit_static_analysis@latest --out reports

Error: [4021] Value run_async_main not found in package `moonbitlang/core/async`.

#The host contract

#The core compatibility contract

Error: [4014]
  ╭─[ src/app/scan.mbt:284:12 ]
 284 │     stdout=@process.read_from_process(),
    │            ──────────────┬─────────────
    │                          ╰─────────────── Expr Type Mismatch
       has type : (ReadFromProcess, SharedProcessOutput)
       wanted   : ProcessOutput

• the fetch runs moon fetch --quiet, so it prints nothing on success and its error reaches the user directly;
• the version comes from the directories the fetch wrote, not from parsing a log;
• the child inherits the parent's streams, so nothing has to be captured.

#What changed in 0.1.14

LunaFlow analyze riantr/LunaFlow@latest@latest --out reports/ --funnel

Error: Invalid package coordinate `riantr/LunaFlow@latest@latest`
Caused by:
    must contain a single version marker

#What changed in 0.1.13

#What changed in 0.1.12

let derived : Int32 = base + 2   // reads a global declared LATER
let base : Int32 = 10

#What changed in 0.1.11

#What changed in 0.1.10

USE-AFTER-FREE  UseAfterFree

  property    a value may be used after the storage it referred to was released

  assumption  NOT APPLICABLE IN MOONBIT: safe MoonBit has no raw pointers, the
              collector owns the storage, and values are immutable -- there is
              nothing to free and nothing to dangle

  excluded    nothing -- and note the kind is RESERVED: safe MoonBit cannot
              express the defect

let mut x : Int32? = None
if flag { x = Some(1) } else { x = Some(2) }
x.unwrap()

#What changed in 0.1.9

moonx riantr/LunaFlow@latest --explain-all

families: code, title, and the property each one asserts

  DEAD-CODE  DeadCode  --  a statement is unreachable after an unconditional exit
  UNREACHABLE  Unreachable  --  no execution reaches this statement: the flow arriving at it has already left the block
  INFINITE-LOOP  InfiniteLoop  --  the loop cannot terminate: its condition holds for every input and it has no break
  TAINT-INDEX  TaintedIndex  --  a tainted value may reach an array index or a buffer offset
  TAINT-INDEX-RANGE  TaintedIndexInRange  --  a tainted value reaches an index that is in range on every observed path
  TAINT-ALLOC  TaintedAllocation  --  a tainted value may control an allocation size
  RANGE-VIOLATION  RangeViolation  --  a value's range may be violated: an assertion may fail, or a size may be negative
  PARSE-GAP  ParseGap  --  a construct the frontend could not model, folded into the statement it belongs to
  BUDGET-EXCEEDED  BudgetExceeded  --  an analysis budget was exhausted, so the rest of the function was not analysed
  UNSUPPORTED  UnsupportedSink  --  a tainted value may reach abort/panic

moonx riantr/LunaFlow@latest --explain TAINT-INDEX

TAINT-INDEX  TaintedIndex

  property    a tainted value may reach an array index or a buffer offset

  assumption  the taint source set was complete, and the sink was reached on an observed path

  excluded    an index the runtime clamps, and a value the source model did not mark tainted

WARNING	unknown family code in --exclude-families: TAINT-* (the roster is DEAD-CODE, UNREACHABLE, ...)

ERROR	the profile includes and excludes the same family code: DEAD-CODE

METRICS	read	files=1	parsed=1	partial=0	understood=100.0%
METRICS	stmts	statements=32	understood=32	unsupported=0	understood-share=100.0%
METRICS	funcs	functions=12	entered=12	skipped=0	entered-share=100.0%
METRICS	findings	total=12	error=6	warning=2	info=4

#What changed in 0.1.8

moonx riantr/LunaFlow@latest .                          # the current directory
moonx riantr/LunaFlow@latest ./src/app                  # a tree, where it stands
moonx riantr/LunaFlow@latest riantr/LunaFlow@latest      # a coordinate, fetched
moonx riantr/LunaFlow@latest                             # no target: the current directory

#What changed in 0.1.7

• The filesystem and process calls sit behind #cfg guards now. There are 13 such call sites, in two files: ten in src/app/scan.mbt and three in src/command/command.mbt. Each one moves into a guarded declaration with a stub for the backends that have no filesystem, because #cfg guards declarations — a statement inside a function body cannot be guarded, so the @fs.mkdir call had to move into a helper of its own. The counters moved into ScanStats::add_file for the same reason: left in the caller, the mut fields would be unused on js and the compiler would reject the build.
• On Node, the command line arrives one element later. env.args() is process.argv there, so the node executable AND the script path come first: [node, script.js, "analyze", ...] where every other backend gives [exe, "analyze", ...]. The CLI read args[1] as the command, so on js it read the script path and printed the usage text instead of analysing. It is one helper now, and it is the only js-specific line in the source.

Error: [4021] Value run_async_main not found in package `moonbitlang/core/async`.

#What changed in 0.1.6

• A contract clause carried the wrong line. parse_spec_expr took a line and never used it. A clause is parsed out of ONE line of a file, so every contract expression claimed to be on line 1 of the file — and a reader who followed the pointer landed on the top of the file. The lexer now takes the base line (lex_at), and each clause of a contract carries the line it was actually written on.
• Two unread bindings. The if expression read its condition and its then-block into two locals it never used. They are discarded explicitly now; the parse is unchanged.

• A slice a[i:j] was not modelled. return line[i + 1:j].to_string() became a return with an unmodelled expression plus three shredded fragments, and the fragments that followed the exit inherited its deadness. Slices are modelled now (ESlice), and because a slice is clamped by the runtime it carries the taint of its parts but raises no out-of-bounds claim.
• A while true whose body holds a construct the parser does not model was called infinite. The break inside such a construct is invisible to the CFG, so the loop looked non-terminating and the code after it looked dead. The analyzer now claims only what it can support: a loop with an unmodelled construct in its body is not proven infinite, and the code after it is not proven unreachable. A fully modelled while true is still reported — refusing to guess must not cost the real finding.

• A MoonBit multiline string (#|) was lexed as a string that ended at the end of its first line. The construct is a string literal, not a comment: #| opens it, the text after the marker is the first chunk, every following line whose first non-blank characters are #| is one more chunk, and the value is the chunks joined with "\n". The old lexer took the rest of the first line and left the rest of the literal in the token stream, so usage() was shredded into thirty-odd statements, the function was not recognised as a function at all, and the statements around it were counted as unsupported. The literal is modelled now, and so is the newline that ends its last chunk line: without that newline the statement after the literal was parsed as part of it, which is how one let in a test file became one unsupported statement instead of three understood ones.

#What changed in 0.1.5

• Seven root causes, all in the frontend. A struct literal was not modelled, so { a: x, b: 2, } became one statement per field — and it ate the enclosing block's closing brace, which truncated the function. A binary expression did not continue across a newline. A match expression leaked its arms. :: was lexed but not parsed, so return CART::Leaf(...) left its tail behind. A string or character literal whose content was { was counted as a brace, and the block ran on past the end of the function, taking the functions after it with it. A for that destructures left its loop body behind as a block. And an if without an else was treated as an unconditional exit, so the code after a guarded return was called unreachable.
• The repair is two layers. The constructs above are now modelled — the qualified path, the qualified record literal, the destructuring for, the named argument, the if expression, the function literal. And the parser no longer lets an unmodelled construct shred itself: a tail it has no rule for is folded into the statement it belongs to and counted as unsupported. The second layer generalises — without it the next construct the parser does not know would shred itself again.
• Taint sinks are deduplicated by site, not by whole-finding equality; the observed value is in the evidence, so one read observed in many trials became dozens of rows. And a tainted index whose observed value was inside the array is now a warning that says so; only an index witnessed out of range, or one whose bounds cannot be resolved, stays an error.
• "No findings" no longer reads as "clean". The CFG pass covers the first 600 functions in file order, so the rest of a large module can carry no CFG finding. The report now says so in its ingestion table, and --max-cfg-functions makes the window configurable.

#What changed in 0.1.4

• The runtime comes from the toolchain. The dependency on moonbitlang/async is gone; the async runtime is moonbitlang/core/async, part of the moonbitlang/core module the toolchain already bundles. moon.mod has no import block any more. The trade is stated above: the package is experimental, and the minimum host toolchain moved up, because the artifact asks the host for a bigger set of symbols than the standalone module provided. The set is measured, not asserted — 108 host imports, 107 of them covered by the bundled core, and the contract is in docs/host_requirements.txt.
• The module has a root package, and moonx runs it. moonx riantr/LunaFlow@latest riantr/LunaFlow@latest is the self-check, and it works. That needed three things: a root package that is an executable (without one, moonx says "Prebuilt wasm asset does not exist"), a wasm artifact for the registry to publish (preferred_target = "wasm"), and a CLI that treats a bare coordinate as an implicit analyze.
• The module builds and runs for wasm, and the library also builds for js. supported_targets is +native+wasm+js, and the wasm artifact fetches, analyses and writes the report. The js build is real — the library is checked and its 73 tests run there — but it has no filesystem, so the js library is what gains: text in, analysis out. wasm-gc is still excluded, and the reason is upstream's — see The host contract.
• The fetch log is gone, and with it a whole class of bug. The version used to be scanned out of the moon fetch log — free-form text whose shape differs between platforms. It is now taken from the directories the fetch wrote. The log scan was the source of two separate defects (a garbage version on the Linux runner, a green run over an empty tree; a version of "." on Windows), and removing it removes both by construction. The Windows case is the sharper one: the fetch log prints the resolved path, and when the module name is a SUFFIX of the repository directory name — moonbit_LunaFlow for the module LunaFlow — the text after the name starts with \.repos\. A dot is a version character, so the token came out as ".". That candidate was then accepted because base + "/." exists: it resolves to the base directory itself. Analysing the module with itself therefore pinned the analysis to the BASE directory, and the report claimed the resolved version was ".".
• The module builds against every core a user may have. The runtime comes from the toolchain, so the core's API is allowed to change shape between toolchains — and it did, between core 0.10.19 and 0.10.20, in the middle of this release. The details are under The core compatibility contract; the short version is that the fetch no longer captures the child's output, so it uses only the API that is the same in both, and scripts/qa/core_compat.mjs checks the rest.

#What changed in 0.1.1

#What changed in 0.1.0

• A hostile module could abort the process. 5,000 nested if statements and 2,000 nested parentheses exhausted the native stack (0xC0000409, STATUS_STACK_BUFFER_OVERRUN). The parser now refuses constructs nested deeper than 256 levels and records them as a parse gap instead: the region is skipped whole and counted as one unsupported statement, so the frontend-coverage number in the report stays honest rather than reading 100 % on a file that was skipped. This is pinned by hardening_test.mbt and by scripts/qa/depth_sweep.mjs.
• A hostile module could steer the report path. The output file name is built from the analysed module's own moon.mod, and only / was neutralised, so a version field of ..\..\..\..\escaped wrote the report, the trace and the summary into an arbitrary directory. The stem now goes through a whitelist sanitiser, and scripts/qa/path_traversal.mjs is the regression.
• A --dir scan could describe someone else's code. The source walker skipped _build, .git, .repos, target and node_modules, but not .mooncakes — the directory the toolchain vendors a module's dependencies into. A self-scan of this repository therefore reported 384 parsed files, 362 of them from the vendored moonbitlang/async module: every file, function and statement count in that report described a third party's code. .mooncakes is skipped as well now, and scripts/qa/vendor_isolation.mjs plants one file behind every skipped directory name and asserts that exactly the module's own source is parsed.

• The version was scanned out of the moon fetch log, which is free-form text whose shape differs between platforms. On Linux the scan took everything up to the next " to " and produced the version 0.164.64\nSuccess\nSuccessfully fetched … — a name that matches no directory. The analyzer then read an empty tree and reported 0 statements, 0 coverage, 0 findings, exit 0. The filesystem is now the authority: the version is cut at the first character that cannot be part of a version, and a candidate is only accepted when the directory it names really exists.
• The harness looked for the built CLI under the wrong name. The MoonBit native target names the executable cli.exe on every platform, Linux included, where the file is an ELF binary with a Windows extension. The resolver picked the name by platform, so on the runner the CLI never ran and the failure surfaced three steps later as a missing output file.
• The vendored-tree regression asserted the wrong thing. It checked that the report does not contain the string _build/, but the report records the analysed root and the harness's scratch directory lives under _build/. It now asserts on ingested content — a foreign file name and a foreign function — and it was checked against a reverted fix to prove it can go red.

#Packages and targets

#Layout

LunaFlow.png               the mark this README shows
LunaFlow_Logo.png          the same artwork at 1024x1024
LICENSE                    MIT
moon.mod                   module metadata (native, wasm and js)
moon.pkg                    the ROOT package: the executable moonx resolves
main.mbt                    the root entrypoint, a forwarder to src/command
src/app/                   18 library files: parser, CFG, L1 interpreter,
                           L2 abstract interpreter, L3 contracts, funnel,
                           taint/slice, family roster, evolved value
                           analysis, memory layout model, foreign address
                           space model, report renderer
src/app/*_test.mbt         134 tests in 14 files
src/command/                the CLI implementation, as a library
src/cli/main.mbt           the published CLI entrypoint
fixtures/vuln_demo/        taint / dead-code / infinite-loop / contract fixture
fixtures/eva_demo/         the evolved value analysis fixture: the defect
                           classes and the ordinary shapes next to them
fixtures/memory_demo/      the memory layout fixture: the global region, the
                           allocation classes and the tail value
fixtures/ffi_demo/         the foreign address space fixture: the C boundary,
                           the ownership contract and the named addresses
features/                  acceptance scenarios in Gherkin
docs/design.md             design, comparison, acceptance criteria (A1-A18)
docs/qa/REPORT.md          deep QA report (security, coverage, metrics)
docs/host_requirements.txt  the published wasm's host contract, measured
reports/                   generated reports for the validation modules
scripts/verify.mjs         dependency-free acceptance checker
scripts/qa/                dependency-free QA harnesses

#Verification

moon run src/cli --target native -- analyze --dir fixtures/vuln_demo \
  --out reports --funnel --trials 4 --max-functions 120 --slice "i@copy_prefix"
moon run src/cli --target native -- analyze riantr/moonbit_static_analysis@latest \
  --out reports --funnel --trials 4 --max-functions 120 --slice "buf@render_reports"
moon run src/cli --target native -- analyze riantr/moonbit_doubleML@latest \
  --out reports --funnel --trials 4 --max-functions 120 --slice "theta_hat@aggregate_coef_se"

#The cross-check against another analyzer's module

1. A struct literal was not modelled, so { a: x, b: 2, } became one statement per fragment, and it ate the enclosing block's closing brace — which truncated the function.
2. A binary expression did not continue across a newline, so each continuation line became its own statement.
3. A match expression leaked its arms into the enclosing statement list.
4. :: was lexed but not parsed, so return CART::Leaf(...) left the tail behind as statements. :: is not a list-cons operator in MoonBit — 1 :: [2] is a parse error in the real toolchain — so it is only ever a qualified path.
5. A string or character literal whose content was { was counted as a brace. match rsplit_at(seg, "{") { stopped the arm scanner at the string, the block ran on past the end of the function, and the functions after it were lost.

#What this is not

• Not sound. L1 reports what happened on synthesized inputs. L2 reports what the abstract input set cannot exclude. L3 proves individual VCs from specifications. Absence of a finding is never a proof.
• Not a full MoonBit frontend. Unsupported syntax is measured and reported (1.06 % of statements on doubleML, 4.39 % on static_analysis). Expression and statement nesting beyond 256 levels is refused as a recorded parse gap rather than risked on the native stack.
• Not alias-aware. Taint is field- and index-insensitive, with a depth-6 interprocedural cutoff; loop-counter implicit taint is deliberately conservative and can over-report.
• Not trace-complete. Slices and ranges cover the recorded trace only. Function names are not package-qualified, so a name-only criterion can match several packages (three packages define render_reports in static_analysis).
• Not SMT-backed. L3 is a WP-style VC generator with an interval decision procedure. Loop invariants are not yet placed per loop, so loop-dependent goals are havocked to unknown. The //@ syntax is ACSL-inspired but adapted to MoonBit comments; ACSL itself targets C.
• Not a database. Reports, traces and summaries are plain files: diffable, human-readable, reproducible. riantr/tesseract was evaluated as a storage dependency — 0.1.17 raises the durable-memory ceiling to 9999 entries, but its dependency footprint is ~28 MB, so it is not adopted. If cross-run queries are needed, an optional SQLite sidecar is the smaller change.

#Quick Start

# analyze a published module; @latest is resolved once and pinned
moon run src/cli --target native -- analyze riantr/moonbit_doubleML@latest --out reports

# the full funnel, with a slice on a variable
moon run src/cli --target native -- analyze riantr/moonbit_doubleML@latest \
  --out reports --funnel --slice "theta_hat@aggregate_coef_se"

# a local checkout, no registry resolution
moon run src/cli --target native -- analyze --dir fixtures/vuln_demo \
  --out reports --funnel --slice "i@copy_prefix"

# focus on one function in a large module
moon run src/cli --target native -- analyze riantr/moonbit_static_analysis@latest \
  --function render_reports --slice "buf@render_reports" --out reports

# compiled coverage, when the target builds
moon coverage analyze
moon coverage report -f cobertura -o cov.xml
moon run src/cli --target native -- analyze <coord> --coverage cov.xml --out reports

moonx riantr/LunaFlow@latest riantr/LunaFlow@latest

#Example

L1 concrete: 12 findings
L2 abstract: 11 findings, 4 new
L3 contracts: 2 proved / 1 failed / 3 unknown

flowchart LR
  L1["L1 concrete: 12 findings"] -->|"dedup, escalate"| L2["L2 abstract: 11 findings, 4 new"]
  L2 -->|"critical functions"| L3["L3 contracts: 2 proved / 1 failed / 3 unknown"]

#Gates and drift detectors

• moon test pins the fixture's static findings: 3 dead, 1 unreachable, 1 infinite loop, and the L3 proved/failed/unknown split.
• scripts/verify.mjs fails on missing sections, invalid Mermaid structure, empty slices, missing L2/L3 counters, coverage below 95 %, or a runtime above 60 s.
• scripts/qa/gherkin.mjs states the acceptance criteria as executable scenarios, including the two hostile-input regressions.
• docs/design.md §10 lists the quantified acceptance table (A1–A18); the measured column is updated from real runs, not from intent.
• Determinism: two runs produce identical summary.json except elapsed_ms, and a byte-identical trace.

#Used By

• src/cli — the executable in this module, the command line over the same library.
• src/command — the CLI implementation, shared by src/cli and the root package that moonx resolves.
• scripts/qa/ — twenty dependency-free harnesses and tools; thirteen of them drive the built binary as a real process against the fixture, the two registry modules and a hostile-input corpus.
• docs/design.md — the design record for the implementation in src/app.

#Attribution

• License: MIT (see LICENSE).
• The documentation layout of this README follows the riantr/tesseract module, whose release notes are a model of stating exactly what changed and what did not.
• The comparison baseline in docs/design.md §8 covers Frama-C / TrustInSoft Analyzer, Joern, CodeQL, SVF and Soot. Every place this module answers differently from those tools is a stated limitation in What this is not, not an omission.