### Installing CrossHair Tool (Shell)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/get_started.rst

Installs the CrossHair static analysis tool using pip within your Python development environment. This command adds the crosshair-tool package to your environment, making it available for use.

```shell
pip install crosshair-tool
```

--------------------------------

### Installation and basic crosshair cover syntax

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/cover.rst

Provides instructions for installing CrossHair using pip and the general command syntax for running `crosshair cover`.

```Shell
$ pip install crosshair-tool
$ crosshair cover <module>.<function>
```

--------------------------------

### Basic crosshair cover usage and output

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/cover.rst

Demonstrates running `crosshair cover` on the example `average` function and shows the default output format, which provides input examples.

```Shell
$ cat foo.py
from typing import List, Optional
def average(nums: List[float], default:Optional[float] = None) -> float:
    if len(nums) == 0:
        if default is None:
            raise ValueError
        return default
    return sum(nums) / len(nums)

$ crosshair cover foo.average
average([0.0, 0.0], None)
average([], 0.0)
average([], None)
```

--------------------------------

### Watching Code with CrossHair (Shell)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/get_started.rst

Starts the CrossHair tool in watch mode, continuously analyzing the code in the specified directory for contract violations. This allows CrossHair to run in the background and re-analyze automatically when code changes.

```shell
crosshair watch [directory with code to analyze]
```

--------------------------------

### Installing CrossHair and Basic diffbehavior Usage

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Provides the command-line steps to install the `crosshair-tool` package using pip and the general syntax for using the `crosshair diffbehavior` command to compare two functions.

```bash
$ pip install crosshair-tool
$ crosshair diffbehavior <module>.<function> <module>.<function>
```

--------------------------------

### Simple Counter Class Example (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/hints_for_your_classes.rst

Shows a basic Python class Counter with an __init__ method that initializes an instance variable count to zero. This example is used to illustrate a scenario where the default CrossHair creation might not capture all possible states.

```Python
class Counter:
  def __init__(self):
    self.count = 0
  # ... more methods ...
```

--------------------------------

### Install Development Requirements (Shell)

Source: https://github.com/pschanely/crosshair/blob/main/doc/contributing_to_docs.md

Installs the project's development dependencies using pip, including the package itself in editable mode. This command should be run from the repository's root directory after activating a virtual environment.

```Shell
pip3 install -e .[dev]
```

--------------------------------

### Installing Development Dependencies with Pip

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contributing.rst

Command to install project dependencies, including development extras, into the active virtual environment using pip. The `--editable .` flag installs the package in editable mode, linking changes in the source code directly to the installed package.

```Shell
pip3 install --editable .[dev]
```

--------------------------------

### Start CrossHair LSP Server (Shell)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/ide_integrations.rst

This command starts the CrossHair Language Server Protocol (LSP) server. It is the preferred method for IDE integration as it allows CrossHair to run persistently in the background. Ensure you use the Python executable from your project's environment.

```shell
{PATH-TO-PROJECT-PYTHON}python -m crosshair server
```

--------------------------------

### Example Python function for coverage analysis

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/cover.rst

Defines a simple Python function `average` with type hints, used as an example target for the `crosshair cover` command.

```Python
from typing import List, Optional
def average(nums: List[float], default:Optional[float] = None) -> float:
    if len(nums) == 0:
        if default is None:
            raise ValueError
        return default
    return sum(nums) / len(nums)
```

--------------------------------

### Generating pytest tests with crosshair cover

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/cover.rst

Shows how to use the `--example_output_format=pytest` option to generate stub pytest test functions based on the found coverage examples.

```Shell
$ crosshair cover --example_output_format=pytest foo.average
import pytest
from foo import average

def test_average():
    assert average([0.0, 0.0], None) == 0.0

def test_average_2():
    assert average([], 0.0) == 0.0

def test_average_3():
    with pytest.raises(ValueError):
        average([], None)
```

--------------------------------

### Using Assert Statements for Contracts in Python

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/kinds_of_contracts.rst

Demonstrates how CrossHair analyzes functions using standard Python assert statements as preconditions and postconditions. Functions must start with one or more asserts to be analyzed. The example shows a function `remove_smallest` with asserts.

