CLI reference

This page is the canonical inventory of visao command-line options grouped by purpose. For tutorial-style guidance see Console mode (one-shot) and Server mode (long-lived).

The options below mirror the parser in frontend/common/InputHandler.hpp. The command visao --help prints the live set for your build. Some options appear when the build includes the matching feature.

Mode selectors

--server

Run as an analysis server. The positional file list becomes the list of bind URLs. You can repeat the flag. Example URLs: tcp://127.0.0.1:5500 and ipc:///tmp/visao.sock. Console mode ignores the server options below.

No flag

One-shot console mode. This is the default.

Inputs

<file> ... (positional)

Analyse these files. On Windows, put -- before the list to separate it from the option flags. The tool reads a single compile_commands.json as a compile database.

-I <path>, --iquote <path>

Add a regular header search directory (#include "...").

--isystem <path>

Add a system header search directory (#include <...>).

--include <header>

Force-include an extra header.

-D <NAME[=VALUE]>, --def <NAME[=VALUE]>

Add a preprocessor definition.

Language and toolchain

--language <id>

Target language. One of: c, cpp, go, python, rust, javascript, typescript, java, kotlin, csharp, ruby, php, swift, lua, delphi, cmake, bash, yaml.

--std <name>

Language standard (c11, c17, gnu++20, …). If omitted, the toolchain probe decides.

--cpu <name>

Target CPU (x86, x86_64, arm, arm64, mips, mipsel, custom).

--os <name>

Target OS (linux, macos, windows, baremetal).

--compiler <name>

Wide compiler name to match (clang, clang++, gcc, g++, clang-cl, go).

--toolchain <name>

Pick a probed toolchain directly (overrides --cpu / --compiler).

--compiler-path <spec>

Register a compiler outside the default search paths. Format <wide-name>:<path>, for example gcc:/opt/arm/bin/arm-none-eabi-gcc.

--compiler-wrapper <name>

Invoke the compiler through a wrapper. Supported: docker.

--update-toolchains

Discard the on-disk cache and reprobe.

--winkit <path>, --vctools <path>

Windows-only paths for the Windows Kit and Visual C++ tools.

Output and presentation

-v, --verbose {critical,error,info,debug}

Engine log verbosity. Default info.

--color {auto,always,never}

Colour output mode. auto honours isatty + NO_COLOR + VISAO_DISABLE_COLORS; always/never override unconditionally.

--no-color

Alias for --color never.

--locale {en-US,ru-RU}

Language of defect messages.

Defect filtering

--severity {Paranoid,Low,Medium,High}

Minimum severity to surface. Default: Low.

--duplicate-results

Keep duplicate findings instead of collapsing them.

--ignore-missing-headers

Do not fail when #include cannot be resolved.

--verify-function <name>

Restrict analysis to the named function(s). Repeatable.

Suspicious places

A second kind of output lists the places that a reviewer reads. Visao classifies each place and prints it with its code. Suspicions never influence --fail-on. Full description in Suspicious places.

--suspicious

Report suspicious places alongside the findings.

--suspicious-only

Report suspicious places and no findings.

--suspicious-all

Include low confidence, which is inventory rather than signal.

--suspicious-categories <a,b,...>

Restrict to these categories: copy-paste, inconsistency, complexity, naming, magic-value, error-handling, boundary, dead-ish, concurrency, api-shape, type-mixing, todo, security.

--suspicious-output <file>

Write them as JSON.

--suspicious-context <N>

Lines of code printed around each one. Default: 2.

Job selection

Default: --defects. If you ask for any other job, defects are silently disabled unless re-enabled.

--defects / --disable-defects

Main defect detector.

--dependency

Dependency analysis. Combine with the --dep-graph-out* options below.

--identify

Language identification.

Workspace and scoping

-j <N>, --jobs <N>

Worker threads for per-WorkspaceJob parallel analysis. 0 = auto-detect (hardware concurrency); 1 (default) keeps the analyzer single-threaded.

--whole-project

Treat all inputs as a single TU group.

--one-toolchain

Force a single toolchain for the whole job batch (useful with mixed compile-DB entries).

-z <file>, --zone <file>

Load a zone file (analysis scoping / partitioning). Repeatable.

-f <glob>, --filter <glob>

Restrict the analysed set to files matching the pattern. Repeatable.

In addition, inside the positional file list, items prefixed with filter:<glob> add a filter pattern, and compiler_path:<spec> adds a compiler binding. These two prefixes are stripped before the rest of the string is interpreted.

Dependency graph output

Only meaningful with --dependency.

--dep-graph-out <file.dot>

Write the Graphviz source.

--dep-graph-out-png <file.png>

Render through dot (must be on PATH). Use the <tag> placeholder to emit one PNG per zone.

Analysis solver tuning

--solver-fallback {z3,cvc5,z3-spacer,cvc5-chc,off}

SMT solver fallback used when the AI domains cannot decide a check. The default is auto. Visao takes the solver that the build includes, and it prefers Z3. The fallback engages without a flag. Pass off to disable it. The option acts when the build includes the selected backend (VISAO_ENABLE_Z3 / VISAO_ENABLE_CVC5 at cmake configure time). z3-spacer routes through Z3’s Spacer Horn-clause engine, and cvc5-chc routes through CVC5’s HORN logic. Both engines ship inside the standard solver binaries, so they work without a rebuild.

--chc-program

Enable the program-as-Horn-clauses encoder pass. The pass walks each function’s IR after the AI analysis and feeds the system to Z3 Spacer for invariant synthesis. It requires VISAO_ENABLE_Z3, and it is off by default. The encoder covers straight-line code.

--function-timeout <SECONDS>

Time limit for the analysis of one function. The limit applies to each of the two phases: the model and the checks. When a function goes over the limit, Visao writes a warning and gives no findings for that function. The analysis of the other functions continues. The default is 300. 0 removes the limit.

--report-proved

Emit [verdict] Proved (path-implied) lines on stderr for each predicate the SMT fallback proves valid. Side-channel for verdict-comparison use (for example against Frama-C WP); requires --solver-fallback.

CI integration and reporting

--report-format {text,sarif,json,gitlab}

Machine-readable report. text (default) is the human console rendering. sarif is SARIF 2.1.0 for GitHub Code Scanning, Jenkins Warnings NG and Azure DevOps. json is the compact Visao findings array, and gitlab is the GitLab SAST report. For a non-text format without --report-output, the document goes to stdout, and Visao holds back the human rendering.

--report-output <file>

Write the report document to a file instead of stdout; the human console rendering is kept alongside.

--report-uri-base <dir>

Prefix stripped from every file path in the report so locations become repo-relative. Set it to the checkout root (for example $GITHUB_WORKSPACE) so inline annotations anchor even when inputs carry absolute paths.

--fail-on {none,paranoid,low,medium,high,critical}

Exit non-zero when at least one surviving finding meets or exceeds this severity. Default none preserves the historical always-0 exit code.

--baseline <file.sarif>

Path to a baseline SARIF document. Visao matches findings against it by rule id, file and message, and it ignores line shifts. A matched finding leaves the report and the --fail-on gate, so new findings surface alone. A missing file suppresses nothing.

--baseline-write

Instead of filtering, write the current full finding set as SARIF to the --baseline path (create or refresh the snapshot) and skip gating. Requires --baseline.

SBOM generation

--sbom-output <file>

Walk the input project root for package manifests (Cargo.toml, package.json, requirements.txt, go.mod, vcpkg.json, boss.json), extract declared dependencies, and emit the SBOM to this file.

--sbom-root <dir>

Directory to scan for manifests. Defaults to the directory of the first analysed input.

--sbom-format {cyclonedx,spdx}

Output format. cyclonedx (default) is CycloneDX 1.5 JSON; spdx is SPDX 2.3 JSON.

--sbom-vuln-db <path>

OSV vulnerability database: a single JSON file (one record or an array) or a directory of *.json files. Matching advisories are attached as CycloneDX vulnerabilities[] entries.

--sbom-license-policy <file>

License-policy file. One directive per line: allow <SPDX> or deny <SPDX>; # starts a comment. Any allow entry switches the policy to whitelist mode. Packages with empty license never trip the policy.

--sbom-diff <file>

Path to a previous CycloneDX/SPDX SBOM. After writing the current SBOM, Visao reports added / removed / version-bumped packages on stderr.

--sbom-diff-output <file>

Write the diff as JSON. Requires --sbom-diff.

Cross-project analysis

--xproj

Enable cross-project symbol indexing. Heterogeneous WorkspaceJobs accumulate exported function symbols into a shared XProjectIndex. One invocation holds C, Rust and Go source trees together. The AI and CHC analyses then resolve calls that cross language boundaries through FFI.

Server tuning

Only applies in --server mode.

--server-max-analyses <N>

Concurrent analysis cap. 0 = unlimited.

--server-response-tick-ms <N>

ResponseSender drain interval. Default 5 ms.

--server-log-traffic

Log every Request and Response.

--server-graceful / --server-no-graceful

Drain inboxes and join threads on SIGINT/SIGTERM. Default: graceful.

--enable-database

Store analysis results in MongoDB (requires an ENABLE_DAL build).

Debugging

--redirect<context> <file>

Redirect a named debug stream to a file. One option is generated per registered DebugContext; run visao --help to see the contexts available in your build.

Environment variables

NO_COLOR

Disable colours (any value).

VISAO_DISABLE_COLORS=y

Same, legacy variant.

VISAO_DETAILED_TOOLCHAIN=y

Verbose toolchain probing diagnostics.

VISAO_ABORT_ON_FAILURE=y

Abort on assertion failures rather than continuing.

VISAO_OPENVEF_WIN32=y

Internal hint used by the OpenVEF test use on Windows.

Exit code

Without --fail-on the exit code is always 0; pass/fail is communicated through output content (presence of Finished successfully / Failed to parse some files markers, plus the per-report error: lines). With --fail-on <severity> the process exits 1 when at least one surviving finding meets or exceeds that severity, and 0 otherwise.

With --trace, the process exits 3 when the build exits with a non-zero code. Visao still analyses the files that the build compiled before it stopped.