typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
997 stars 350 forks source link

Member reference: pre and post conditions should be part of function type #801

Open smillst opened 8 years ago

smillst commented 8 years ago

When comparing the types of method references, the the pre- and post-conditions should be considered.

In contexts such as pseudo-assignments, the pre- and post-conditions should be checked like they are when checking method overriding. Although some may not be useful because post conditions generally refer to fields (but there will be no shared fields). See test case in checker/tests/nullness/java8/methodref/Postconditions.java.

smillst commented 6 years ago

Pre and post conditions are checked for lambdas either. See todo in org.checkerframework.common.basetype.BaseTypeVisitor#visitLambdaExpression.