Class NISuppressor


  • public class NISuppressor
    extends Object
    Class that defines a suppressor invariant for use in non-instantiating suppressions. In non-instantiating suppressions, suppressor invariants are defined independent of specific variables. Instead, arguments are identified by their variable index in the suppressee.
    • Field Detail

      • debug

        public static final Logger debug
        Debug tracer.
    • Method Detail

      • swap

        public NISuppressor swap()
        Returns a new suppressor that is the same as this one except with its variables swapped. Unary suppressors have their variable index swapped from 0 to 1 or 1 to 0.
      • is_enabled

        @Pure
        public boolean is_enabled()
        Returns whether or not this suppressor is enabled. A suppressor is enabled if the invariant on which it depends is enabled.
      • instantiate_ok

        public boolean instantiate_ok​(VarInfo[] vis)
        Returns whether or not this suppressor invariant could be instantiated over the specified variables. A suppressor that canot be instantiated over the variables cannot possibly suppress. Consider the NonZero invariant. It is suppressed by EqualsOne. But while NonZero is valid over all variables, EqualsOne is only valid over non-pointer variables. Thus the suppression is only valid over non-pointer variables.
      • check

        public NIS.SuppressState check​(PptTopLevel ppt,
                                       VarInfo[] vis,
                                       @Nullable Invariant inv)
        Sets the status of this suppressor with regards to the specified vis and falsified invariant. The status consists of whether or not the suppressor is valid (true) and whether or not it matches the falsified invariant.

        Matching a suppressor is more complex than is apparent at first glance. The invariant AND its variables must match. Since suppressors are specified without variables, the variables are taken from the specified vis. The variable indices specify which variables to consider.

        For example consider the suppressor {1, 2, IntLessEqual} and a vis of {x, y, z}. The suppressor is true if the IntLessEqual invariant exists in the slice {y, z}. This allows ternary invariants to specify exactly the suppressor required for their particular permutation ofarguments. Invariants that have an internal permute variable must match that as well.

        Parameters:
        ppt - the top level program point
        vis - the slice of the suppressee. Thus, if the suppressee is ternary, vis, should specify three variables.
        inv - the falsified invariant. inv_match indicates whether or not inv matches this suppressor.
        Returns:
        the state of this suppressor which is one of (NIS.SuppressState.MATCH, NIS.SuppressState.VALID, NIS.SuppressState.INVALID, NIS.SuppressState.NONSENSICAL)
      • match

        public boolean match​(Invariant inv)
        Returns true if inv matches this suppressor. It is assumed that inv's variables already match (i.e., that it was looked up in compatible slice).
      • match

        public boolean match​(NISuppressee sse)
        Returns true if the suppressee matches this suppressor. Currently only checks that the class matches but this will need to be expanded to check for a permutation match as well.
      • clear_state

        public void clear_state()
        clears the state of this suppressor to NIS.none
      • toString

        @SideEffectFree
        public String toString​(@GuardSatisfied NISuppressor this)
        Returns a string representation of the suppressor. Rather than show var indices as numbers, the variables x, y, and z are shown instead with indices 0, 1, and 2 respectively.
        Overrides:
        toString in class Object