Skip to content

Commit 91cb39f

Browse files
committed
Add JavaDoc
1 parent f9a30ff commit 91cb39f

1 file changed

Lines changed: 5 additions & 0 deletions

File tree

  • liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,11 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
101101
return constr;
102102
}
103103

104+
/**
105+
* Performs a best-effort satisfiability check for a refinement reporting a warning if unsat. Runs an SMT check on a
106+
* temporary scope and if the refinement mentions other names that are still unavailable at this point, the SMT
107+
* check fails and that failure is ignored.
108+
*/
104109
private void checkRefinementSatisfiability(String refinement, Predicate predicate, CtElement element) {
105110
context.enterContext();
106111
try {

0 commit comments

Comments
 (0)