Supported Features

This page is a reference of all Python language constructs, data structures, and standard library modules currently supported by ESBMC-Python.

Basic Constructs

• Control flow: if/elif/else, for (with range()), while
• Arithmetic: +, -, *, /, //, %, **
• Logical operations: and, or, not
• Identity comparisons: is, is not (including x is None, x is not None)
• None handling: Proper type distinction from int, bool, str, etc.; correctly falsy in boolean contexts (None and True → None, None or 1 → 1)
• Global variables: The global keyword for accessing and modifying global scope from within functions
• Context managers: with and async with statements via preprocessor desugaring into explicit __enter__/__exit__ calls:
  • with EXPR as VAR: BODY — binds the return value of __enter__() to VAR
  • with EXPR: BODY — context manager used without variable binding
  • with A as a, B as b: BODY — multiple context managers in one statement; expanded left-to-right, __exit__ called in reverse order
  • async with is handled identically to with
  • Exception suppression: when the body raises, __exit__(type, value, traceback) is called and the exception is re-raised iff the return value is falsy, matching CPython semantics. This covers static return True, conditional returns (return self.flag, return et is ValueError), implicit-None bodies (propagate by default), and single-level base-class inheritance of __exit__.

Functions and Methods

• Function definitions: Parameters, return values, and calls
• Variadic parameters: *args syntax for variable-length positional argument lists
• Type annotations: Basic types (int, float, bool, str), Any, Union[T1, T2], PEP 604 T1 | T2 syntax
• Union types: Both Union[int, bool] and int | bool syntax are supported, including chained unions with multiple members
• Type widening: ESBMC selects the widest type from Union members using the hierarchy float > int > bool
• Any type: When a function is annotated -> Any, ESBMC infers the actual return type by analyzing return statements in the function body; supports int, float, bool, and expressions evaluating to those types
• Variable inference: Variables annotated with Any that are assigned from function calls inherit the function’s inferred return type
• Lambda expressions: Single-expression lambdas with multiple parameters; converted to regular functions and stored as function pointers; can be assigned to variables and called indirectly

Object-Oriented Programming

• Classes: Definitions, methods, and attributes
• Class attributes: Class-level variables shared across all instances; supports both explicit type annotations and automatic type inference from assigned values; accessible via both instance.attr and ClassName.attr
• Instance variables: Attributes defined in __init__
• Inheritance: Single and multi-level inheritance; verification of scenarios involving overridden methods
• super() calls: super().__init__(...) and other super().method(...) calls, enabling verification of polymorphic behavior and parent-constructor side effects

String Formatting and Literals

• Basic variable interpolation: f"Hello {name}!"; multiple variables in one f-string
• Built-in variable access in f-strings: f"Running as: {__name__}"
• Integer format specs: f"{num:d}", f"{num:i}"
• Float format specs: f"{val:.2f}", f"{price:.1f}"
• Boolean formatting: automatic conversion to True/False strings
• Empty and literal f-strings: f"", f"Just a string"
• F-string concatenation with other strings
• IEEE 754–compliant 32-bit and 64-bit float-to-string conversion

Data Structures

Lists

• append(x): Add element to end
• clear(): Remove all elements
• pop([i]): Remove and return element at index (default: last)
• remove(x): Remove first occurrence of value
• copy(): Return a shallow copy
• extend(iterable): Append all elements from an iterable
• reverse(): Reverse in place
• sort(): Sort in place (no arguments; key/reverse parameters not supported)
• insert(i, x): Insert at position; handles index at/beyond end, within bounds, and empty lists
• in operator: Membership testing (2 in [1, 2, 3])
• + operator: List concatenation ([1,2] + [3,4])
• Repetition: lst * n with both literal and variable lists
• Nested lists: Method calls on subscripted elements (e.g., nested[i].append(v))
• Typed instance attributes: self.attr: List[T] instance attributes with full method support

Strings

Predicates: startswith(), endswith(), isspace(), isalpha(), isdigit(), islower(), isupper(), isalnum(), isnumeric(), isidentifier()

Case conversion: lower(), upper(), capitalize(), title(), swapcase(), casefold()

Search: find(), rfind(), index(), count() (with optional range arguments)

Modification: replace(), strip(), lstrip(), rstrip(), removeprefix(), removesuffix()

