= Static program analysis
<Static program analysis> derives information about a <computer program> from its representation and <programming language semantics>, without executing each concrete input case. An analysis commonly approximates many possible executions at once. <Data-flow analysis> propagates such information between locations in a <control-flow graph>.<Data flow analysis: an informal introduction in the Clang documentation>[Introduction, symbolic values and joins]{ref}
For example, after `if c then x=1 else x=2`, an analysis can infer that `x` belongs to $\{1,2\}$ at the join and hence is nonzero. More complicated paths may force a less precise answer. A conservative warning can therefore flag a possible failure that no actual input reaches. The guarantee depends on what the approximation includes: failing to model an external call or <integer overflow> can invalidate an apparent proof.
Back to article page