```python
# foo.py
from typing import List

def remove_smallest(numbers: List[int]) -> None:
  ''' Removes the smallest number in the given list. '''

  # The precondition: CrossHair will assume this to be true:
  assert len(numbers) > 0

  smallest = min(numbers)

  numbers.remove(smallest)

  # The postcondition: CrossHair will find examples to make this be false:
  assert len(numbers) == 0 or min(numbers) > smallest
```

--------------------------------

### Activating Virtual Environment on Windows

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contributing.rst

Command to activate the created virtual environment on Windows systems. This makes the environment's Python and installed packages available in the current shell session.

```Shell
venv\Scripts\activate
```

--------------------------------

### Displaying Dog Names with Locations (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/case_studies.rst

Defines a Python generator function `display_in_locations` that takes a list of locations. It uses the `dog_names` function to get dog names and pairs them with locations, yielding formatted strings for display.

```Python
def display_in_locations(locations: List[str]):
    for dog_name, location in zip(dog_names(len(locations)), locations):
        yield dog_name.ljust(10) + "is in" + location.rjust(10)
```

--------------------------------

### Activating Virtual Environment on Unix/Mac

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contributing.rst

Command to activate the created virtual environment on Unix-like systems (Linux, macOS). This makes the environment's Python and installed packages available in the current shell session.

```Shell
source venv/bin/activate
```

--------------------------------

### Example Test Function with Crosshair Contract (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/plugins.rst

Defines a simple Python function `myrandom` that uses `np.random.randint` and includes a docstring contract (`pre` and `post` conditions) that Crosshair will check. This function serves as an example to demonstrate how Crosshair interacts with contracted external functions.

```python
import numpy as np
def myrandom(a: int) -> int:
    """
    pre: a < 10
    post: _ > a
    """
    return np.random.randint(a, 10)
```

--------------------------------

### Re-implementing Native Code for CrossHair Plugin (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/plugins.rst

This example demonstrates how a CrossHair plugin can provide pure Python re-implementations of classes and functions from a native (C) module. It shows how to define a replacement class (`_Bunny`) and function (`_introduce_bunnies`) and register them with CrossHair using `register_type` and `register_patch`.

```Python
from crosshair import register_patch, register_type, SymbolicFactory
from typing import Union

# import the original, native implementations:
from bunnies import Bunny, introduce_bunnies

# Replicate the native "Bunny" class in pure Python:

class _Bunny:
    happiness: int
    def __init__(self, factory: SymbolicFactory):
        # CrossHair will pass your constructor a factory that you can use to create
        # more symbolic values of any other type.
        self.happiness = factory(int)

    def pet(self: _Bunny) -> None:
        self.happiness += 1

# Replicate functions too:

AnyBunny = Union[Bunny, _Bunny]  # arguments can be any kind of Bunny
def _introduce_bunnies(bunny1: AnyBunny, bunny2: AnyBunny) -> None:
    bunny1.happiness += 1
    bunny2.happiness += 1


# Tell CrossHair to use these implementations instead of the native ones:
register_type(bunnies.Bunny, _Bunny)
register_patch(bunnies.introduce_bunnies, _introduce_bunnies)
```

--------------------------------

### Example Usage of diffbehavior Shell Function (Bash)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Demonstrates how to invoke the previously defined `diffbehavior` shell function with a target like `foo.cut` to compare code behavior.

```bash
$ diffbehavior foo.cut
...
```

--------------------------------

### Creating a Bash Function for git worktree diffbehavior Workflow

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Provides an example bash shell function that automates the process of creating a temporary clean git worktree and preparing to run `crosshair diffbehavior` against it.

```bash
diffbehavior() {
    git worktree add --detach _clean || exit 1
}
```

--------------------------------

### Registering Contract and Signature for External Function (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/plugins.rst

This snippet demonstrates how to register both a contract and the signature for an external function, particularly useful for functions from C modules like NumPy where CrossHair might not infer the signature automatically. It shows the necessary imports and the start of creating a `Signature` object.

```Python
from crosshair.register_contract import register_contract
import numpy as np
from inspect import Parameter, Signature
randint_sig = Signature(
    parameters=[

```

--------------------------------

### Defining Python Functions for Comparison

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Defines two Python functions, `cut1` and `cut2`, which attempt to remove an element from a list at a given index. These functions are used as examples to demonstrate the `crosshair diffbehavior` command.

