Coverage Analysis

ESBMC supports coverage analysis for branches, conditions, assertions, branches plus function entry, and bounded k-path. This helps identify which code paths have been exercised in your program.

Usage

ESBMC provides five primary coverage modes:

# Branch coverage
esbmc example.c --branch-coverage

# Condition coverage
esbmc example.c --condition-coverage

# Assertion coverage (use a sound unwinding strategy, e.g. k-induction)
esbmc example.c --k-induction --assertion-coverage

# Branch + function-entry coverage
esbmc example.c --branch-function-coverage

# K-path coverage (PathCrawler-style bounded path coverage)
esbmc example.c --k-path-coverage

Each mode also has a *-claims variant that lists every reached witness with its source location (e.g. --branch-coverage-claims, --condition-coverage-claims, --assertion-coverage-claims, --branch-function-coverage-claims, --k-path-coverage-claims).

Coverage Modes

Branch Coverage

Branch coverage verifies that all branches of conditional statements are executed. For each if, else, while, or for statement, both the true and false branches must be covered.

Example:

int check_sign(int n) {
    if (n > 0)
        return 1;
    else
        return -1;
}

int main() {
    check_sign(5);   // Only covers true branch
    return 0;
}

$ esbmc example.c --branch-coverage
...
[Coverage]

Branches : 2
Reached : 1
Branch Coverage: 50%

The Branch Coverage: 50% shows incomplete coverage. The output indicates that n <= 0 is needed to cover the else branch.

Full coverage example:

int main() {
    check_sign(5);    // Covers true branch
    check_sign(-3);   // Covers false branch
    return 0;
}

$ esbmc example.c --branch-coverage
...
[Coverage]

Branches : 2
Reached : 2
Branch Coverage: 100%

The Branch Coverage: 100% indicates all branches have been tested.

Listing reached branches. Add --branch-coverage-claims to print each reached branch guard with its source location alongside the summary.

Condition Coverage

Condition coverage verifies that each boolean sub-expression in conditional statements evaluates to both true and false at least once. Unlike branch coverage, which tests branches, condition coverage tests individual conditions within complex expressions.

Example:

int validate(int x, int y) {
    if (x > 0 && y > 0)  // Complex condition
        return 1;
    else
        return 0;
}

int main() {
    validate(5, 3);
    return 0;
}

$ esbmc example.c --condition-coverage
...
[Coverage]

Reached Conditions:  4
Short Circuited Conditions:  0
Total Conditions:  4

Condition Properties - SATISFIED:  2
Condition Properties - UNSATISFIED:  2

Condition Coverage: 50%

The Condition Coverage: 50% shows that only the true cases of both conditions were tested. For full condition coverage, each condition must evaluate to both true and false at least once:

• x > 0 must be true (✓ tested) and false (✗ not tested)
• y > 0 must be true (✓ tested) and false (✗ not tested)

Full coverage example:

int main() {
    validate(5, 3);    // x>0: T, y>0: T
    validate(5, -1);   // x>0: T, y>0: F
    validate(-1, -1);  // x>0: F (y>0 short-circuited)
    return 0;
}

Note: Due to short-circuit evaluation in &&, when x>0 is false, y>0 is never evaluated. To test y>0 as both true and false, x>0 must be true in those tests.

Listing reached sub-expressions. Add --condition-coverage-claims to print each condition with a per-polarity SATISFIED / UNSATISFIED verdict and its source location.

Disabling short-circuit handling. --condition-coverage-rm (and its claims-aware counterpart --condition-coverage-claims-rm) drop the short-circuit handling step. The metric then reports all sub-expressions independently of evaluation order — useful when contrasting MC/DC-style counts against the short-circuit-aware default.

Assertion Coverage

Assertion coverage verifies that all assertions in the code are reached. This ensures every validation check is exercised by some input.

Note. Use a sound unwinding strategy when running assertion coverage. The examples below pair --assertion-coverage with --k-induction so that all loop iterations are considered; bounded --unwind N works too, provided N is large enough for the program. With --k-induction, ESBMC prints a [Coverage] block per phase (base case, forward condition, inductive step); the final block is the verdict.

Example:

#include <assert.h>
int process(int n) {
    if (n > 10) {
        assert(n < 100);
        return n * 2;
    }
    else {
        assert(n < 10);
        return n + 2;
    }
    return n;
}

int main() {
    process(5);    // Covers second assertion
    return 0;
}

