Add an option to check all functions as if they had post: True

[Zac-HD]

When I'm getting started, I often have a module full of type-annotated code but no CrossHair compatible docstrings. As a quick way to get started, it would be great to have an option to treat all functions as if they had a docstring containing post: True.

This would save some time initially, but also work well with an "assert all your postconditions" style - we'd then only use docstrings for preconditions and invariants.

(which raises a related issue: does CrossHair use information from assertions for interproceedural analysis? Doing so would make this style considerably more efficient...)

[pschanely]

Does CrossHair use information from assertions for interprocedural analysis?

It's complicated! CrossHair does interprocedural analysis in two ways: One of those (the most common way) is that it simply runs the code of the callee symbolically. In that sense, asserts in the callee are confirmed, and can be relied on in the caller. As for the second way, CrossHair will sometimes skip over the body of the callee - instead it will just check the preconditions and assert the postconditions on fresh symbolic values. The second way cannot see assert statements in the body of the callee.

At any rate, I like this idea.

I am not sure how quickly issues around other CrossHair directives like allowed exceptions ("raises:") and class invariants ("inv:") come up. I suppose one can simply repeat themselves for class invariants. More CrossHair usages in the wild would help inform us how frequently these features are needed.

I think the precondition inference idea in #27 is pretty important for making this work; I am hard pressed to imagine the kinds of python files that would clearly not require preconditions.

Finally, I suspect that we don't want to allow this option when checking a directory tree. CrossHair actually executes code, so it will blindly and happily run your functions that do filesystem mutations, etc.

[pschanely]

One very minor update related to this issue: CrossHair presently checks any function that has a precondition (or a leading assert in --analysis_kind=asserts mode), effectively looking for exceptions/assertions in those functions (and, as always, recursively in subroutines).

So, there no reason to add post: True if you've already got a precondition.