Splitting/joining: split(), splitlines(), partition(), join()

Padding: center(), ljust(), rjust(), zfill(), expandtabs()

Formatting: format() with {}, {0}, {name} placeholders; format_map() with constant dicts

Slicing: s[start:end], omitted bounds (s[:end], s[start:]), negative indices (s[-3:]), empty slices

Operators: in (substring test), * (repetition: "a" * 3, 3 * "a", boolean multipliers)

Sets

• Literals: {1, 2, 3}
• Empty set: set() (note: {} creates an empty dict, not a set)
• From iterable: set(list), set(str), set(d.keys()), set(d.values())
• Operators: - (difference), & (intersection), | (union)
• Membership: x in s, x not in s
• Equality: s1 == s2, s1 != s2 (order-independent)
• len() built-in

Tuples

• Literals: (1, 2, 3), (), (5,) (single-element)
• Mixed types: (42, "hello", 3.14)
• Nested tuples: ((1, 2), (3, 4))
• Constant-index access with bounds checking: t[0], t[2]
• Generic annotation (t: tuple) and parameterized annotation (-> tuple[int, int])
• Equality comparison: t1 == (1, 2, 3)
• len() built-in
• isinstance(obj, tuple) type checking

Dictionaries

• Literals: {"a": 1, "b": 2}
• Subscript access: d["a"]; raises KeyError if absent
• Subscript assignment: d["c"] = 3
• Membership: "a" in d, "a" not in d
• Deletion: del d["a"]; raises KeyError if absent
• Equality: d1 == d2 (order-independent)
• Iteration: for loops over d.keys(), d.values(), d.items()
• update(other): Merge another dict
• get(key[, default]): Return value or default; returns Optional[T] when no default is provided
• setdefault(key[, default]): Insert key with default if absent, then return value; supports int, float, bool, str
• pop(key[, default]): Remove and return value; raises KeyError if absent and no default
• popitem(): Remove and return last inserted (key, value) pair; raises KeyError if empty
• Nested dicts: dict[int, dict[int, int]]
• Optional[T] values: dict[str, Optional[T]] storage and retrieval

Complex Numbers

• Literals: 3+4j, 1j, 0j
• Constructor: complex(real, imag) with int, float, or bool arguments
• Attributes: .real, .imag (read-only float)
• Methods: .conjugate() — returns complex conjugate
• Arithmetic: +, -, *, /, **; augmented assignment (+=, -=, *=, /=)
• Promotion: int, float, and bool operands are automatically promoted to complex
• abs(z): Returns the magnitude as a float (IEEE-754 hypot)
• Boolean context: bool(z) is False only when both .real and .imag are 0.0 (signed-zero aware)
• Equality: ==, !=; ordering operators (<, <=, >, >=) and //, % raise TypeError
• Annotations: z: complex; Optional[complex], Union[complex, float]

Enum Module (enum)

• Enum base class: members store value: int and name: str
• Comparison: ==, !=
• Hash: __hash__() returns value
• Representation: __str__() and __repr__() return name

Bytes and Integers

Byte sequences and integer class methods:

• int.from_bytes(bytes_data, big_endian, signed) — converts a byte sequence to an integer; supports big- and little-endian, signed and unsigned
• int.bit_length(n) — returns the number of bits required to represent n in binary

Error Handling

• try/except blocks with multiple handlers and except ExceptionType as var binding
• raise statements with exception instantiation and custom messages; bare raise re-raises the active exception inside an except handler
• assert statements for property verification
• __ESBMC_assume for constraining non-deterministic inputs
• ImportError guards: Imports inside try/except ImportError are handled statically

Built-in exception hierarchy:

• BaseException → Exception → AssertionError, ValueError, TypeError, IndexError, KeyError, ZeroDivisionError, ImportError
• OSError → FileNotFoundError, FileExistsError, PermissionError

Exception instances expose a message attribute and support __str__().

Concurrency (threading module)

ESBMC-Python lowers threading primitives onto ESBMC’s existing pthread operational model in src/c2goto/library/pthread_lib.c, so symex’s interleaving exploration, deadlock detection, and data-race detection apply.

threading.Lock

Lock.acquire() and Lock.release() mirror pthread_mutex_lock_noassert via __ESBMC_atomic_begin / __ESBMC_assume / __ESBMC_atomic_end. Supported usage:

