Conversation
rcosta358
added
enhancement
CatarinaGamboa
left a comment
CatarinaGamboa
left a comment
There was a problem hiding this comment.
I think I need some description of our approach on this. So we check satisfiability every time that we try to get the value of a @Refinement (and skip if it already has it). But why do we need to add the vars to context? what if a refinements mentions several params that are not yet in context?
| return constr; | ||
| } | ||
|
|
||
| private void checkRefinementSatisfiability(String refinement, Predicate predicate, CtElement element) { |
| CtTypeReference<?> annotationType = element instanceof CtTypedElement<?> typedElement | ||
| ? typedElement.getType() : null; | ||
| if (annotationType != null && !context.hasVariable(Keys.WILDCARD)) | ||
| context.addVarToContext(Keys.WILDCARD, annotationType, p, element); |
There was a problem hiding this comment.
I'm a bit confused, why are we adding the vars to context here? because this happens before we add them to context?
|
We do the satisfiability check once per element inside a temporary scope. We add names like |
2 participants
This PR adds a warning for unsatisfiable, self-contradictory refinements. It also avoids re-running the same satisfiability check for the same element across verifier passes.
Examples