Package daikon.inv

Class DiscardCode

  • All Implemented Interfaces:
    Serializable, Comparable<DiscardCode>
    public class DiscardCode
extends Object
implements Comparable<DiscardCode>, Serializable
    DiscardCode is an enumeration type. It represents reasons why an invariant is falsified or disregarded. Methods that decide whether an Invariant should be printed later (such as isObviousImplied()), side effect Invariants to contain DiscardCode instances in their discardCode field slot.

    The different elements of the enumeration are:

    obvious // is implied by other already known invariants

    bad_sample // is falsified by a seen example

    bad_confidence // has an unjustified confidence

    (unused) // was few_modified_samples

    not_enough_samples // not enough samples seen for the Invariant

    non_canonical_var // expression involves a non-canonical variable

    implied_post_condition // implied by some prestate conditions

    only_constant_vars // expression for invariant only contains constant variables

    derived_param // has a VarInfo that has derived and uninteresting param

    unmodified_var // invariant discarded because it says some var hasn't been modified

    control_check // if discarded due to the ControlledInvariantFilter

    exact // isExact() fails

    var_filtered // Doesn't contain a desirable variable

    filtered // filtered by some other means not in the above list

    There is no representation for an invariant that is *not* discarded; don't use a DiscardCode in that situation.

    See Also:
    Serialized Form

    • Field Detail

      • obvious

        public static final DiscardCode obvious
        used when an invariant is implied by other known invariants

      • bad_sample

        public static final DiscardCode bad_sample
        used when an invariant is falsified by a seen example

      • derived_param

        public static final DiscardCode derived_param
        used when an invariant's VarInfo returns true for isDerivedParamAndUninteresting()

      • control_check

        public static final DiscardCode control_check
        used for invariants discarded because of the ControlledInvariantsFilter

      • exact

        public static final DiscardCode exact
        used for invariants discarded when isExact() fails

      • var_filtered

        public static final DiscardCode var_filtered
        used for invariants that don't contain desired variables

      • filtered

        public static final DiscardCode filtered
        used for invariants that are filtered by some means not in the above list

      • enumValue

        public final int enumValue
        Each member of the enumeration is associated with a distinct int for comparability.

    • Method Detail

      • compareTo

        @Pure
public int compareTo​(@GuardSatisfied DiscardCode this,
                     DiscardCode o)
        The enumeration members in sorted order:
        obvious, bad_sample, bad_confidence, [unused], not_enough_samples, non_canonical_var,
        implied_post_condition, only_constant_vars, derived_param, unmodified_var, control_check, exact, var filter
        Specified by:
        compareTo in interface Comparable<DiscardCode>
        Returns:
        this.enumValue.compareTo(o.enumValue) where the enumValue are treated as Integers
        Throws:
        ClassCastException - iff !(o instanceof DiscardCode)

      • toString

        @SideEffectFree
public String toString​(@GuardSatisfied DiscardCode this)
        Prints out a string describing the reason for discard.
        Overrides:
        toString in class Object
        Returns:
        one of {"Not discarded", "Obvious, "Bad sample seen", "Unjustified confidence", "Few modified samples", "Not enough samples", "Non-canonical variable", "Implied post state", "Only constant variables in this expression", "Derived Param", "Control Check", "Exact", "Variable Filter", "Filtered"}