$ esbmc example.c --k-induction --assertion-coverage
...
[Coverage]

Total Asserts: 2
Total Assertion Instances: 2
Reached Assertion Instances: 1
Assertion Instances Coverage: 50%

Full coverage example:

int main() {
    process(50);   // Covers first assertion
    process(5);    // Covers second assertion
    return 0;
}

$ esbmc example.c --k-induction --assertion-coverage
...
[Coverage]

Total Asserts: 2
Total Assertion Instances: 2
Reached Assertion Instances: 2
Assertion Instances Coverage: 100%

Listing reached assertions. Add --assertion-coverage-claims to print each reached assertion guard with its source location.

Branch + Function Entry Coverage

--branch-function-coverage extends branch coverage with a witness for every function entry point. The resulting percentage therefore exposes both unreached branches and entirely unreached functions — a common gap that plain branch coverage hides when a function is never called.

Example:

int helper(int n) {
    if (n > 0)
        return n;
    else
        return -n;
}

int unused(int n) {
    return n + 1;
}

int main() {
    helper(5);
    return 0;
}

$ esbmc example.c --branch-function-coverage
...
[Coverage]

Function Entry Points & Branches : 5
Reached : 3
Branch Coverage: 60%

The denominator is 5: three function entries (main, helper, unused — main counts because the entry-point itself is an instrumented witness) plus two branches inside helper. unused and the n <= 0 branch of helper remain unreached, giving 3/5 = 60%. Add --branch-function-coverage-claims to print which entries and branches were reached.

K-Path Coverage

K-path coverage is a PathCrawler-style bounded path-coverage criterion. At every conditional branch if (g) goto L, ESBMC emits a witness goal for each combination of the previous (n−1) prior branch directions and the current direction. Each goal is discharged by the same multi-property engine used for branch coverage: a SAT verdict marks the corresponding bounded path as reachable. The coverage percentage uses Marré-Bertolino spanning-set scoring (IEEE TSE 29(11), 2003) — both numerator and denominator restrict to maximal goals under the atom-multiset subsumption order, so subsumed shorter-prefix goals never inflate the score.

This sits between branch coverage (length-1 prefixes only) and full path enumeration (exponential in the number of branches). With n = 2 the metric is equivalent to boundary-interior coverage; larger n exposes correlations that branch coverage alone cannot distinguish.

Flags:

Example (loop body with one branch):

int main()
{
  int x;
  for (int i = 0; i < 3; i++)
  {
    if (x > 0)
      x = x - 1;
    else
      x = x + 1;
  }
  return x;
}

$ esbmc example.c --k-path-coverage=2 --unwind 4 --no-unwinding-assertions
...
[Coverage]
k-Path Witnesses : 6
Spanning Set : 4
Reached : 2
k-Path Coverage: 50%

Six witnesses are emitted (two length-1 at the loop-exit guard plus four length-2 at the inner branch) but only the four length-2 form the spanning set; the two length-1 are subsumed. Of those four maximal goals, two are structurally unreachable — you cannot be inside the loop body with the exit guard already true — so the spanning-set coverage is 2/4 = 50%. The 50% honestly reflects that the loop guard and x > 0 are correlated after entry, a relationship --branch-coverage cannot expose since each branch is reachable in isolation.

Phase-2 limitations. Subsumption uses structural multiset containment, which is a sound but not complete approximation: a reachable goal whose structural subsumer is unreachable will be dropped from the numerator alongside its subsumer, leaving the percentage too pessimistic in those cases. Implementation pruning also collects prior branch guards by linear walk over the goto program, which over-approximates the prefix when branches join, and witnesses whose post-simplification depth exceeds --k-path-witness-depth are dropped with no ghost-flag fallback yet. Proper CFG analysis and ghost-flag fallback are tracked under issue #4325.

References.

• Williams, Marre, Mouy, and Roger, PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis, EDCC 2005 — doi:10.1007/11408901_21.
• Holzer, Schallhart, Tautschnig, and Veith, FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement, CAV 2008 — doi:10.1007/978-3-540-70545-1_20.
• Huang, Meyer, and Weber, Loop Unrolling: Formal Definition and Application to Testing, ICTSS 2025 — doi:10.1007/978-3-032-05188-2_2.

Supported Languages

Coverage analysis is supported for:

• C - All C features supported by ESBMC
• C++ - All C++ features supported by ESBMC
• Python - Full Python frontend support
• Solidity - Full Solidity frontend support

