Skip to content

Commit

Permalink
Disable checking of contracts. (#183)
Browse files Browse the repository at this point in the history
We've historically accomplished this with `-AsuppressWarnings`, but this
CL's solution may be more general. Also, it avoids running some code
entirely, which saves us from having to keep that code updated for the
very new JDKs that we run with. (It might also help performance if we're
lucky, and maybe it moves us a step closer to not needing JavaParser
(though that may be on the way out, anyway).)
  • Loading branch information
cpovirk authored Jul 9, 2024
1 parent 5194e00 commit aa63538
Showing 1 changed file with 26 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,10 @@
import org.checkerframework.framework.type.typeannotator.TypeAnnotator;
import org.checkerframework.framework.type.visitor.AnnotatedTypeVisitor;
import org.checkerframework.framework.util.AnnotationFormatter;
import org.checkerframework.framework.util.Contract.ConditionalPostcondition;
import org.checkerframework.framework.util.Contract.Postcondition;
import org.checkerframework.framework.util.Contract.Precondition;
import org.checkerframework.framework.util.ContractsFromMethod;
import org.checkerframework.framework.util.DefaultAnnotationFormatter;
import org.checkerframework.framework.util.DefaultQualifierKindHierarchy;
import org.checkerframework.framework.util.QualifierKindHierarchy;
Expand Down Expand Up @@ -919,6 +923,28 @@ public boolean applyConservativeDefaults(Element annotationScope) {
}
}

// Disable checking of contracts.
@Override
protected ContractsFromMethod createContractsFromMethod() {
return new ContractsFromMethod(this) {
@Override
public Set<ConditionalPostcondition> getConditionalPostconditions(
ExecutableElement methodElement) {
return emptySet();
}

@Override
public Set<Precondition> getPreconditions(ExecutableElement executableElement) {
return emptySet();
}

@Override
public Set<Postcondition> getPostconditions(ExecutableElement executableElement) {
return emptySet();
}
};
}

@Override
protected void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow) {
super.addComputedTypeAnnotations(
Expand Down

0 comments on commit aa63538

Please sign in to comment.