• lock = threading.Lock() at module scope or as a class instance attribute
• lock.acquire() / lock.release()
• Multiple Lock instances co-existing on the same object (e.g. paired mutex and lock fields)
• from threading import Lock aliasing

threading.Thread

For each Thread(target=f, args=(...)) construction site, the frontend synthesises a per-call-site trampoline __pythread_trampoline_<N> plus three helpers in pthread_lib.c (__pyt_init_tid, __pyt_terminate, __pyt_join) that mirror pthread_create / pthread_join bookkeeping. The resulting GOTO program is a direct call (not a function pointer), so symex preserves precision.

Supported Thread shapes:

• target=f — f must be a function statically resolvable at the construction site (a Name or attribute chain). Lambdas, runtime-callable values, and Thread-subclassing’s run override are out of scope.
• args=(...) — must be a tuple literal whose elements are expressions evaluable at the construction site. Passing simple values (ints, floats, bools, strings) works end-to-end.
• t.start() and t.join() — lower to pthread_create and pthread_join semantics; join establishes happens-before.
• Multiple construction sites per program, with independent trampolines.

Data-race detection

Python module-level globals (declared with x: T = … or x = … at module scope) are flagged in the symbol table so they are visible to ESBMC’s race-assertion pass. Two threads writing to the same global without synchronisation are detected under --data-races-check:

import threading

shared: int = 0

def writer_a() -> None:
    global shared
    shared = 1

def writer_b() -> None:
    global shared
    shared = 2

t1 = threading.Thread(target=writer_a)
t2 = threading.Thread(target=writer_b)
t1.start(); t2.start(); t1.join(); t2.join()

esbmc race.py --incremental-bmc --data-races-check reports W/W data race on py:race.py@shared and VERIFICATION FAILED.

Cover Properties and Reachability

__ESBMC_cover(cond) checks whether a condition is satisfiable at a given program point (inverted assertion semantics: a counterexample means the condition is reachable).

Use with --multi-property to report all reachable/unreachable points without stopping at the first result.

x: int = __VERIFIER_nondet_int()
if x > 0:
    __ESBMC_cover(x > 100)  # Is this branch reachable?

Strict Type Checking

The --strict-types flag enables type compatibility validation for function arguments at verification time. When a type mismatch is detected, a TypeError is generated with a descriptive message. Instance methods, class methods, and static methods are all handled with appropriate implicit-parameter awareness.

Code Quality Analysis

• Missing return statement detection: Statically detects non-void functions lacking return statements on all paths; reports as verification failures; excludes __init__ automatically

Module System

• __name__: Set to "__main__" when run directly; set to the module name when imported. Enables if __name__ == "__main__": idioms.
• Imports: Standard import and from ... import ... styles validated at verification time

Built-in Functions

Complex Math Module (cmath)

All functions accept complex, float, int, or bool arguments. Real inputs are promoted to complex automatically.

Constants: pi, e, tau, inf, nan, infj, nanj

Conversion: phase(z), polar(z) → (r, φ), rect(r, φ) → complex

Power/log: exp(z), log(z[, base]), log10(z), sqrt(z)

Trigonometric: sin, cos, tan, asin, acos, atan

Hyperbolic: sinh, cosh, tanh, asinh, acosh, atanh

Utilities: isnan(z), isinf(z), isfinite(z), isclose(a, b[, rel_tol, abs_tol])

Math Module (math)

Constants: pi, e, inf, tau, nan

Rounding: floor(x), ceil(x), trunc(x), fabs(x), modf(x)

Power/log: exp(x), expm1(x), exp2(x), log(x), log1p(x), log2(x), log10(x), pow(x, y)

Trigonometric: sin, cos, tan, asin, acos, atan, atan2

Hyperbolic: sinh, cosh, tanh, asinh, acosh, atanh

Integer helpers: factorial(n), gcd(a, b), lcm(a, b), isqrt(n), perm(n[, k]), comb(n, k), prod(lst[, start]) (expects list[int])

Geometry: hypot(x, y), dist(p, q) (expects list[float])

Utilities: fmod(x, y), remainder(x, y), copysign(x, y), degrees(x), radians(x), isclose(a, b), isfinite(x), isnan(x), isinf(x)

Advanced: cbrt(x), erf(x), erfc(x), gamma(x), lgamma(x), frexp(x) → (mantissa, exponent), ldexp(x, i), nextafter(x, y), ulp(x), sumprod(a, b) (expects list[float]), fsum(values) (expects list[float])

Regular Expression Module (re)

Functions: re.match(pattern, string), re.search(pattern, string), re.fullmatch(pattern, string)

Supported pattern features:

• Universal match: .*
• Empty patterns and literal strings (no metacharacters)
• Character class ranges with quantifiers: [a-z]+, [A-Z]+, [0-9]*
• Digit sequences: \d+, \d*
• Alternation: (x|y)z*
• Prefix-with-wildcard: patterns ending with .*

Match results: Usable for Boolean/None testing (if re.match(...), re.search(...) is not None). Group-capture methods (.group(), .groups(), .span()) are not supported.

Type validation: Both arguments must be string or bytes-like; invalid types raise TypeError.

Verification approach: Uses operational models combining direct pattern recognition, literal string matching, and nondeterministic behavior for complex patterns.

Random Module (random)

All functions are modelled using nondeterministic values with appropriate constraints via __ESBMC_assume, allowing ESBMC to explore all possible values within the specified ranges.

• random.random() → nondeterministic float in [0.0, 1.0)
• random.uniform(a, b) → nondeterministic float N where min(a,b) ≤ N ≤ max(a,b)
• random.randint(a, b) → nondeterministic int N where a ≤ N ≤ b
• random.getrandbits(k) → nondeterministic integer with k random bits
• random.randrange(start[, stop[, step]]) → randomly selected integer from the specified range; single-argument form (randrange(stop)) is also supported

See also: Random Operational Model

Collections Module (collections)

• defaultdict(default_factory): Dict subclass that returns a default value for missing keys; modelled as a plain dict with a nondeterministic default
• Counter: Mapping of elements to integer counts; supports __getitem__, __setitem__, values(), and boolean truthiness

Datetime Module (datetime)

• datetime.datetime(year, month, day): Constructs a datetime object with fields year, month, day, hour (0), minute (0), second (0), microsecond (0)

Decimal Module (decimal)

• Decimal class with full arithmetic:
  • Comparison: ==, !=, <, <=, >, >=
  • Arithmetic: +, -, *, /, //, %
  • Unary: -d (negation), abs(d)
  • Special values: infinity and NaN (via is_special flag; propagated through all operations)

Heapq Module (heapq)

All functions operate on plain Python lists used as min-heaps.

• heapify(heap): No-op in the model (heap invariant assumed)
• heappush(heap, item): Appends item to the heap list
• heappop(heap): Removes and returns the minimum element
• heappushpop(heap, item): Pushes then pops the minimum

Time Module (time)

Functions use a monotonic counter model.

• time.time(): Returns a monotonically increasing float (increments by 1.0 each call)
• time.sleep(seconds): Validates seconds >= 0; no actual delay

OS Module (os)

All os functions use nondeterministic modelling to verify both success and failure paths.

Path: os.path.exists(path), os.path.basename(path)

Directory operations:

• os.makedirs(path, exist_ok=False): Creates directory tree; supports exist_ok
• os.mkdir(path): Creates single directory; may raise FileExistsError
• os.rmdir(path): Removes empty directory; may raise OSError
• os.listdir(path): Lists directory contents

File operations:

• os.remove(path): Removes file; may raise FileNotFoundError
• os.popen(cmd): Opens a pipe (modelled for verification)

NumPy Module (numpy)

Partial stub-level support for type-inference and basic arithmetic verification. Arrays are modelled as plain Python lists.

Array construction: np.array(l), np.zeros(shape), np.ones(shape)

Element-wise arithmetic: np.add(a, b), np.subtract(a, b), np.multiply(a, b), np.divide(a, b), np.power(a, b)

Math: np.ceil(x), np.floor(x), np.fabs(x), np.sqrt(x), np.trunc(x), np.round(x), np.copysign(x, y), np.fmin(x, y), np.fmax(x, y), np.sin(x)

Additional stubs (return constant placeholder values for type inference only): np.cos(x), np.arccos(x), np.arctan(x), np.exp(x), np.fmod(x), np.dot(a, b), np.matmul(a, b), np.transpose(a, b)

Linear algebra (numpy.linalg): np.linalg.det(a, b) (2×2 stub)