001package daikon.diff; 002 003import daikon.PptTopLevel; 004import daikon.inv.Invariant; 005import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 006import org.checkerframework.checker.nullness.qual.MonotonicNonNull; 007import org.checkerframework.checker.nullness.qual.Nullable; 008import org.checkerframework.checker.nullness.qual.RequiresNonNull; 009 010/** Computes A - B, where A and B are the two sets of invariants. */ 011public class MinusVisitor extends DepthFirstVisitor { 012 013 private InvMap result = new InvMap(); 014 private @MonotonicNonNull PptTopLevel currentPpt; 015 016 /** If the first ppt is non-null, it should be part of the result. */ 017 @Override 018 public void visit(PptNode node) { 019 PptTopLevel ppt1 = node.getPpt1(); 020 if (ppt1 != null) { 021 result.addPpt(ppt1); 022 currentPpt = ppt1; 023 super.visit(node); 024 } 025 } 026 027 /** Possibly add the first invariant to the result set. */ 028 @Override 029 @SuppressWarnings( 030 "nullness:contracts.precondition.override" // visitor invariant, because the PptNode has 031 // already been visited 032 ) 033 @RequiresNonNull("currentPpt") 034 public void visit(InvNode node) { 035 Invariant inv1 = node.getInv1(); 036 Invariant inv2 = node.getInv2(); 037 if (shouldAdd(inv1, inv2)) { 038 result.add(currentPpt, inv1); 039 } 040 } 041 042 /** 043 * If the first invariant is non-null and justified, and the second one is null or unjustified, 044 * the first invariant should be added. 045 */ 046 @EnsuresNonNullIf(result = true, expression = "#1") 047 private static boolean shouldAdd(@Nullable Invariant inv1, @Nullable Invariant inv2) { 048 return (inv1 != null) && (inv2 == null); 049 } 050 051 /** Returns the InvMap generated as a result of the traversal. */ 052 public InvMap getResult() { 053 return result; 054 } 055}