Python Pytest Test Case Generation

Overview

ESBMC now supports automatic generation of pytest test cases for Python programs. This feature automatically discovers test inputs that achieve high code coverage.

Usage

Basic Command

esbmc example.py --branch-coverage --generate-pytest-testcase

This will generate a test_example.py file containing pytest test cases.

Input Format

Your Python code should use __VERIFIER_nondet_*() functions to mark symbolic inputs:

# example.py
def classify_number(n: int) -> str:
    """Classify a number and return appropriate message"""
    if n > 0:
        if n > 100:
            return "large positive"
        else:
            return "small positive"
    elif n < 0:
        if n < -100:
            return "large negative"
        else:
            return "small negative"
    else:
        return "zero"

# Test generation mode: use nondet inputs
result = classify_number(__VERIFIER_nondet_int())

Output Format

ESBMC will generate a pytest file such as:

# Auto-generated by ESBMC 7.11.0
# Original file: example.py
# Generated: 2025-Dec-11 20:33:00.832611

from example import *
import pytest

@pytest.mark.parametrize("n", [
    -49,
    -4611686027017322505,
    0,
    -9223372036854775808,
    36,
    4611686018427388061,
    -9223372036854775805,
    2047,
])
def test_classify_number(n):
    """Auto-generated test cases for classify_number"""
    classify_number(n)

Running the Tests

After ESBMC has generated the pytest test cases, you should remove the nondeterministic input lines from the original program, such as classify_number(__VERIFIER_nondet_int()) These calls are required only during the verification phase and are no longer needed (cause errors) when running the generated pytest tests. For nondet_dict() and nondet_list(), You need to assign it to a variable first, and then pass that variable into the function. Example: x = nondet_list() classify_number(x). For more details, see nondet.py.

# Run the generated tests
pytest test_example.py

You should get the following output:

==================================================== test session starts ====================================================
platform linux -- Python 3.10.12, pytest-8.4.1, pluggy-1.6.0
rootdir: /home/lucas/examples
plugins: anyio-4.9.0, hypothesis-6.135.26
collected 8 items

test_example.py ........                                                                                              [100%]

===================================================== 8 passed in 0.16s =====================================================

If you want to run pytest with coverage, you might need to install the pytest-cov plugin as follows:

$pip install pytest-cov

Once the pytest-cov plugin is installed, you can run it as follows:

# Run with coverage
$ pytest --cov=example --cov-branch

You should get the following output:

==================================================== test session starts ====================================================
platform linux -- Python 3.10.12, pytest-8.4.1, pluggy-1.6.0
rootdir: /home/lucas/examples
plugins: anyio-4.9.0, hypothesis-6.135.26, cov-7.0.0
collected 8 items

test_example.py ........                                                                                              [100%]

====================================================== tests coverage =======================================================
_____________________________________ coverage: platform linux, python 3.10.12-final-0 ______________________________________

Name         Stmts   Miss Branch BrPart  Cover
----------------------------------------------
example.py      10      0      8      0   100%
----------------------------------------------
TOTAL           10      0      8      0   100%
===================================================== 8 passed in 0.17s =====================================================

Supported Types

__VERIFIER_nondet_int() → Python int
__VERIFIER_nondet_bool() → Python True/False
__VERIFIER_nondet_float() → Python float
__VERIFIER_nondet_str() → Python string
nondet_list() → Python list
nondet_dict() → Python dict

Example: Multiple Parameters

# example.py
def add_positive(a: int, b: int) -> int:
    """Add two positive numbers"""
    if a < 0 or b < 0:
        a = a + b
    return a + b

add_positive(__VERIFIER_nondet_int(), __VERIFIER_nondet_int())

Generated output:

# Auto-generated by ESBMC 7.11.0
# Original file: example.py

from test import *
import pytest

@pytest.mark.parametrize("a,b", [
    (-9223372036854775808, -9223372036854775808),
    (0, 0),
    (-9223372036854775808, -9223372036854775808),
])
def test_add_positive(a,b):
    """Auto-generated test cases for add_positive"""
    add_positive(a, b)

Example: nondet_list

def sum_of_positive_elements(x: list[int]) -> None:
    if len(x) > 0:
        all_positive = True
        for elem in x:
            if elem <= 0:
                all_positive = False
                break
        
        if all_positive:
            total = 0
            for elem in x:
                total += elem
            assert total > 0

x = nondet_list()
sum_of_positive_elements(x)

Generated output:

# Auto-generated by ESBMC 8.0.0
# Original file: test.py

from test import *
import pytest

@pytest.mark.parametrize("list0", [
    [4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904],
    [4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904],
    [4611686018427387904, 4611686018427387904],
    # ... many similar cases omitted ...
    [0, 0, 0, 0],
    [3, 3, 3, 3, 3, 3, 3, 3],
    [4611686018427387904, 4611686018427387904],
    [4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904, 4611686018427387904],
])
def test_sum_of_positive_elements(list0):
    """Auto-generated test cases for sum_of_positive_elements"""
    sum_of_positive_elements(list0)

Example: nondet_dict

def sum_of_positive_elements(x: dict[int, int]) -> None:
    if 0 in x:
        all_positive = True
        if all_positive:
            total = 0
            if total in x:
                total += 1


x = nondet_dict(2, key_type=nondet_int(), value_type=nondet_int())
sum_of_positive_elements(x)

Generated output:

# Auto-generated by ESBMC 8.0.0
# Original file: test.py

from test import *
import pytest

@pytest.mark.parametrize("dict0", [
    {0: 0},
    {1375: 1375},
    {0: 0},
    {0: 0},
])
def test_sum_of_positive_elements(dict0):
    """Auto-generated test cases for sum_of_positive_elements"""
    sum_of_positive_elements(dict0)

Comparison with C Test Generation

This feature is similar to the existing --generate-testcase flag for C programs, but outputs pytest-compatible Python test files instead of XML.

Feature	C (`--generate-testcase`)	Python (`--generate-pytest-testcase`)
Input Format	`int a = __VERIFIER_nondet_int();`	`__VERIFIER_nondet_int()`
Output Format	XML (Test-Comp format)	Python (pytest format)
Test Execution	Test-Comp tools	pytest
Coverage Measurement	Test-Comp	pytest-cov

Random OM