```python
from typing import List

def cut1(a: List[int], i: int) -> None:
  a[i:i+1] = []

def cut2(a: List[int], i: int) -> None:
  a[:] = a[:i] + a[i+1:]
```

--------------------------------

### Crosshair Error Output Example

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/plugins.rst

Shows the output from running `crosshair check` when a contract violation is found. It indicates the function call (`myrandom(0)`) and the specific patched return value (`numpy.random.mtrand.RandomState.randint: [0]`) that caused the postcondition (`_ > a`) to fail.

```text
error: false when calling myrandom(0)
with crosshair.patch_to_return(numpy.random.mtrand.RandomState.randint: [0]})
```

--------------------------------

### Registering Custom Type Creation with CrossHair (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/hints_for_your_classes.rst

Provides an example of registering a custom function symbolic_counter with crosshair.register_type to control how CrossHair creates instances of the Counter class. The custom function uses a SymbolicFactory to assign a symbolic integer value to the count attribute, allowing CrossHair to explore states where count is not zero.

```Python
import crosshair
def symbolic_counter(factory: crosshair.SymbolicFactory) -> Counter:
  counter = Counter()
  counter.count = factory(int)  # count is now a symbolic holding any integer value
  return counter
crosshair.register_type(Counter, symbolic_counter)
```

--------------------------------

### Silencing Exceptions in CrossHair Assert Contracts using Docstrings

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/kinds_of_contracts.rst

Explains how to prevent CrossHair from reporting exceptions by documenting them in the function's docstring using the Sphinx-style `:raises` directive. Provides a simple example function `choose`.

```python
def choose(option: int) -> str:
    """
    Does things.

    :raises IndexError: when option isn't a valid choice
    """
    ...
```

--------------------------------

### Initializing CrossHair Symbolic Execution Context

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Demonstrates how to set up a standalone symbolic execution environment in CrossHair by importing necessary components and entering the statespace context. This is the first step before creating or manipulating symbolic values.

```Python
from crosshair.core_and_libs import proxy_for_type
from crosshair.core_and_libs import NoTracing
from crosshair.core_and_libs import standalone_statespace
space = standalone_statespace.__enter__()
```

--------------------------------

### Configuring CrossHair Plugin Entry Point in setup.py (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/plugins.rst

This snippet shows how to configure a Python package's `setup.py` file to register it as a CrossHair plugin. It uses the `entry_points` mechanism under the `crosshair.plugin` key to make the plugin discoverable by CrossHair.

```Python
from setuptools import setup
setup(
    name="crosshair-plugin-bunnies",
    py_modules=["crosshair_plugin_bunnies"],
    entry_points={"crosshair.plugin": ["bunnies = crosshair_plugin_bunnies"]},
)
```

--------------------------------

### crosshair cover command help message

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/cover.rst

Displays the full help output for the `crosshair cover` command, listing all available options, arguments, and their descriptions.

```Shell
crosshair cover --help
```

```Text
usage: crosshair cover [-h] [--verbose]
                       [--extra_plugin EXTRA_PLUGIN [EXTRA_PLUGIN ...]]
                       [--example_output_format FORMAT] [--coverage_type TYPE]
                       [--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS]
                       [--per_path_timeout FLOAT]
                       [--per_condition_timeout FLOAT]
                       TARGET [TARGET ...]

Generates inputs to a function, hopefully getting good line, branch,
and path coverage.
See https://crosshair.readthedocs.io/en/latest/cover.html

positional arguments:
  TARGET                A fully qualified module, class, or function, or
                        a directory (which will be recursively analyzed), or
                        a file path with an optional ":<line-number>" suffix.
                        See https://crosshair.readthedocs.io/en/latest/contracts.html#targeting

options:
  -h, --help            show this help message and exit
  --verbose, -v         Output additional debugging information on stderr
  --extra_plugin EXTRA_PLUGIN [EXTRA_PLUGIN ...]
                        Plugin file(s) you wish to use during the current execution
  --example_output_format FORMAT
                        Determines how to output examples.
                            eval_expression     : [default] Output examples as expressions,
                                                  suitable for eval()
                            arg_dictionary      : Output arguments as repr'd, ordered
                                                  dictionaries
                            pytest              : Output examples as stub pytest tests
                            argument_dictionary : Deprecated
  --coverage_type TYPE  Determines what kind of coverage to achieve.
                            opcode : [default] Cover as many opcodes of the function as
                                     possible. This is similar to "branch" coverage.
                            path   : Cover any possible execution path.
                                     There will usually be an infinite number of paths (e.g.
                                     loops are effectively unrolled). Use
                                     max_uninteresting_iterations and/or per_condition_timeout
                                     to bound results.
                                     Many path decisions are internal to CrossHair, so you may
                                     see more duplicative-ness in the output than you'd expect.
  --max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
                        Maximum number of consecutive iterations to run without making
                        significant progress in exploring the codebase.
                        (by default, 5 iterations, unless --per_condition_timeout is set)

                        This option can be more useful than --per_condition_timeout
                        because the amount of time invested will scale with the complexity
                        of the code under analysis.

                        Use a small integer (3-5) for fast but weak analysis.
                        Values in the hundreds or thousands may be appropriate if you
```

