Issue warnings when top is passed as a pre/postcondition qualifier#6409
Issue warnings when top is passed as a pre/postcondition qualifier#6409jyoo980 wants to merge 4 commits into
Conversation
| 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 |
1 participant
No description provided.