Issue warnings when top is passed as a pre/postcondition qualifier #6409
Conversation
| @@ -1280,6 +1280,8 @@ private void checkContractsAtMethodDeclaration( | |||
| contract.viewpointAdaptDependentTypeAnnotation( | |||
| atypeFactory, stringToJavaExpr, methodTree); | |||
|
|
|||
| checkValidRefinementContract(annotation, contract.kind, methodTree); | |||
There was a problem hiding this comment.
@mernst I understand that we initially discussed implementing this check in the implementation of BaseTypeVisitor#visitAnnotation, but I found that the contracts were already available in this method.
Let me know if this is an issue and I can go back to the original plan.
There was a problem hiding this comment.
As expected, I had to move the check into BaseTypeVisitor#visitAnnotation
|
I believe the failing tests are due to "implicit" pre/postconditions also being checked by the new logic, will need to investigate. |
| ExecutableElement methodElement = TreeUtils.elementFromDeclaration(methodTree); | ||
| Set<Contract> contracts = atypeFactory.getContractsFromMethod().getContracts(methodElement); |
There was a problem hiding this comment.
@smillst To me, this feels like a very roundabout way to get the annotations for a method (specifically, the contract annotations like @EnsuresQualifier or @EnsuresQualifierIf) when we're already visiting the annotation itself; do you know of a better API that lets me get this directly without having to go through the methodTree?
|
Closing in favour of #6412 |
No description provided.