--------------------------------

### Build Documentation with Sphinx (Shell)

Source: https://github.com/pschanely/crosshair/blob/main/doc/contributing_to_docs.md

Changes the current directory to the 'doc' directory and then runs the Sphinx build command. This compiles the reStructuredText source files into the 'build' directory.

```Shell
cd doc
sphinx-build source build
```

--------------------------------

### Displaying CrossHair Watch Command Help (Text)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contracts.rst

This snippet shows the command-line help output for the crosshair watch command. It details the command's usage, positional arguments (TARGET), and available options like --verbose, --extra_plugin, and --analysis_kind, explaining how to monitor files or directories for contract violations.

```text
usage: crosshair watch [-h] [--verbose]
                       [--extra_plugin EXTRA_PLUGIN [EXTRA_PLUGIN ...]]
                       [--analysis_kind KIND]
                       TARGET [TARGET ...]

The watch command continuously looks for contract counterexamples.
Type Ctrl-C to stop this command.

positional arguments:
  TARGET                File or directory to watch. Directories will be recursively analyzed.
                        See https://crosshair.readthedocs.io/en/latest/contracts.html#targeting

options:
  -h, --help            show this help message and exit
  --verbose, -v         Output additional debugging information on stderr
  --extra_plugin EXTRA_PLUGIN [EXTRA_PLUGIN ...]
                        Plugin file(s) you wish to use during the current execution
      --analysis_kind KIND  Kind of contract to check.
                            By default, the PEP316, deal, and icontract kinds are all checked.
                            Multiple kinds (comma-separated) may be given.
```

--------------------------------

### Creating a Z3 Expression Directly

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Demonstrates how to import the `z3` library and create a Z3 expression by combining a Z3 variable (obtained from a symbolic object) with a Z3 integer literal.

```Python
import z3

expr = symbolic_x.var + z3.IntVal(1)
expr
type(expr)
```

--------------------------------

### Displaying crosshair diffbehavior Help

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Shows the command to display the help message for the `crosshair diffbehavior` command, listing available options and arguments.

```bash
crosshair diffbehavior --help
```

--------------------------------

### Defining a Dataclass for CrossHair (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/hints_for_your_classes.rst

Demonstrates how to define a simple Python dataclass with type hints. Dataclasses automatically generate an __init__ method with typed arguments, making them compatible with CrossHair out-of-the-box for symbolic instance creation.

```Python
import dataclasses
@dataclasses.dataclass
class Person:
  name: str
  age: int
```

--------------------------------

### crosshair diffbehavior Command Line Options

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Provides the detailed usage information and available command-line options for the `crosshair diffbehavior` tool, including arguments like function names, verbosity, plugins, exception handling, and timeouts.

