Sifa Tool

This page documents the sifa verifier front-end in tools/verifier/sifa/.

Binary: sifa

Source: tools/verifier/sifa/sifa.cpp

Overview

sifa analyzes a target function or block using the Sifa framework. It can run in a lightweight reachability mode, a native abstract-domain mode, or a SymAbs-backed SMT mode.

Basic usage

./build/bin/sifa input.bc
./build/bin/sifa input.bc --function=foo
./build/bin/sifa input.bc --function=foo --block=loop.header
./build/bin/sifa input.bc --symabs --abstract-domain=Octagon

Important options

  • --function=<name> selects the function to analyze. The default is main when available.

  • --block=<label> analyzes to a named block instead of the function return.

  • --abstract-domain=Interval|Octagon|both selects the abstract domain.

  • --symabs enables SMT-backed symbolic abstraction.

  • --represent-all includes unnamed SSA values in the printed invariant.

  • --widening-delay and --widening-frequency tune widening in SymAbs mode.

  • --reachability only reports whether the target is reachable.

  • --list-functions and --list-blocks inspect available analysis targets.

  • --log-level=none|error|warning|info|progress|debug|trace controls diagnostic output.

See also

  • See Sifa for the framework-level overview.