CLI Tools

def main(cmd_args=None):
    """
    Main CLI entry point for CrossHair.
    
    Parameters:
    - cmd_args: Optional list of command line arguments. If None, uses sys.argv
    
    Provides access to all CrossHair subcommands: check, watch, cover, 
    diffbehavior, and server.
    """

# Basic function checking
crosshair check mymodule.py::my_function

# Check all functions in a module
crosshair check mymodule.py

# Check with specific analysis options
crosshair check --analysis_kind=PEP316 mymodule.py

# Enable verbose output
crosshair check --verbose mymodule.py

def check(args, options, stdout, stderr):
    """
    Check command implementation for contract verification.
    
    Parameters:
    - args: Parsed command line arguments
    - options: AnalysisOptions configuration
    - stdout: Output stream for results
    - stderr: Error stream for diagnostics
    
    Returns:
    Exit code (0 for success, non-zero for failures/errors)
    
    Analyzes functions for contract violations using symbolic execution.
    Finds counterexamples where preconditions are satisfied but 
    postconditions fail.
    """

# Check single function
crosshair check mymodule.py::calculate_interest

# Check with time limit
crosshair check --per_condition_timeout=10 mymodule.py

# Check specific contract types
crosshair check --analysis_kind=icontract mymodule.py

# Check with detailed output
crosshair check --report_all --report_verbose mymodule.py

def divide(a: float, b: float) -> float:
    """
    Divide two numbers.
    
    pre: b != 0.0
    post: abs(__return__ * b - a) < 1e-10
    """
    return a / b

# CrossHair will verify this contract and report violations

def watch(args, options, max_watch_iterations=sys.maxsize):
    """
    Watch command implementation for continuous analysis.
    
    Parameters:
    - args: Parsed command line arguments
    - options: AnalysisOptions configuration  
    - max_watch_iterations: Maximum number of watch cycles
    
    Monitors specified files/modules for changes and automatically
    re-runs contract checking when modifications are detected.
    """

# Watch a single module
crosshair watch mymodule.py

# Watch with custom check interval
crosshair watch --watch_timeout=5 mymodule.py

# Watch multiple files
crosshair watch mymodule.py othermodule.py

# Watch with specific analysis options
crosshair watch --analysis_kind=deal mymodule.py

def cover(args, options, stdout, stderr):
    """
    Cover command implementation for test generation.
    
    Parameters:
    - args: Parsed command line arguments
    - options: AnalysisOptions configuration
    - stdout: Output stream for generated tests
    - stderr: Error stream for diagnostics
    
    Returns:
    Exit code (0 for success, non-zero for errors)
    
    Generates unit tests that achieve high symbolic execution coverage
    of the target functions. Can output in various formats including
    pytest and unittest.
    """

# Generate pytest tests
crosshair cover --coverage_type=pytest mymodule.py::my_function

# Generate unittest tests
crosshair cover --coverage_type=unittest mymodule.py

# Generate tests with specific coverage goals
crosshair cover --per_path_timeout=5 mymodule.py::complex_function

# Output tests to file
crosshair cover mymodule.py > test_generated.py

# Generated by CrossHair
import pytest
from mymodule import calculate_score

def test_calculate_score():
    # Test case found by symbolic execution
    result = calculate_score(age=25, experience=3, performance=0.85)
    assert result >= 0
    
def test_calculate_score_edge_case():
    # Edge case discovered by symbolic execution
    result = calculate_score(age=0, experience=0, performance=0.0)
    assert result == 0

def diffbehavior(args, options, stdout, stderr):
    """
    Diff behavior command for comparing function implementations.
    
    Parameters:
    - args: Parsed command line arguments containing function pairs
    - options: AnalysisOptions configuration
    - stdout: Output stream for comparison results
    - stderr: Error stream for diagnostics
    
    Returns:
    Exit code (0 for identical behavior, non-zero for differences)
    
    Compares two function implementations to find inputs where they
    produce different outputs or exhibit different exception behavior.
    """

# Compare two functions
crosshair diffbehavior mymodule.py::old_function mymodule.py::new_function

# Compare with exception equivalence options
crosshair diffbehavior --exception_equivalence=SAME_TYPE old.py::func new.py::func

# Compare with timeout limits
crosshair diffbehavior --per_path_timeout=10 func1 func2

Found difference between old_sort and new_sort:
Input: items=[3, 1, 2], reverse=True
old_sort returns: [3, 2, 1]  
new_sort returns: [1, 2, 3]

Reason: new_sort ignores reverse parameter

def search(args, options, stdout, stderr):
    """
    Search command implementation for path exploration.
    
    Parameters:
    - args: Parsed command line arguments
    - options: AnalysisOptions configuration
    - stdout: Output stream for search results  
    - stderr: Error stream for diagnostics
    
    Searches for execution paths that satisfy specific conditions
    or reach particular code locations.
    """

# Search for paths leading to exceptions
crosshair search --target_exceptions mymodule.py::risky_function

# Search for specific return values
crosshair search --target_returns="lambda x: x < 0" mymodule.py::compute

# Search with path constraints
crosshair search --path_depth=10 mymodule.py::complex_logic

def server(args, options, stdout, stderr):
    """
    LSP server implementation for IDE integration.
    
    Parameters:
    - args: Parsed command line arguments
    - options: AnalysisOptions configuration
    - stdout: Output stream (used for LSP communication)
    - stderr: Error stream for server diagnostics
    
    Returns:
    Does not return (NoReturn) - runs until terminated
    
    Runs a Language Server Protocol server that provides real-time
    CrossHair analysis integration for IDEs like VS Code and PyCharm.
    """

# Start LSP server
crosshair server

# Start LSP server with custom options
crosshair server --analysis_kind=icontract

# Start server with debug logging
crosshair server --verbose

def mypy_and_check(cmd_args=None):
    """
    MyPy integration command (mypycrosshair console command).
    
    Parameters:
    - cmd_args: Optional command line arguments
    
    Runs MyPy type checking followed by CrossHair contract analysis,
    providing comprehensive static analysis combining type safety
    and contract verification.
    """

# Run MyPy then CrossHair
mypycrosshair mymodule.py

# With custom MyPy configuration
mypycrosshair --mypy-config=mypy.ini mymodule.py

# Skip MyPy and run only CrossHair
mypycrosshair --skip-mypy mymodule.py

class AnalysisOptions:
    """
    Configuration options for CrossHair analysis.
    
    Controls various aspects of symbolic execution including timeouts,
    analysis depth, output verbosity, and contract interpretation.
    """

class AnalysisKind(enum.Enum):
    """
    Types of contract analysis supported.
    
    - PEP316: PEP 316 style docstring contracts
    - icontract: icontract library contracts  
    - deal: deal library contracts
    - hypothesis: Hypothesis property testing integration
    - asserts: Python assert statement checking
    """
    PEP316 = "PEP316"
    icontract = "icontract"
    deal = "deal"
    hypothesis = "hypothesis"
    asserts = "asserts"

DEFAULT_OPTIONS = AnalysisOptions()

# Analysis behavior
--analysis_kind=PEP316|icontract|deal|hypothesis|asserts
--per_condition_timeout=SECONDS
--per_path_timeout=SECONDS

# Output control  
--verbose                 # Detailed output
--report_all             # Report all findings
--report_verbose         # Verbose error reporting
--extra_plugin_dir=PATH  # Additional plugin directory

# Coverage options
--coverage_type=pytest|unittest|doctest
--cover_loops            # Include loop coverage

# Behavioral comparison
--exception_equivalence=SAME_TYPE|SAME_TYPE_AND_MESSAGE|EXACT

from crosshair.options import AnalysisOptions, AnalysisKind

options = AnalysisOptions(
    analysis_kind=AnalysisKind.icontract,
    per_condition_timeout=10.0,
    report_all=True,
    verbose=True
)