Interpreting Coverage Results

The key output of coverage analysis is the coverage percentage shown in the [Coverage] section. This indicates what portion of your code paths have been exercised.

Coverage Statistics

ESBMC reports:

• Total elements: Number of branches/conditions/assertions in the code
• Reached elements: How many were covered by the test inputs
• Coverage percentage: (Reached / Total) × 100%

Understanding the Output

Coverage analysis uses verification internally to determine reachability. You may see VERIFICATION SUCCESSFUL or VERIFICATION FAILED in the output, but these are intermediate messages during coverage computation, not indicators of program correctness.

What matters: The coverage percentage (e.g., “Branch Coverage: 75%”) Less relevant: VERIFICATION status (just shows coverage tool operation)

Python Examples

Branch Coverage

def is_positive(n: int) -> int:
    if n > 0:
        return 1
    else:
        return 0

# Only covers positive branch
is_positive(10)

$ esbmc example.py --branch-coverage
...
[Coverage]

Branches : 2
Reached : 1
Branch Coverage: 50%

The Branch Coverage: 50% indicates incomplete coverage.

Condition Coverage

def check_range(x: int, y: int) -> int:
    if x > 0 and y > 0:
        return 1
    else:
        return 0

# Full condition coverage - accounting for short-circuit evaluation
check_range(5, 3)    # x>0: T, y>0: T
check_range(5, -1)   # x>0: T, y>0: F
check_range(-1, -1)  # x>0: F (y>0 short-circuited)

$ esbmc example.py --condition-coverage
...
[Coverage]

Reached Conditions:  4
Short Circuited Conditions:  0
Total Conditions:  4

Condition Properties - SATISFIED:  4
Condition Properties - UNSATISFIED:  0

Condition Coverage: 100%

The Condition Coverage: 100% indicates that each condition was tested with both true and false inputs.

Assertion Coverage

def validate_positive(n: int) -> int:
    assert n > 0, "n must be positive"
    return n * 2

validate_positive(5)

$ esbmc example.py --k-induction --assertion-coverage
...
[Coverage]

Total Asserts: 1
Total Assertion Instances: 1
Reached Assertion Instances: 1
Assertion Instances Coverage: 100%

Technical Notes

• Coverage analysis in ESBMC uses symbolic execution and SMT solving
• Unlike traditional testing tools, ESBMC determines path reachability and calculates exact coverage percentages
• All paths are explored automatically without manual test case writing
• Coverage analysis adds false assertions to test each branch/condition
• Verification time increases with code complexity

Combining with Other Flags

Coverage analysis can be combined with other ESBMC options:

# With bounded model checking
esbmc example.c --branch-coverage --unwind 10

# With k-induction
esbmc example.c --branch-coverage --k-induction

Multiple Input Files

ESBMC supports coverage computation for multiple input files. For example:

$ esbmc 1.c 2.c --branch-coverage

or:

$ esbmc 1.c --include-file 2.c --branch-coverage

The generated coverage report includes reached and unreached targets across all input files. Note that coverage is computed in aggregate rather than on a per-file basis.

Handling Assertions in Coverage Computation

By default, for branch and condition coverage, ESBMC treats all assertions as true. This assumes that all assertions hold, thereby reducing verification overhead.

ESBMC also supports coverage computation while taking assertions into account via --cov-assume-asserts. In this mode, assertions are converted into assumptions to preserve path constraints. Consequently, if an assertion instance fails, the corresponding execution path is considered unreachable and is not explored further.

$ esbmc example.c --branch-coverage --cov-assume-asserts

Use --no-cov-asserts to exclude the surrounding guard from each assertion’s reachability claim. This counts an assertion as reached whenever control flow reaches its source location, regardless of whether the guard that protects it is satisfiable — useful when measuring how many assert statements the test inputs touch, rather than how many distinct instances the guard makes feasible.

$ esbmc example.c --k-induction --assertion-coverage --no-cov-asserts

JSON Output and HTML Report

ESBMC supports exporting and formatting coverage summaries. First, use --cov-report-json to generate a JSON coverage report (cov-report.json). For example:

$ esbmc 1.c --include-file 2.c --branch-coverage --cov-report-json

Next, run the Python script located in the ESBMC scripts directory:

$ python3 scripts/cov-report.py cov-report.json -o .

This script reads the JSON file produced by esbmc --cov-report-json and generates an LCOV-style HTML report, including annotated source code and per-file coverage summaries.