```text
usage: crosshair diffbehavior [-h] [--verbose]
                                  [--extra_plugin EXTRA_PLUGIN [EXTRA_PLUGIN ...]]
                                  [--exception_equivalence EXCEPTION_EQUIVALENCE]
                                  [--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS]
                                  [--per_path_timeout FLOAT]
                                  [--per_condition_timeout FLOAT]
                                  FUNCTION1 FUNCTION2

Find differences in the behavior of two functions.
See https://crosshair.readthedocs.io/en/latest/diff_behavior.html

positional arguments:
  FUNCTION1             first fully-qualified function to compare (e.g. "mymodule.myfunc")
  FUNCTION2             second fully-qualified function to compare

options:
  -h, --help            show this help message and exit
  --verbose, -v         Output additional debugging information on stderr
  --extra_plugin EXTRA_PLUGIN [EXTRA_PLUGIN ...]
                            Plugin file(s) you wish to use during the current execution
  --exception_equivalence EXCEPTION_EQUIVALENCE
                            Decide how to treat exceptions, while searching for a counter-example.
                            `ALL` treats all exceptions as equivalent,
                            `SAME_TYPE`, considers matches on the type.
                            `TYPE_AND_MESSAGE` matches for the same type and message.
      --max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
                            Maximum number of consecutive iterations to run without making
                            significant progress in exploring the codebase.
                            (by default, 5 iterations, unless --per_condition_timeout is set)

                            This option can be more useful than --per_condition_timeout
                            because the amount of time invested will scale with the complexity
                            of the code under analysis.

                            Use a small integer (3-5) for fast but weak analysis.
                            Values in the hundreds or thousands may be appropriate if you
                            intend to run CrossHair for hours.
      --per_path_timeout FLOAT
                            Maximum seconds to spend checking one execution path.
                            If unspecified:
                            1. CrossHair will timeout each path at the square root of
                               `--per_condition_timeout`, if specified.
                            3. Otherwise, it will timeout each path at a number of seconds
                               equal to `--max_uninteresting_iterations`, unless it is
                               explicitly set to zero.
                               (NOTE: `--max_uninteresting_iterations` is 5 by default)
                            2. Otherwise, it will not use any per-path timeout.
      --per_condition_timeout FLOAT
                            Maximum seconds to spend checking execution paths for one condition
```

--------------------------------

### Defining a Function with Contractual SemVer Contracts (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/case_studies.rst

Defines a Python function `dog_names` that returns a list of dog names up to a specified limit. It includes a docstring with pre- and post-conditions (`pre:` and `post:`) defining its contractual behavior for use with tools like CrossHair. The `# crosshair: specs_complete=True` directive indicates that the function's behavior is fully described by its contracts.

```Python
from typing import List
def dog_names(limit: int) -> List[str]:
    """
    Do not give us a negative limit:
    pre: limit >= 0

    All dog names are non-empty:
    post: all(len(name) > 0 for name in __return__)

    We never return more names than the limit you provide:
    post: len(__return__) <= limit

    We will provide at least 3 names:
    post: limit > 3 or len(__return__) == limit
    """
    # crosshair: specs_complete=True
    return ["Toto", "Clifford", "Fido", "Doge", "Lassie"][:limit]
```

--------------------------------

### Running Pre-commit Checks

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contributing.rst

Command to execute all configured pre-commit hooks on all files in the repository. This ensures code formatting and consistency before committing changes.

```Shell
pre-commit run --all-files
```

--------------------------------

### Creating a Symbolic Integer

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Shows how to create a symbolic value representing a Python integer using `proxy_for_type`. Initially, this object behaves like a regular integer for standard Python operations.

```Python
symbolic_x = proxy_for_type(int, 'x')
type(symbolic_x)
```

--------------------------------

### Running diffbehavior on isack (Bash)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Executes `diffbehavior` on the `isack` function to find inputs that reveal the behavioral differences between the original and modified versions, showing the counterexamples found.

```bash
$ diffbehavior foo.isack
Given: (s='\x00'),
             foo.isack : returns False
      _clean.foo.isack : raises ValueError('invalid ack')
    Given: (s='YES'),
             foo.isack : returns False
      _clean.foo.isack : returns True
```

--------------------------------

### Comparing Code Changes with git worktree and crosshair diffbehavior

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Illustrates a workflow using `git worktree` to create a clean copy of the repository and then using `crosshair diffbehavior` to compare a function in the current working copy against the version in the clean copy.

```bash
# Let's say we edit the clean() function in foo.py

# Step 1: Create an unmodified source tree under a directory named "clean":
$ git worktree add --detach clean

# Step 2: Have CrossHair try to detect a difference:
$ crosshair diffbehavior foo.cut clean.foo.cut

# Step 3: Remove the "clean" directory when you're done:
$ git worktree remove clean
```

