Package daikon.inv.unary.scalar
Class NonZero
- Object
-
- Invariant
-
- UnaryInvariant
-
- SingleScalar
-
- NonZero
-
- All Implemented Interfaces:
Serializable,Cloneable
public class NonZero extends SingleScalar
Represents long scalars that are non-zero. Prints asx != 0, or asx != nullfor pointer types.- See Also:
- Serialized Form
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from class Invariant
Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match
-
-
Field Summary
Fields Modifier and Type Field Description static LoggerdebugDebug tracer.static booleandkconfig_enabledBoolean.-
Fields inherited from class Invariant
checkedMergeOverridden, CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debugFlow, debugGuarding, debugIsObvious, debugIsWorthPrinting, debugPrint, debugPrintEquality, dkconfig_confidence_limit, dkconfig_fuzzy_ratio, dkconfig_simplify_define_predicates, falsified, invariantEnabledDefault, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED
-
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatusadd_modified(long v, int count)Similar toSingleScalar.check_modified(long, int)except that it can change the state of the invariant if necessary.InvariantStatuscheck_modified(long v, int count)Presents a sample to the invariant.protected doublecomputeConfidence()This method computes the confidence that this invariant occurred by chance.protected doublecomputeProbability()booleanenabled()Returns whether or not this class of invariants is currently enabled.Stringformat_using(OutputFormat format)Return a printed representation of this invariant, in the given format.static NonZeroget_proto()Returns the prototype invariant for NonZeroNonZeroinstantiate_dyn(PptSlice slice)Instantiates (creates) an invariant of the same class on the specified slice.booleaninstantiate_ok(VarInfo[] vis)Returns true if it makes sense to instantiate this invariant over the specified variables.booleanisExclusiveFormula(Invariant other)Returns true iff the two invariants represent mutually exclusive mathematical formulas -- that is, if one of them is true, then the other must be false.@Nullable DiscardInfoisObviousDynamically(VarInfo[] vis)Return non-null if this invariant is necessarily true from a fact that can be determined dynamically (after checking data) -- for the given varInfos rather than the varInfos of this.@Nullable DiscardInfoisObviousStatically(VarInfo[] vis)Return true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this.booleanisSameFormula(Invariant other)Returns true iff the two invariants represent the same mathematical formula.-
Methods inherited from class SingleScalar
add, add_unmodified, check, check_unmodified, valid_types, valid_types_static, var
-
Methods inherited from class UnaryInvariant
resurrect_done
-
Methods inherited from class Invariant
add_sample, asInvClass, checkRep, clear_falsified, clone, clone_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, isObvious, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isSameInvariant, isValidEscExpression, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, merge, mergeFormulasOk, permute, prob_and, prob_and, prob_is_ge, prob_or, repCheck, repr, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames
-
-
-
-
Field Detail
-
dkconfig_enabled
public static boolean dkconfig_enabled
Boolean. True iff NonZero invariants should be considered.
-
-
Method Detail
-
enabled
public boolean enabled()
Description copied from class:InvariantReturns whether or not this class of invariants is currently enabled.Its implementation is almost always
return dkconfig_enabled;.
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
Description copied from class:InvariantReturns true if it makes sense to instantiate this invariant over the specified variables. Checks details beyond what is provided byInvariant.valid_types(daikon.VarInfo[]). This should never be called without calling valid_types() first (implementations should be able to presume that valid_types() returns true).This method does not have to be overridden; the default implementation in Invariant returns true.
- Overrides:
instantiate_okin classInvariant- See Also:
Invariant.valid_types(VarInfo[])
-
instantiate_dyn
public NonZero instantiate_dyn( NonZero this, PptSlice slice)
Description copied from class:InvariantInstantiates (creates) an invariant of the same class on the specified slice. Must be overridden in each class. Must be used rather thanInvariant.clone()so that checks inInvariant.instantiate(daikon.PptSlice)for reasonable invariants are done.The implementation of this method is almost always
return new <em>InvName</em>(slice);- Specified by:
instantiate_dynin classInvariant- Returns:
- the new invariant
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied NonZero this, OutputFormat format)
Description copied from class:InvariantReturn a printed representation of this invariant, in the given format.- Specified by:
format_usingin classInvariant
-
check_modified
public InvariantStatus check_modified(long v, int count)
Description copied from class:SingleScalarPresents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.- Specified by:
check_modifiedin classSingleScalarcount- how many identical samples were observed in a row. For example, three calls to check_modified with a count parameter of 1 is equivalent to one call to check_modified with a count parameter of 3.- Returns:
- whether or not the sample is consistent with the invariant
-
add_modified
public InvariantStatus add_modified(long v, int count)
Description copied from class:SingleScalarSimilar toSingleScalar.check_modified(long, int)except that it can change the state of the invariant if necessary. If the invariant doesn't have any state, then the implementation should simply callSingleScalar.check_modified(long, int). This method need not check for falsification; that is done by the caller.- Specified by:
add_modifiedin classSingleScalar
-
computeConfidence
protected double computeConfidence()
Description copied from class:InvariantThis method computes the confidence that this invariant occurred by chance. Clients should callInvariant.getConfidence()instead.This method need not check the value of field "falsified", as the caller does that.
- Specified by:
computeConfidencein classInvariant- Returns:
- confidence of this invariant
- See Also:
Invariant.getConfidence()
-
computeProbability
protected double computeProbability()
-
isObviousStatically
@Pure public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis)
Description copied from class:InvariantReturn true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this. Conceptually, this means "is this invariant statically obvious if its VarInfos were switched with vis?" Intended to be overridden by subclasses. Should only do static checking.Precondition: vis.length == this.ppt.var_infos.length
- Overrides:
isObviousStaticallyin classInvariant- Parameters:
vis- the VarInfos this invariant is obvious over. The position and data type of the variables is the *same* as that of this.ppt.var_infos.
-
isObviousDynamically
@Pure public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis)
Description copied from class:InvariantReturn non-null if this invariant is necessarily true from a fact that can be determined dynamically (after checking data) -- for the given varInfos rather than the varInfos of this. Conceptually, this means, "Is this invariant dynamically obvious if its VarInfos were switched with vis?" Intended to be overriden by subclasses so they can filter invariants after checking; the overriding method should first call "super.isObviousDynamically(vis)". Since this method is dynamic, it should only be called after all processing.- Overrides:
isObviousDynamicallyin classInvariant
-
isSameFormula
@Pure public boolean isSameFormula(Invariant other)
Description copied from class:InvariantReturns true iff the two invariants represent the same mathematical formula. Does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities. As a rule of thumb, if two invariants format the same, this method returns true. Furthermore, in many cases, if an invariant does not involve computed constants (as "x>c" and "y=ax+b" do for constants a, b, and c), then this method vacuously returns true.- Specified by:
isSameFormulain classInvariant- Parameters:
other- the invariant to compare to this one- Returns:
- true iff the two invariants represent the same mathematical formula. Does not consider
-
isExclusiveFormula
@Pure public boolean isExclusiveFormula(Invariant other)
Description copied from class:InvariantReturns true iff the two invariants represent mutually exclusive mathematical formulas -- that is, if one of them is true, then the other must be false. This method does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities.- Overrides:
isExclusiveFormulain classInvariant- Parameters:
other- the other invariant to compare to this one- Returns:
- true iff the two invariants represent mutually exclusive mathematical formulas
-
-