Phillip Schanely
Phillip Schanely
I've found 30 contract counterexamples via CrossHair in the correct solutions. They appear to be largely missing preconditions. Some may result from inconsistent expectations between CrossHair and icontract (especially perhaps...
We're actually running low on important semantic issues, so I'd probably turn next to performance issues - there are some very slow tests that I've just skipped because they take...
Importing CrossHair transitively imports a ~majority of the standard library, because we register patches for it all. It would be better to register patches only for the currently loaded modules...
For now, a straight-up realization is sufficient - just don't crash. This will fix some issues in downstream modules too, like `base64` and `uu`.
Some hypothesis tests at hypothesis-python/tests/cover/test_lookup.py fail under crosshair, revealing that some crosshair proxies aren't emulating the appropriate runtime types, investigate these: * DictKeys * DictValues * ItemsView * re.Match /...
[from `test_assume_has_status_reason`:](https://github.com/HypothesisWorks/hypothesis/actions/runs/10046646626/job/27766587120?pr=4034#step:6:3400) ```python-traceback Traceback (most recent call last): File ".../crosshair/libimpl/builtinslib.py", line 900, in __abs__ return self._unary_op(lambda v: z3.If(v < 0, -v, v)) File ".../crosshair/libimpl/builtinslib.py", line 319, in _unary_op return self.__class__(op(self.var),...
There's a few ways that CrossHair can behave subtly different than CPython. Many path executions won't implement true IEEE float semantics, it could use an impossible set iteration order, etc....
Weak references are inherently non-deterministic. CrossHair right now does nothing special to address this, and so it'll likely raise `NotDeterministic` when executing such code. This issue (or maybe just a...
We use symbolic integers with constant bounds quite often. (container and string lengths, for starters) It **might** make sense to layer in something just above the solver which could track...