--------------------------------

### Improved Unit Test for Display Function (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/case_studies.rst

An improved version of the unit test for `display_in_locations`. Instead of asserting on the full formatted string, it asserts only on the location suffix, making the test less dependent on the specific dog names returned by the library function.

```Python
def test_display_in_locations():
    lines = display_in_locations(["Halifax", "New York"])
    assert [l[10:] for l in lines] == [
        "   Halifax",
        "  New York",
    ]
```

--------------------------------

### Checking Assert-based Contracts with CrossHair Shell Command

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/kinds_of_contracts.rst

Shows how to run CrossHair analysis on a Python file containing assert-based contracts using the command line. The output demonstrates how CrossHair reports an AssertionError when it finds a counterexample that violates a postcondition.

```shell
$ crosshair check --analysis_kind=asserts foo.py
foo.py:14:error:AssertionError:  when calling remove_smallest(numbers = [0, -1, -177, -178, -178])
```

--------------------------------

### Registering Crosshair Contract for NumPy randint (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/plugins.rst

Shows how to define a function signature and register a pre/post condition contract for a method from an external library like NumPy using Crosshair's `register_contract`. It includes the parameter definitions for `np.random.RandomState.randint` and specifies conditions for its inputs (`low < high`) and outputs (`low <= __return__ < high`).

```python
Parameter("self", Parameter.POSITIONAL_OR_KEYWORD),
Parameter("low", Parameter.POSITIONAL_OR_KEYWORD, annotation=int),
Parameter("high", Parameter.POSITIONAL_OR_KEYWORD, annotation=int),
],
return_annotation=int,
)
register_contract(
    np.random.RandomState.randint,
    pre=lambda low, high: low < high,
    post=lambda __return__, low, high: low <= __return__ < high,
    sig=randint_sig,
)
```

--------------------------------

### Brittle Unit Test for Display Function (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/case_studies.rst

A unit test for the `display_in_locations` function. It uses a trivial `""" post: True """` contract to enable CrossHair analysis. The assertion is brittle as it relies on specific dog names returned by `dog_names`, which may change in future library versions.

```Python
def test_display_in_locations():
    """ post: True """  #  <- The trivial contract enables CrossHair analysis
    lines = display_in_locations(["Halifax", "New York"])
    assert lines == [
        "Clifford  is in   Halifax",
        "Fido      is in  New York",
    ]
```

--------------------------------

### Running crosshair diffbehavior on Python Functions

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Demonstrates how to use the `crosshair diffbehavior` command from the command line to compare the behavior of two Python functions, `foo.cut1` and `foo.cut2`.

```bash
$ crosshair diffbehavior foo.cut1 foo.cut2
```

--------------------------------

### Accessing Symbolic Variable Representation (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Demonstrates how to access the underlying symbolic representation of a CrossHair symbolic variable using the '.var' attribute.

```Python
>>> (symbolic_x >= 0).var
```

```Python
0 <= x
```

--------------------------------

### Creating a Python Virtual Environment

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contributing.rst

Command to create a new virtual environment named 'venv' using the Python `venv` module. This isolates project dependencies.

```Shell
python -m venv venv
```

--------------------------------

### Wrapping a Z3 Expression in a Symbolic Object

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Illustrates how to create a new CrossHair symbolic object (specifically `SymbolicInt`) from an existing Z3 expression, allowing the result of Z3 operations to be used within the CrossHair framework.

```Python
from crosshair.libimpl.builtinslib import SymbolicInt
symbolic_x_incr = SymbolicInt(symbolic_x.var + z3.IntVal(1))
```

--------------------------------

### Usage and Options for CrossHair Check Command (Text)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contracts.rst

This snippet shows the command-line usage, positional arguments, and available options for the `crosshair check` command. It also explains the output format for errors and the possible exit codes.

