Limitations

A (possibly incomplete) list of limitations. Some of these will be lifted over time (your help is welcome!); some may never be lifted.

• Be aware that the absence of a counterexample does not guarantee that the property holds.

• Symbolic values are implemented as Python proxy values. CrossHair patches the system to maintain a good illusion, but the illusion is not complete. For example, code that cares about the identity values (x is y) may not be correctly analyzed.

• Only function and class definitions at the top level are analyzed (i.e. not when nested inside other functions or classes).

• Only deterministic behavior can be analyzed (i.e. your code always does the same thing when starting with the same values).

  • CrossHair may produce a NotDeterministic error when it detects this.

• Be careful: CrossHair will actually run your code and may apply any arguments to it.

  • CrossHair puts some protections in place (via sys.addaudithook) to prevent disk and network access, but this protection is not perfect (notably, it will not prevent actions taken by C-based modules)

• Consuming values of an iterator or a generator in a pre- or post-condition will produce unexpected behavior.

• SMT solvers have very different perspectives on hard problems and easy problems than humans.

  • Be prepared to be surprised both by what CrossHair can tell you, and what it cannot.