Analyze Python code for correctness using symbolic execution and SMT solving to automatically find counterexamples for functions with type annotations and contracts.
86
A Python utility that generates symbolic values for testing and constraint solving. The generator creates symbolic representations of Python types that can be used in symbolic execution and validation scenarios.
@generates
from typing import Any, Type
class SymbolicValueGenerator:
"""
A generator that creates symbolic values for different Python types.
"""
def create_symbolic(self, type_hint: Type, name: str = "sym") -> Any:
"""
Creates a symbolic value of the specified type.
Args:
type_hint: The Python type to generate a symbolic value for
name: A variable name for the symbolic value (default: "sym")
Returns:
A symbolic value that represents the given type and can be
used in constraint solving and symbolic execution
Raises:
TypeError: If the type is not supported for symbolic generation
"""
pass
def realize(self, symbolic_value: Any) -> Any:
"""
Converts a symbolic value to a concrete value.
Args:
symbolic_value: A symbolic value to convert
Returns:
A concrete Python value
"""
passProvides symbolic execution and type proxy support for generating symbolic values.
Install with Tessl CLI
npx tessl i tessl/pypi-crosshair-toolevals
scenario-1
scenario-2
scenario-3
scenario-4
scenario-5
scenario-6
scenario-7
scenario-8
scenario-9
scenario-10