```text
usage: crosshair check [-h] [--verbose]
                       [--extra_plugin EXTRA_PLUGIN [EXTRA_PLUGIN ...]]
                       [--report_all] [--report_verbose]
                       [--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS]
                       [--per_path_timeout FLOAT]
                       [--per_condition_timeout FLOAT] [--analysis_kind KIND]
                       TARGET [TARGET ...]

The check command looks for counterexamples that break contracts.

It outputs machine-readable messages in this format on stdout:
    <filename>:<line number>: error: <error message>

It exits with one of the following codes:
    0 : No counterexamples are found
    1 : Counterexample(s) have been found
    2 : Other error

positional arguments:
  TARGET                A fully qualified module, class, or function, or
                        a directory (which will be recursively analyzed), or
                        a file path with an optional ":<line-number>" suffix.
                        See https://crosshair.readthedocs.io/en/latest/contracts.html#targeting

options:
  -h, --help            show this help message and exit
  --verbose, -v         Output additional debugging information on stderr
  --extra_plugin EXTRA_PLUGIN [EXTRA_PLUGIN ...]
                        Plugin file(s) you wish to use during the current execution
  --report_all          Output analysis results for all postconditions (not just failing ones)
  --report_verbose      Output context and stack traces for counterexamples
  --max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
                        Maximum number of consecutive iterations to run without making
                        significant progress in exploring the codebase.
                        (by default, 5 iterations, unless --per_condition_timeout is set)

                        This option can be more useful than --per_condition_timeout
                        because the amount of time invested will scale with the complexity
                        of the code under analysis.

                        Use a small integer (3-5) for fast but weak analysis.
                        Values in the hundreds or thousands may be appropriate if you
                        intend to run CrossHair for hours.
  --per_path_timeout FLOAT
                        Maximum seconds to spend checking one execution path.
                        If unspecified:
                        1. CrossHair will timeout each path at the square root of
                           `--per_condition_timeout`, if specified.
                        3. Otherwise, it will timeout each path at a number of seconds
                           equal to `--max_uninteresting_iterations`, unless it is
                           explicitly set to zero.
                           (NOTE: `--max_uninteresting_iterations` is 5 by default)
                        2. Otherwise, it will not use any per-path timeout.
  --per_condition_timeout FLOAT
                        Maximum seconds to spend checking execution paths for one condition
  --analysis_kind KIND  Kind of contract to check.
                        By default, the PEP316, deal, and icontract kinds are all checked.
                        Multiple kinds (comma-separated) may be given.
                        See https://crosshair.readthedocs.io/en/latest/kinds_of_contracts.html
                            asserts    : check assert statements
                            PEP316     : check PEP316 contracts (docstring-based)
                            icontract  : check icontract contracts (decorator-based)
                            deal       : check deal contracts (decorator-based)
```

--------------------------------

### Registering Contract for External Function (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/plugins.rst

This snippet shows how to register a contract (preconditions and postconditions) for an external function like `random.randint`. Registering a contract allows CrossHair to skip executing the function during analysis, assuming the contract holds if the preconditions are met. This is useful for non-deterministic or complex functions.

```Python
from crosshair.register_contract import register_contract
from random import Random
register_contract(
    Random.randint,
    pre=lambda a, b: a <= b,
    post=lambda __return__, a, b: a <= __return__ <= b,
)
```

--------------------------------

### Conditional Logic with Symbolic Variables (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Illustrates a scenario where a symbolic boolean expression is used in a Python conditional statement, requiring CrossHair to resolve it to a concrete boolean value by consulting Z3.

```Python
if symbolic_x > 0:
    print('bigger than zero')
```

--------------------------------

### Running Full Test Suite with Pytest

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contributing.rst

Command to run the full test suite using pytest within the virtual environment. It sets the `PYTHONHASHSEED` environment variable for reproducibility and uses parallel execution (`-n auto --dist worksteal`).

```Shell
env PYTHONHASHSEED=0 python -m pytest -n auto --dist worksteal
```

--------------------------------

### Accessing the Underlying Z3 Variable

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Shows how to access the Z3 variable(s) held by a CrossHair symbolic object using the `.var` attribute. It also demonstrates checking the type of the retrieved Z3 variable.

```Python
symbolic_x.var
type(symbolic_x.var)
```

--------------------------------

### Check File with CrossHair (Shell)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/ide_integrations.rst

This command runs CrossHair on a specific file. This method is an alternative to LSP integration, where the IDE executes this command and parses its standard output and exit code to display diagnostics. The output format is similar to mypy.

```shell
crosshair check [FILENAME]
```

--------------------------------

