21567425116

Committed 01 Feb 2026 05:48PM UTC coverage: 86.023% (-8.2%) from 94.188%

Build # 21567425116

Build Type

Pull #1290

github

Committed by

web-flow

Commit Message

Merge 1c12df2dd into c539ba7b6

Pull Request Pull Request #1290: Create python-ta-z3 package

Run Details

11 of 37 new or added lines in 3 files covered. (29.73%)

18261 of 21228 relevant lines covered (86.02%)

3.4 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

18.75

/packages/python-ta-z3/src/python_ta_z3/utils.py

"""Utility functions for Z3 integration."""

from __future__ import annotations

import logging
from typing import Any

# Debug flag
DEBUG_CONTRACTS = False


def _debug(msg: str) -> None:
    """Display a debugging message.

    Do nothing if DEBUG_CONTRACTS is False.
    """
    if not DEBUG_CONTRACTS:
        return
    logging.basicConfig(format="[%(levelname)s] %(message)s", level=logging.DEBUG)
    logging.debug(msg)


def parse_assertions(obj: Any, parse_token: str = "Precondition") -> list[str]:
    """Return a list of preconditions/postconditions/representation invariants parsed from the given entity's docstring.

    Uses parse_token to determine what to look for. parse_token defaults to Precondition.

    Currently only supports two forms:

    1. A single line of the form "<parse_token>: <cond>"
    2. A group of lines starting with "<parse_token>s:", where each subsequent
       line is of the form "- <cond>". Each line is considered a separate condition.
       The lines can be separated by blank lines, but no other text.
    """
    if hasattr(obj, "doc_node") and obj.doc_node is not None:
        # Check if obj is an astroid node
        docstring = obj.doc_node.value
    else:
        docstring = getattr(obj, "__doc__") or ""
    lines = [line.strip() for line in docstring.split("\n")]
    assertion_lines = [
        i for i, line in enumerate(lines) if line.lower().startswith(parse_token.lower())
    ]

    if assertion_lines == []:
        return []

    first = assertion_lines[0]

    if lines[first].startswith(parse_token + ":"):
        return [lines[first][len(parse_token + ":") :].strip()]
    elif lines[first].startswith(parse_token + "s:"):
        assertions = []
        for line in lines[first + 1 :]:
            if line.startswith("-"):
                assertion = line[1:].strip()
                if hasattr(obj, "__qualname__"):
                    _debug(f"Adding assertion to {obj.__qualname__}: {assertion}")
                assertions.append(assertion)
            elif line != "":
                break
        return assertions
    else:
        return []

1	"""Utility functions for Z3 integration."""
2
3	from __future__ import annotations	10✔
4
5	import logging	10✔
6	from typing import Any	10✔
7
8	# Debug flag
9	DEBUG_CONTRACTS = False	10✔
10
11
12	def _debug(msg: str) -> None:	10✔
13	"""Display a debugging message.
14
15	Do nothing if DEBUG_CONTRACTS is False.
16	"""
NEW 17	if not DEBUG_CONTRACTS:	×
NEW 18	return	×
NEW 19	logging.basicConfig(format="[%(levelname)s] %(message)s", level=logging.DEBUG)	×
NEW 20	logging.debug(msg)	×
21
22
23	def parse_assertions(obj: Any, parse_token: str = "Precondition") -> list[str]:	10✔
24	"""Return a list of preconditions/postconditions/representation invariants parsed from the given entity's docstring.
25
26	Uses parse_token to determine what to look for. parse_token defaults to Precondition.
27
28	Currently only supports two forms:
29
30	1. A single line of the form "<parse_token>: <cond>"
31	2. A group of lines starting with "<parse_token>s:", where each subsequent
32	line is of the form "- <cond>". Each line is considered a separate condition.
33	The lines can be separated by blank lines, but no other text.
34	"""
NEW 35	if hasattr(obj, "doc_node") and obj.doc_node is not None:	×
36	# Check if obj is an astroid node
NEW 37	docstring = obj.doc_node.value	×
38	else:
NEW 39	docstring = getattr(obj, "__doc__") or ""	×
NEW 40	lines = [line.strip() for line in docstring.split("\n")]	×
NEW 41	assertion_lines = [	×
42	i for i, line in enumerate(lines) if line.lower().startswith(parse_token.lower())
43	]
44
NEW 45	if assertion_lines == []:	×
NEW 46	return []	×
47
NEW 48	first = assertion_lines[0]	×
49
NEW 50	if lines[first].startswith(parse_token + ":"):	×
NEW 51	return [lines[first][len(parse_token + ":") :].strip()]	×
NEW 52	elif lines[first].startswith(parse_token + "s:"):	×
NEW 53	assertions = []	×
NEW 54	for line in lines[first + 1 :]:	×
NEW 55	if line.startswith("-"):	×
NEW 56	assertion = line[1:].strip()	×
NEW 57	if hasattr(obj, "__qualname__"):	×
NEW 58	_debug(f"Adding assertion to {obj.__qualname__}: {assertion}")	×
NEW 59	assertions.append(assertion)	×
NEW 60	elif line != "":	×
NEW 61	break	×
NEW 62	return assertions	×
63	else:
NEW 64	return []	×

pyta-uoft / pyta / 21567425116

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous