 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.^[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.