### Revealing CrossHair Type with NoTracing

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Explains how to use the `NoTracing` context manager to reveal the underlying CrossHair type of a symbolic object, demonstrating that it is not a native Python type but a custom CrossHair implementation.

```Python
no_tracing = NoTracing()
no_tracing.__enter__()
type(symbolic_x)
```

--------------------------------

### Performing Standard Operations on Symbolic Objects

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/how_does_it_work.rst

Shows that after exiting the `NoTracing` context, standard Python operations (like addition) can be performed directly on symbolic objects. The CrossHair object handles the underlying Z3 operations and the result's `.var` attribute shows the resulting Z3 expression. Also includes exiting the `NoTracing` context.

```Python
no_tracing.__exit__()
(symbolic_x + 1).var
```

--------------------------------

### CrossHair Output Showing Assertion Failure

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/case_studies.rst

This snippet shows the output from CrossHair when analyzing the brittle `test_display_in_locations` function. It indicates an `AssertionError` occurred and provides a `crosshair.patch_to_return` expression that can be used to reproduce the failure by patching `dog_names` to return `['a', 'a']`.

```CrossHair Output
AssertionError when calling test_display_in_locations()
with crosshair.patch_to_return({dog_names: [['a', 'a']]})
```

--------------------------------

### Reproducing Crosshair Failure with patch_to_return (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/plugins.rst

Mentions the `crosshair.patch_to_return` context manager, which can be used in a Python `with` statement to reproduce the specific conditions (like a patched return value) that caused a Crosshair failure reported in the output.

```python
crosshair.patch_to_return(numpy.random.mtrand.RandomState.randint: [0]})
```

--------------------------------

### Modified isack Function (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

A modified version of the `isack` function that accepts 'y', 'yes', 'Y', 'YES' as True, 'n', 'no', 'N', 'NO' as False, and raises a `ValueError` for other inputs.

```python
def isack(s: str) -> bool:
        if s in ('y', 'yes', 'Y', 'YES'):
            return True
        if s in ('n', 'no', 'N', 'NO'):
            return False
        raise ValueError('invalid ack')
```

--------------------------------

### Original isack Function (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

The initial implementation of a Python function `isack` that checks if a string is 'y' or 'yes', returning True, otherwise False.

```python
def isack(s: str) -> bool:
        if s in ('y', 'yes'):
            return True
        return False
```

--------------------------------

### Running diffbehavior on longest_str (Bash)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Executes `diffbehavior` on the `longest_str` function to verify that the refactoring did not change its behavior, showing the output indicating no differences found.

```bash
$ diffbehavior foo.longest_str
No differences found. (attempted 15 iterations)
Consider trying longer with: --per_condition_timeout=<seconds>
```

--------------------------------

### Define Shell Function for diffbehavior (Bash)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

Defines a shell function `diffbehavior` that creates a temporary git worktree `_clean`, runs `crosshair diffbehavior` against it, and then removes the worktree. This allows comparing the current state with a clean version.

```bash
crosshair diffbehavior "$1" "_clean.$@"
git worktree remove _clean
```

--------------------------------

### Configuring CrossHair Analysis with Directives (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/contracts.rst

This snippet demonstrates how to use special comments (directives) within Python code to control CrossHair's analysis. Directives like # crosshair: off, # crosshair: on, and # crosshair: analysis_kind can enable/disable analysis or specify the contract syntax to use for specific functions or modules.

```Python
# crosshair: off

def grow(age: int):
    # crosshair: on
    # crosshair: analysis_kind=asserts
    assert age >= 0
    ...
```

--------------------------------

### Refactored longest_str Function (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

A refactored version of the `longest_str` function using Python's built-in `max` function with a `key` argument for conciseness.

```python
def longest_str(items: List[str]) -> str:
  return max(items,
                 key=lambda item: len(item),
                 default='')
```

--------------------------------

### Original longest_str Function (Python)

Source: https://github.com/pschanely/crosshair/blob/main/doc/source/diff_behavior.rst

The initial implementation of a Python function `longest_str` that finds the longest string in a list by iterating through the items.

```python
# foo.py
def longest_str(items: List[str]) -> str:
  longest = ''
  for item in items:
    if len(item) > len(longest):
      longest = item
  return longest
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.