Next: Front ends and instrumentation, Previous: Daikon output, Up: Top [Contents][Index]

## 6 Enhancing Daikon output

Next: Conditional invariants, Up: Enhancing Daikon output [Contents][Index]

### 6.1 Configuration options

Many aspects of Daikon’s behavior can be controlled by setting various configuration parameters. These configuration parameters control which invariants are checked and reported, the statistical tests for invariants, which derived variables are created, and more.

There are two ways to set configuration options. You can specify a configuration setting directly on the command line, using the `--config_option name=value` option (which you may repeat as many times as you want). Or, you can create a configuration file and supplying it to Daikon on the command line using the `--config filename` option. Daikon applies all the command-line arguments in order. You may wish to use the supplied example configuration file `daikon/java/daikon/config/example-settings.txt` as an example when creating your own configuration files. (If you did not download Daikon’s sources, you must extract the example from `daikon.jar` to read it.)

You can also control Daikon’s output via its command-line options (see Running Daikon) and via the command-line options to its front ends — such as DynComp (see DynComp for Java options), Chicory (see Chicory options) or Kvasir (see Kvasir options).

The configuration options are different from the debugging flags `--debug` and `--dbg category` (see Daikon debugging options). The debugging flags permit Daikon to produce debugging output, but they do not affect the invariants that Daikon computes.

Up: Configuration options [Contents][Index]

#### 6.1.1 List of configuration options

This is a list of all Daikon configuration options. The configuration option name contains the Java class in which it is defined. (In the Daikon source code, the configuration value is stored in a variable whose name contains a `dkconfig_` prefix, but that should be irrelevant to users.) To learn more about a specific invariant or derived variable than appears in this manual, see its source code.

Next: Options to enable/disable specific invariants, Previous: List of configuration options, Up: List of configuration options [Contents][Index]

#### 6.1.1.1 Options to enable/disable filters

These configuration options enable or disable filters that suppress printing of certain invariants. Invariants are filtered if they are redundant. See Invariant filters, for more information. Also see configuration option `daikon.PrintInvariants.print_all`.

`daikon.inv.filter.DerivedParameterFilter.enabled`

  Boolean. If true, DerivedParameterFilter is initially turned on. The default value is ‘true’.

`daikon.inv.filter.DotNetStringFilter.enabled`

  Boolean. If true, DotNetStringFilter is initially turned on. See its Javadoc. The default value is ‘false’.

`daikon.inv.filter.ObviousFilter.enabled`

  Boolean. If true, ObviousFilter is initially turned on. The default value is ‘true’.

`daikon.inv.filter.OnlyConstantVariablesFilter.enabled`

  Boolean. If true, OnlyConstantVariablesFilter is initially turned on. The default value is ‘true’.

`daikon.inv.filter.ParentFilter.enabled`

  Boolean. If true, ParentFilter is initially turned on. The default value is ‘true’.

`daikon.inv.filter.ReadonlyPrestateFilter.enabled`

  Boolean. If true, ReadonlyPrestateFilter is initially turned on. The default value is ‘true’.

`daikon.inv.filter.SimplifyFilter.enabled`

  Boolean. If true, SimplifyFilter is initially turned on. The default value is ‘true’.

`daikon.inv.filter.UnjustifiedFilter.enabled`

  Boolean. If true, UnjustifiedFilter is initially turned on. The default value is ‘true’.

`daikon.inv.filter.UnmodifiedVariableEqualityFilter.enabled`

  Boolean. If true, UnmodifiedVariableEqualityFilter is initially turned on. The default value is ‘true’.

Next: Other invariant configuration parameters, Previous: Options to enable/disable filters, Up: List of configuration options [Contents][Index]

#### 6.1.1.2 Options to enable/disable specific invariants

These options control whether Daikon looks for specific kinds of invariants. See Invariant list, for more information about the corresponding invariants.

`daikon.inv.binary.sequenceScalar.Member.enabled`

  Boolean. True iff Member invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.MemberFloat.enabled`

  Boolean. True iff Member invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqFloatEqual.enabled`

  Boolean. True iff SeqFloatEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqFloatGreaterEqual.enabled`

  Boolean. True iff SeqFloatGreaterEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqFloatGreaterThan.enabled`

  Boolean. True iff SeqFloatGreaterThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqFloatLessEqual.enabled`

  Boolean. True iff SeqFloatLessEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqFloatLessThan.enabled`

  Boolean. True iff SeqFloatLessThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqIntEqual.enabled`

  Boolean. True iff SeqIntEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqIntGreaterEqual.enabled`

  Boolean. True iff SeqIntGreaterEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqIntGreaterThan.enabled`

  Boolean. True iff SeqIntGreaterThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqIntLessEqual.enabled`

  Boolean. True iff SeqIntLessEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceScalar.SeqIntLessThan.enabled`

  Boolean. True iff SeqIntLessThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.sequenceString.MemberString.enabled`

  Boolean. True iff Member invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.FloatEqual.enabled`

  Boolean. True iff FloatEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.FloatGreaterEqual.enabled`

  Boolean. True iff FloatGreaterEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.FloatGreaterThan.enabled`

  Boolean. True iff FloatGreaterThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.FloatLessEqual.enabled`

  Boolean. True iff FloatLessEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.FloatLessThan.enabled`

  Boolean. True iff FloatLessThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.FloatNonEqual.enabled`

  Boolean. True iff FloatNonEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.IntEqual.enabled`

  Boolean. True iff IntEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.IntGreaterEqual.enabled`

  Boolean. True iff IntGreaterEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.IntGreaterThan.enabled`

  Boolean. True iff IntGreaterThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.IntLessEqual.enabled`

  Boolean. True iff IntLessEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.IntLessThan.enabled`

  Boolean. True iff IntLessThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.IntNonEqual.enabled`

  Boolean. True iff IntNonEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.LinearBinary.enabled`

  Boolean. True iff LinearBinary invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.LinearBinaryFloat.enabled`

  Boolean. True iff LinearBinary invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.NumericFloat.Divides.enabled`

  Boolean. True iff divides invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.NumericFloat.Square.enabled`

  Boolean. True iff square invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.NumericFloat.ZeroTrack.enabled`

  Boolean. True iff zero-track invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoScalar.NumericInt.BitwiseAndZero.enabled`

  Boolean. True iff BitwiseAndZero invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoScalar.NumericInt.BitwiseComplement.enabled`

  Boolean. True iff bitwise complement invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoScalar.NumericInt.BitwiseSubset.enabled`

  Boolean. True iff bitwise subset invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoScalar.NumericInt.Divides.enabled`

  Boolean. True iff divides invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.NumericInt.ShiftZero.enabled`

  Boolean. True iff ShiftZero invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoScalar.NumericInt.Square.enabled`

  Boolean. True iff square invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoScalar.NumericInt.ZeroTrack.enabled`

  Boolean. True iff zero-track invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.PairwiseFloatEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseFloatGreaterEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseFloatGreaterThan.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseFloatLessEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseFloatLessThan.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseIntEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseIntGreaterEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseIntGreaterThan.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseIntLessEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseIntLessThan.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseLinearBinary.enabled`

  Boolean. True iff PairwiseLinearBinary invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseLinearBinaryFloat.enabled`

  Boolean. True iff PairwiseLinearBinary invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseNumericFloat.Divides.enabled`

  Boolean. True iff divides invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseNumericFloat.Square.enabled`

  Boolean. True iff square invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseNumericFloat.ZeroTrack.enabled`

  Boolean. True iff zero-track invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseAndZero.enabled`

  Boolean. True iff BitwiseAndZero invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseComplement.enabled`

  Boolean. True iff bitwise complement invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseSubset.enabled`

  Boolean. True iff bitwise subset invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.PairwiseNumericInt.Divides.enabled`

  Boolean. True iff divides invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseNumericInt.ShiftZero.enabled`

  Boolean. True iff ShiftZero invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.PairwiseNumericInt.Square.enabled`

  Boolean. True iff square invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseNumericInt.ZeroTrack.enabled`

  Boolean. True iff zero-track invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.PairwiseString.SubString.enabled`

  Boolean. True iff SubString invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.PairwiseStringEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseStringGreaterEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseStringGreaterThan.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseStringLessEqual.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.PairwiseStringLessThan.enabled`

  Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.Reverse.enabled`

  Boolean. True iff Reverse invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.ReverseFloat.enabled`

  Boolean. True iff Reverse invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqFloatEqual.enabled`

  Boolean. True iff SeqSeqFloatEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqFloatGreaterEqual.enabled`

  Boolean. True iff SeqSeqFloatGreaterEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqFloatGreaterThan.enabled`

  Boolean. True iff SeqSeqFloatGreaterThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqFloatLessEqual.enabled`

  Boolean. True iff SeqSeqFloatLessEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqFloatLessThan.enabled`

  Boolean. True iff SeqSeqFloatLessThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqIntEqual.enabled`

  Boolean. True iff SeqSeqIntEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqIntGreaterEqual.enabled`

  Boolean. True iff SeqSeqIntGreaterEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqIntGreaterThan.enabled`

  Boolean. True iff SeqSeqIntGreaterThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqIntLessEqual.enabled`

  Boolean. True iff SeqSeqIntLessEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqIntLessThan.enabled`

  Boolean. True iff SeqSeqIntLessThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqStringEqual.enabled`

  Boolean. True iff SeqSeqStringEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqStringGreaterEqual.enabled`

  Boolean. True iff SeqSeqStringGreaterEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqStringGreaterThan.enabled`

  Boolean. True iff SeqSeqStringGreaterThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqStringLessEqual.enabled`

  Boolean. True iff SeqSeqStringLessEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SeqSeqStringLessThan.enabled`

  Boolean. True iff SeqSeqStringLessThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoSequence.SubSequence.enabled`

  Boolean. True iff SubSequence invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.SubSequenceFloat.enabled`

  Boolean. True iff SubSequence invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.SubSet.enabled`

  Boolean. True iff SubSet invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.SubSetFloat.enabled`

  Boolean. True iff SubSet invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.SuperSequence.enabled`

  Boolean. True iff SubSequence invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.SuperSequenceFloat.enabled`

  Boolean. True iff SubSequence invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.SuperSet.enabled`

  Boolean. True iff SubSet invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoSequence.SuperSetFloat.enabled`

  Boolean. True iff SubSet invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoString.StdString.SubString.enabled`

  Boolean. True iff SubString invariants should be considered. The default value is ‘false’.

`daikon.inv.binary.twoString.StringEqual.enabled`

  Boolean. True iff StringEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoString.StringGreaterEqual.enabled`

  Boolean. True iff StringGreaterEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoString.StringGreaterThan.enabled`

  Boolean. True iff StringGreaterThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoString.StringLessEqual.enabled`

  Boolean. True iff StringLessEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoString.StringLessThan.enabled`

  Boolean. True iff StringLessThan invariants should be considered. The default value is ‘true’.

`daikon.inv.binary.twoString.StringNonEqual.enabled`

  Boolean. True iff StringNonEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.ternary.threeScalar.FunctionBinary.enabled`

  Boolean. True if FunctionBinary invariants should be considered. The default value is ‘false’.

`daikon.inv.ternary.threeScalar.FunctionBinaryFloat.enabled`

  Boolean. True if FunctionBinaryFloat invariants should be considered. The default value is ‘false’.

`daikon.inv.ternary.threeScalar.LinearTernary.enabled`

  Boolean. True iff LinearTernary invariants should be considered. The default value is ‘true’.

`daikon.inv.ternary.threeScalar.LinearTernaryFloat.enabled`

  Boolean. True iff LinearTernary invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.CompleteOneOfScalar.enabled`

  Boolean. True iff CompleteOneOfScalar invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.scalar.IsPointer.enabled`

  Boolean. True iff IsPointer invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.scalar.LowerBound.enabled`

  Boolean. True iff LowerBound invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.LowerBoundFloat.enabled`

  Boolean. True iff LowerBoundFloat invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.Modulus.enabled`

  Boolean. True iff Modulus invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.scalar.NonModulus.enabled`

  Boolean. True iff NonModulus invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.scalar.NonZero.enabled`

  Boolean. True iff NonZero invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.NonZeroFloat.enabled`

  Boolean. True iff NonZeroFloat invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.OneOfFloat.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.OneOfScalar.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.Positive.enabled`

  Boolean. True iff Positive invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.RangeInt.Even.enabled`

  Boolean. True if Even invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.scalar.RangeInt.PowerOfTwo.enabled`

  Boolean. True if PowerOfTwo invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.UpperBound.enabled`

  Boolean. True iff UpperBound invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.scalar.UpperBoundFloat.enabled`

  Boolean. True iff UpperBoundFloat invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.CommonFloatSequence.enabled`

  Boolean. True iff CommonSequence invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.CommonSequence.enabled`

  Boolean. True iff CommonSequence invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.EltLowerBound.enabled`

  Boolean. True iff EltLowerBound invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltLowerBoundFloat.enabled`

  Boolean. True iff EltLowerBoundFloat invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltNonZero.enabled`

  Boolean. True iff EltNonZero invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltNonZeroFloat.enabled`

  Boolean. True iff EltNonZero invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltOneOf.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltOneOfFloat.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltRangeInt.Even.enabled`

  Boolean. True if Even invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.EltRangeInt.PowerOfTwo.enabled`

  Boolean. True if PowerOfTwo invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltUpperBound.enabled`

  Boolean. True iff EltUpperBound invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltUpperBoundFloat.enabled`

  Boolean. True iff EltUpperBoundFloat invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseFloatEqual.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseFloatGreaterEqual.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseFloatGreaterThan.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseFloatLessEqual.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseFloatLessThan.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseIntEqual.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseIntGreaterEqual.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseIntGreaterThan.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseIntLessEqual.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.EltwiseIntLessThan.enabled`

  Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.NoDuplicates.enabled`

  Boolean. True iff NoDuplicates invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.NoDuplicatesFloat.enabled`

  Boolean. True iff NoDuplicates invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.OneOfFloatSequence.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.OneOfSequence.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.sequence.SeqIndexFloatEqual.enabled`

  Boolean. True iff SeqIndexFloatEqual invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexFloatGreaterEqual.enabled`

  Boolean. True iff SeqIndexFloatGreaterEqual invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexFloatGreaterThan.enabled`

  Boolean. True iff SeqIndexFloatGreaterThan invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexFloatLessEqual.enabled`

  Boolean. True iff SeqIndexFloatLessEqual invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexFloatLessThan.enabled`

  Boolean. True iff SeqIndexFloatLessThan invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexFloatNonEqual.enabled`

  Boolean. True iff SeqIndexFloatNonEqual invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexIntEqual.enabled`

  Boolean. True iff SeqIndexIntEqual invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexIntGreaterEqual.enabled`

  Boolean. True iff SeqIndexIntGreaterEqual invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexIntGreaterThan.enabled`

  Boolean. True iff SeqIndexIntGreaterThan invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexIntLessEqual.enabled`

  Boolean. True iff SeqIndexIntLessEqual invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexIntLessThan.enabled`

  Boolean. True iff SeqIndexIntLessThan invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.sequence.SeqIndexIntNonEqual.enabled`

  Boolean. True iff SeqIndexIntNonEqual invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.string.CompleteOneOfString.enabled`

  Boolean. True iff CompleteOneOfString invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.string.OneOfString.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.string.PrintableString.enabled`

  Boolean. True iff PrintableString invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.stringsequence.CommonStringSequence.enabled`

  Boolean. True iff CommonStringSequence invariants should be considered. The default value is ‘false’.

`daikon.inv.unary.stringsequence.EltOneOfString.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

`daikon.inv.unary.stringsequence.OneOfStringSequence.enabled`

  Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.

Next: Options to enable/disable derived variables, Previous: Options to enable/disable specific invariants, Up: List of configuration options [Contents][Index]

#### 6.1.1.3 Other invariant configuration parameters

The configuration options listed in this section parameterize the behavior of certain invariants. See Invariant list, for more information about the invariants.

`daikon.inv.Invariant.confidence_limit`

  Floating-point number between 0 and 1. Invariants are displayed only if the confidence that the invariant did not occur by chance is greater than this. (May also be set via the `--conf_limit` command-line option to Daikon; refer to manual.) The default value is ‘0.99’.

`daikon.inv.Invariant.fuzzy_ratio`

  Floating-point number between 0 and 0.1, representing the maximum relative difference between two floats for fuzzy comparisons. Larger values will result in floats that are relatively farther apart being treated as equal. A value of 0 essentially disables fuzzy comparisons. Specifically, if `abs(1 - f1/f2)` is less than or equal to this value, then the two doubles (`f1` and `f2`) will be treated as equal by Daikon. The default value is ‘1.0E-4’.

`daikon.inv.Invariant.simplify_define_predicates`

  A boolean value. If true, Daikon’s Simplify output (printed when the `--format simplify` flag is enabled, and used internally by `--suppress_redundant`) will include new predicates representing some complex relationships in invariants, such as lexical ordering among sequences. If false, some complex relationships will appear in the output as complex quantified formulas, while others will not appear at all. When enabled, Simplify may be able to make more inferences, allowing `--suppress_redundant` to suppress more redundant invariants, but Simplify may also run more slowly. The default value is ‘false’.

`daikon.inv.binary.twoScalar.IntNonEqual.integral_only`

  Boolean. True iff IntNonEqual invariants should be considered. The default value is ‘true’.

`daikon.inv.filter.DerivedVariableFilter.class_re`

  Regular expression to match against the class name of derived variables. Invariants that contain derived variables that match will be filtered out. If null, nothing will be filtered out. The default value is ‘null’.

`daikon.inv.unary.scalar.LowerBound.maximal_interesting`

  Long integer. Together with the corresponding `minimal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of LowerBound invariants whose cutoff was one of (-1,0,1,2). The default value is ‘2’.

`daikon.inv.unary.scalar.LowerBound.minimal_interesting`

  Long integer. Together with the corresponding `maximal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of LowerBound invariants whose cutoff was one of (-1,0,1,2). The default value is ‘-1’.

`daikon.inv.unary.scalar.LowerBoundFloat.maximal_interesting`

  Long integer. Together with the corresponding `minimal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of LowerBoundFloat invariants whose cutoff was one of (-1,0,1,2). The default value is ‘2’.

`daikon.inv.unary.scalar.LowerBoundFloat.minimal_interesting`

  Long integer. Together with the corresponding `maximal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of LowerBoundFloat invariants whose cutoff was one of (-1,0,1,2). The default value is ‘-1’.

`daikon.inv.unary.scalar.OneOfFloat.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘3’.

`daikon.inv.unary.scalar.OneOfScalar.omit_hashcode_values_Simplify`

  Boolean. If true, invariants describing hashcode-typed variables as having any particular value will have an artificial value substituted for the exact hashhode values. The artificial values will stay the same from run to run even if the actual hashcode values change (as long as the OneOf invariants remain the same). If false, hashcodes will be formatted as the application of a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode. One might wish to omit the exact values of the hashcodes because they are usually uninteresting; this is the same reason they print in the native Daikon format, for instance, as `var has only one value` rather than `var == 150924732`. The default value is ‘false’.

`daikon.inv.unary.scalar.OneOfScalar.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘3’.

`daikon.inv.unary.scalar.UpperBound.maximal_interesting`

  Long integer. Together with the corresponding `minimal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of UpperBound invariants whose cutoff was one of (-1,0,1,2). The default value is ‘2’.

`daikon.inv.unary.scalar.UpperBound.minimal_interesting`

  Long integer. Together with the corresponding `maximal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of UpperBound invariants whose cutoff was one of (-1,0,1,2). The default value is ‘-1’.

`daikon.inv.unary.scalar.UpperBoundFloat.maximal_interesting`

  Long integer. Together with the corresponding `minimal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of UpperBoundFloat invariants whose cutoff was one of (-1,0,1,2). The default value is ‘2’.

`daikon.inv.unary.scalar.UpperBoundFloat.minimal_interesting`

  Long integer. Together with the corresponding `maximal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of UpperBoundFloat invariants whose cutoff was one of (-1,0,1,2). The default value is ‘-1’.

`daikon.inv.unary.sequence.CommonFloatSequence.hashcode_seqs`

  Boolean. Set to true to consider common sequences over hashcodes (pointers). The default value is ‘false’.

`daikon.inv.unary.sequence.CommonSequence.hashcode_seqs`

  Boolean. Set to true to consider common sequences over hashcodes (pointers). The default value is ‘false’.

`daikon.inv.unary.sequence.EltLowerBound.maximal_interesting`

  Long integer. Together with the corresponding `minimal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of EltLowerBound invariants whose cutoff was one of (-1,0,1,2). The default value is ‘2’.

`daikon.inv.unary.sequence.EltLowerBound.minimal_interesting`

  Long integer. Together with the corresponding `maximal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of EltLowerBound invariants whose cutoff was one of (-1,0,1,2). The default value is ‘-1’.

`daikon.inv.unary.sequence.EltLowerBoundFloat.maximal_interesting`

  Long integer. Together with the corresponding `minimal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of EltLowerBoundFloat invariants whose cutoff was one of (-1,0,1,2). The default value is ‘2’.

`daikon.inv.unary.sequence.EltLowerBoundFloat.minimal_interesting`

  Long integer. Together with the corresponding `maximal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of EltLowerBoundFloat invariants whose cutoff was one of (-1,0,1,2). The default value is ‘-1’.

`daikon.inv.unary.sequence.EltOneOf.omit_hashcode_values_Simplify`

  Boolean. If true, invariants describing hashcode-typed variables as having any particular value will have an artificial value substituted for the exact hashhode values. The artificial values will stay the same from run to run even if the actual hashcode values change (as long as the OneOf invariants remain the same). If false, hashcodes will be formatted as the application of a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode. One might wish to omit the exact values of the hashcodes because they are usually uninteresting; this is the same reason they print in the native Daikon format, for instance, as `var has only one value` rather than `var == 150924732`. The default value is ‘false’.

`daikon.inv.unary.sequence.EltOneOf.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘3’.

`daikon.inv.unary.sequence.EltOneOfFloat.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘3’.

`daikon.inv.unary.sequence.EltUpperBound.maximal_interesting`

  Long integer. Together with the corresponding `minimal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of EltUpperBound invariants whose cutoff was one of (-1,0,1,2). The default value is ‘2’.

`daikon.inv.unary.sequence.EltUpperBound.minimal_interesting`

  Long integer. Together with the corresponding `maximal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of EltUpperBound invariants whose cutoff was one of (-1,0,1,2). The default value is ‘-1’.

`daikon.inv.unary.sequence.EltUpperBoundFloat.maximal_interesting`

  Long integer. Together with the corresponding `minimal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of EltUpperBoundFloat invariants whose cutoff was one of (-1,0,1,2). The default value is ‘2’.

`daikon.inv.unary.sequence.EltUpperBoundFloat.minimal_interesting`

  Long integer. Together with the corresponding `maximal_interesting` parameter, specifies the range of the computed constant that is “interesting” — the range that should be reported. For instance, setting `minimal_interesting` to -1 and `maximal_interesting` to 2 would only permit output of EltUpperBoundFloat invariants whose cutoff was one of (-1,0,1,2). The default value is ‘-1’.

`daikon.inv.unary.sequence.OneOfFloatSequence.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘3’.

`daikon.inv.unary.sequence.OneOfSequence.omit_hashcode_values_Simplify`

  Boolean. If true, invariants describing hashcode-typed variables as having any particular value will have an artificial value substituted for the exact hashhode values. The artificial values will stay the same from run to run even if the actual hashcode values change (as long as the OneOf invariants remain the same). If false, hashcodes will be formatted as the application of a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode. One might wish to omit the exact values of the hashcodes because they are usually uninteresting; this is the same reason they print in the native Daikon format, for instance, as `var has only one value` rather than `var == 150924732`. The default value is ‘false’.

`daikon.inv.unary.sequence.OneOfSequence.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘3’.

`daikon.inv.unary.sequence.SingleSequence.SeqIndexDisableAll`

  Boolean. Set to true to disable all SeqIndex invariants (SeqIndexIntEqual, SeqIndexFloatLessThan, etc). This overrides the settings of the individual SeqIndex enable configuration options. To disable only some options, the options must be disabled individually. The default value is ‘false’.

`daikon.inv.unary.string.OneOfString.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘3’.

`daikon.inv.unary.stringsequence.EltOneOfString.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘3’.

`daikon.inv.unary.stringsequence.OneOfStringSequence.size`

  Positive integer. Specifies the maximum set size for this type of invariant (x is one of `size` items). The default value is ‘2’.

Next: Simplify interface configuration options, Previous: Other invariant configuration parameters, Up: List of configuration options [Contents][Index]

#### 6.1.1.4 Options to enable/disable derived variables

These options control whether Daikon looks for invariants involving certain forms of derived variables. Also see Variable names.

`daikon.derive.Derivation.disable_derived_variables`

  Boolean. If true, Daikon will not create any derived variables. Derived variables, which are combinations of variables that appeared in the program, like `array[index]` if `array` and `index` appeared, can increase the number of properties Daikon finds, especially over sequences. However, derived variables increase Daikon’s time and memory usage, sometimes dramatically. If false, individual kinds of derived variables can be enabled or disabled individually using configuration options under `daikon.derive`. The default value is ‘false’.

`daikon.derive.binary.SequenceFloatIntersection.enabled`

  Boolean. True iff SequenceFloatIntersection derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequenceFloatSubscript.enabled`

  Boolean. True iff SequenceFloatSubscript derived variables should be generated. The default value is ‘true’.

`daikon.derive.binary.SequenceFloatSubsequence.enabled`

  Boolean. True iff SequenceFloatSubsequence derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequenceFloatUnion.enabled`

  Boolean. True iff SequenceFloatUnion derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequenceScalarIntersection.enabled`

  Boolean. True iff SequenceScalarIntersection derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequenceScalarSubscript.enabled`

  Boolean. True iff SequenceScalarSubscript derived variables should be generated. The default value is ‘true’.

`daikon.derive.binary.SequenceScalarSubsequence.enabled`

  Boolean. True iff SequenceScalarSubsequence derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequenceScalarUnion.enabled`

  Boolean. True iff SequenceScalarUnion derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequenceStringIntersection.enabled`

  Boolean. True iff SequenceStringIntersection derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequenceStringSubscript.enabled`

  Boolean. True iff SequenceStringSubscript derived variables should be generated. The default value is ‘true’.

`daikon.derive.binary.SequenceStringSubsequence.enabled`

  Boolean. True iff SequenceStringSubsequence derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequenceStringUnion.enabled`

  Boolean. True iff SequenceStringUnion derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequencesConcat.enabled`

  Boolean. True iff SequencesConcat derived variables should be created. The default value is ‘false’.

`daikon.derive.binary.SequencesJoin.enabled`

  Boolean. True iff SequencesJoin derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequencesJoinFloat.enabled`

  Boolean. True iff SequencesJoin derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequencesPredicate.boolOnly`

  Boolean. True if Daikon should only generate derivations on boolean predicates. The default value is ‘true’.

`daikon.derive.binary.SequencesPredicate.enabled`

  Boolean. True iff SequencesPredicate derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequencesPredicate.fieldOnly`

  Boolean. True if Daikon should only generate derivations on fields of the same data structure. The default value is ‘true’.

`daikon.derive.binary.SequencesPredicateFloat.boolOnly`

  Boolean. True if Daikon should only generate derivations on boolean predicates. The default value is ‘true’.

`daikon.derive.binary.SequencesPredicateFloat.enabled`

  Boolean. True iff SequencesPredicate derived variables should be generated. The default value is ‘false’.

`daikon.derive.binary.SequencesPredicateFloat.fieldOnly`

  Boolean. True if Daikon should only generate derivations on fields of the same data structure. The default value is ‘true’.

`daikon.derive.ternary.SequenceFloatArbitrarySubsequence.enabled`

  Boolean. True iff SequenceFloatArbitrarySubsequence derived variables should be generated. The default value is ‘false’.

`daikon.derive.ternary.SequenceScalarArbitrarySubsequence.enabled`

  Boolean. True iff SequenceScalarArbitrarySubsequence derived variables should be generated. The default value is ‘false’.

`daikon.derive.ternary.SequenceStringArbitrarySubsequence.enabled`

  Boolean. True iff SequenceStringArbitrarySubsequence derived variables should be generated. The default value is ‘false’.

`daikon.derive.unary.SequenceInitial.enabled`

  Boolean. True iff SequenceInitial derived variables should be generated. The default value is ‘false’.

`daikon.derive.unary.SequenceInitialFloat.enabled`

  Boolean. True iff SequenceInitial derived variables should be generated. The default value is ‘false’.

`daikon.derive.unary.SequenceLength.enabled`

  Boolean. True iff SequenceLength derived variables should be generated. The default value is ‘true’.

`daikon.derive.unary.SequenceMax.enabled`

  Boolean. True iff SequencesMax derived variables should be generated. The default value is ‘false’.

`daikon.derive.unary.SequenceMin.enabled`

  Boolean. True iff SequenceMin derived variables should be generated. The default value is ‘false’.

`daikon.derive.unary.SequenceSum.enabled`

  Boolean. True iff SequenceSum derived variables should be generated. The default value is ‘false’.

`daikon.derive.unary.StringLength.enabled`

  Boolean. True iff StringLength derived variables should be generated. The default value is ‘false’.

Next: Splitter options, Previous: Options to enable/disable derived variables, Up: List of configuration options [Contents][Index]

#### 6.1.1.5 Simplify interface configuration options

The configuration options in this section are used to customize the interface to the Simplify theorem prover. See the description of the `--suppress_redundant` command-line option in Options to control invariant detection.

`daikon.simplify.LemmaStack.print_contradictions`

  Boolean. Controls Daikon’s response when inconsistent invariants are discovered while running Simplify. If true, Daikon will print an error message to the standard error stream listing the contradictory invariants. This is mainly intended for debugging Daikon itself, but can sometimes be helpful in tracing down other problems. For more information, see the section on troubleshooting contradictory invariants in the Daikon manual. The default value is ‘false’.

`daikon.simplify.LemmaStack.remove_contradictions`

  Boolean. Controls Daikon’s response when inconsistent invariants are discovered while running Simplify. If false, Daikon will give up on using Simplify for that program point. If true, Daikon will try to find a small subset of the invariants that cause the contradiction and avoid them, to allow processing to continue. For more information, see the section on troubleshooting contradictory invariants in the Daikon manual. The default value is ‘true’.

`daikon.simplify.LemmaStack.synchronous_errors`

  Boolean. If true, ask Simplify to check a simple proposition after each assumption is pushed, providing an opportunity to wait for output from Simplify and potentially receive error messages about the assumption. When false, long sequences of assumptions may be pushed in a row, so that by the time an error message arrives, it’s not clear which input caused the error. Of course, Daikon’s input to Simplify isn’t supposed to cause errors, so this option should only be needed for debugging. The default value is ‘false’.

`daikon.simplify.Session.simplify_max_iterations`

  A non-negative integer, representing the largest number of iterations for which Simplify should be allowed to run on any single conjecture before giving up. Larger values may cause Simplify to run longer, but will increase the number of invariants that can be recognized as redundant. The default value is small enough to keep Simplify from running for more than a few seconds on any one conjecture, allowing it to verify most simple facts without getting bogged down in long searches. A value of 0 means not to bound the number of iterations at all, though see also the `simplify_timeout` parameter..

`daikon.simplify.Session.simplify_timeout`

  A non-negative integer, representing the longest time period (in seconds) Simplify should be allowed to run on any single conjecture before giving up. Larger values may cause Simplify to run longer, but will increase the number of invariants that can be recognized as redundant. Roughly speaking, the time spent in Simplify will be bounded by this value, times the number of invariants generated, though it can be much less. A value of 0 means to not bound Simplify at all by time, though also see the option `simplify_max_iterations`. Beware that using this option might make Daikon’s output depend on the speed of the machine it’s run on. The default value is ‘0’.

`daikon.simplify.Session.trace_input`

  Boolean. If true, the input to the Simplify theorem prover will also be directed to a file named simplifyN.in (where N is a number starting from 0) in the current directory. Simplify’s operation can then be reproduced with a command like `Simplify -nosc <simplify0.in`. This is intended primarily for debugging when Simplify fails. The default value is ‘false’.

`daikon.simplify.Session.verbose_progress`

  Positive values mean to print extra indications as each candidate invariant is passed to Simplify during the `--suppress_redundant` check. If the value is 1 or higher, a hyphen will be printed when each invariant is passed to Simplify, and then replaced by a `T` if the invariant was redundant, `F` if it was not found to be, and `?` if Simplify gave up because of a time limit. If the value is 2 or higher, a `<` or `>` will also be printed for each invariant that is pushed onto or popped from from Simplify’s assumption stack. This option is mainly intended for debugging purposes, but can also provide something to watch when Simplify takes a long time. The default value is ‘0’.

Next: Debugging options, Previous: Simplify interface configuration options, Up: List of configuration options [Contents][Index]

#### 6.1.1.6 Splitter options

The configuration options in this section are used to customize the behavior of splitters, which yield conditional invariants and implications (see Conditional invariants).

`daikon.split.ContextSplitterFactory.granularity`

  Enumeration (integer). Specifies the granularity to use for callsite splitter processing. (That is, for creating invariants for a method that are dependent on where the method was called from.) 0 is line-level granularity; 1 is method-level granularity; 2 is class-level granularity. The default value is ‘1’.

`daikon.split.PptSplitter.disable_splitting`

  Boolean. If true, the built-in splitting rules are disabled. The built-in rules look for implications based on boolean return values and also when there are exactly two exit points from a method. The default value is ‘false’.

`daikon.split.PptSplitter.dummy_invariant_level`

  Integer. A value of zero indicates that DummyInvariant objects should not be created. A value of one indicates that dummy invariants should be created only when no suitable condition was found in the regular output. A value of two indicates that dummy invariants should be created for each splitting condition. The default value is ‘0’.

`daikon.split.PptSplitter.split_bi_implications`

  Split bi-implications ("`a <==> b`") into two separate implications ("`a ==> b`" and "`b ==> a`"). The default value is ‘false’.

`daikon.split.PptSplitter.suppressSplitterErrors`

  When true, compilation errors during splitter file generation will not be reported to the user. The default value is ‘true’.

`daikon.split.SplitterFactory.compile_timeout`

  Positive integer. Specifies the Splitter compilation timeout, in seconds, after which the compilation process is terminated and retried, on the assumption that it has hung. The default value is ‘20’.

`daikon.split.SplitterFactory.compiler`

  String. Specifies which Java compiler is used to compile Splitters. This can be the full path name or whatever is used on the command line. Uses the current classpath. The default value is ‘javac -nowarn -source 8 -target 8 -classpath /homes/gws/markro/jdk1.8.0_401/lib/tools.jar:/homes/gws/markro/jdk1.8.0_401/classes’.

`daikon.split.SplitterFactory.delete_splitters_on_exit`

  Boolean. If true, the temporary Splitter files are deleted on exit. Set it to "false" if you are debugging splitters. The default value is ‘true’.

`daikon.split.SplitterList.all_splitters`

  Boolean. Enables indiscriminate splitting (see Daikon manual, Indiscriminate splitting, for an explanation of this technique). The default value is ‘true’.

Next: Quantity of output, Previous: Splitter options, Up: List of configuration options [Contents][Index]

#### 6.1.1.7 Debugging options

The configuration options in this section are used to cause extra output that is useful for debugging. Also see section "Daikon debugging options" (see Daikon debugging options).

`daikon.Debug.internal_check`

  When true, perform detailed internal checking. These are essentially additional, possibly costly assert statements. The default value is ‘false’.

`daikon.Debug.logDetail`

  Returns true if detailed info (such as from `add_modified`) is printed. The default value is ‘false’.

`daikon.Debug.showTraceback`

  Returns true if traceback information is printed for each call to log. The default value is ‘false’.

`daikon.Debug.show_stack_trace`

  If true, show stack traces for errors such as file format errors. The default value is ‘false’.

Next: General configuration options, Previous: Debugging options, Up: List of configuration options [Contents][Index]

#### 6.1.1.8 Quantity of output

The configuration options in this section make Daikon print more or less output. They do not affect which invariants Daikon computes, only how it outputs them. Also see the following section.

`daikon.Daikon.guardNulls`

  If "always", then invariants are always guarded. If "never", then invariants are never guarded. If "missing", then invariants are guarded only for variables that were missing ("can be missing") in the dtrace (the observed executions). If "default", then use "missing" mode for Java output and "never" mode otherwise.

  Guarding means adding predicates that ensure that variables can be dereferenced. For instance, if `a` can be null — that is, if `a.b` can be nonsensical — then the guarded version of

      a.b == 5

  is

      (a != null) -> (a.b == 5)

  .

  (To do: Some configuration option (maybe this one) should add guards for other reasons that lead to nonsensical values (see Variable names).)
  The default value is ‘default’.

`daikon.Daikon.output_conditionals`

  Boolean. Controls whether conditional program points are displayed. The default value is ‘true’.

`daikon.Daikon.print_sample_totals`

  Boolean. Controls whether or not the total samples read and processed are printed at the end of processing. The default value is ‘false’.

`daikon.Daikon.progress_delay`

  The amount of time to wait between updates of the progress display, measured in milliseconds. A value of -1 means do not print the progress display at all. The default value is ‘1000’.

`daikon.Daikon.progress_display_width`

  The number of columns of progress information to display. In many Unix shells, this can be set to an appropriate value by `--config_option daikon.Daikon.progress_display_width=$COLUMNS`. The default value is ‘80’.

`daikon.Daikon.quiet`

  Boolean. Controls whether or not processing information is printed out. Setting this variable to true also automatically sets `progress_delay` to -1. The default value is ‘false’.

`daikon.FileIO.count_lines`

  Boolean. When false, don’t count the number of lines in the dtrace file before reading. This will disable the percentage progress printout. The default value is ‘true’.

`daikon.FileIO.dtrace_line_count`

  Long integer. If non-zero, this value will be used as the number of lines in (each) dtrace file input for the purposes of the progress display, and the counting of the lines in the file will be suppressed. The default value is ‘0’.

`daikon.FileIO.unmatched_procedure_entries_quiet`

  Boolean. When true, don’t print a warning about unmatched procedure entries, which are ignored by Daikon (unless the `--nohierarchy` command-line argument is provided). The default value is ‘false’.

`daikon.FileIO.verbose_unmatched_procedure_entries`

  Boolean. If true, prints the unmatched procedure entries verbosely. The default value is ‘false’.

`daikon.PrintInvariants.print_all`

  If true, print all invariants without any filtering. The default value is ‘false’.

`daikon.PrintInvariants.print_inv_class`

  Print invariant classname with invariants in output of `format()` method. Normally used only for debugging output rather than ordinary printing of invariants. This is especially useful when two different invariants have the same printed representation. The default value is ‘false’.

`daikon.PrintInvariants.true_inv_cnt`

  If true, print the total number of true invariants. This includes invariants that are redundant and would normally not be printed or even created due to optimizations. The default value is ‘false’.

Previous: Quantity of output, Up: List of configuration options [Contents][Index]

#### 6.1.1.9 General configuration options

This section lists miscellaneous configuration options for Daikon.

`daikon.Daikon.calc_possible_invs`

  Boolean. Just print the total number of possible invariants and exit. The default value is ‘false’.

`daikon.Daikon.ppt_perc`

  Integer. Percentage of program points to process. All program points are sorted by name, and all samples for the first `ppt_perc` program points are processed. A percentage of 100 matches all program points. The default value is ‘100’.

`daikon.Daikon.undo_opts`

  Boolean. Controls whether the Daikon optimizations (equality sets, suppressions) are undone at the end to create a more complete set of invariants. Output does not include conditional program points, implications, reflexive and partially reflexive invariants. The default value is ‘false’.

`daikon.DynamicConstants.OneOf_only`

  Boolean. Controls which invariants are created for variables that are constant for the entire run. If true, create only OneOf invariants. If false, create all possible invariants.

  Note that setting this to true only fails to create invariants between constants. Invariants between constants and non-constants are created regardless.

  A problem occurs with merging when this is turned on. If a var_info is constant at one child slice, but not constant at the other child slice, interesting invariants may not be merged because they won’t exist on the slice with the constant. This is thus currently defaulted to false. The default value is ‘false’.

`daikon.DynamicConstants.use_dynamic_constant_optimization`

  If true, use the dynamic constants optimization. This optimization doesn’t instantiate invariants over constant variables (i.e., those that have only seen one value). When the variable receives a second value, invariants are instantiated and are given the sample representing the previous constant value. The default value is ‘true’.

`daikon.FileIO.add_changed`

  Boolean. When false, set modbits to 1 iff the printed representation has changed. When true, set modbits to 1 if the printed representation has changed; leave other modbits as is. The default value is ‘true’.

`daikon.FileIO.continue_after_file_exception`

  Boolean. When true, suppress exceptions related to file reading. This permits Daikon to continue even if there is a malformed trace file. Use this with care: in general, it is better to fix the problem that caused a bad trace file, rather than to suppress the exception. The default value is ‘false’.

`daikon.FileIO.ignore_missing_enter`

  When true, just ignore exit ppts that don’t have a matching enter ppt rather than exiting with an error. Unmatched exits can occur if only a portion of a dtrace file is processed. The default value is ‘false’.

`daikon.FileIO.max_line_number`

  Integer. Maximum number of lines to read from the dtrace file. If 0, reads the entire file. The default value is ‘0’.

`daikon.FileIO.read_samples_only`

  Boolean. When true, only read the samples, but don’t process them. Used to gather timing information. The default value is ‘false’.

`daikon.FileIO.rm_stack_dups`

  If true, modified all ppt names to remove duplicate routine names within the ppt name. This is used when a stack trace (of active methods) is used as the ppt name. The routine names must be separated by vertical bars (|). The default value is ‘false’.

`daikon.PptRelation.enable_object_user`

  Boolean. Controls whether the object-user relation is created in the variable hierarchy. The default value is ‘false’.

`daikon.PptSliceEquality.set_per_var`

  If true, create one equality set for each variable. This has the effect of turning the equality optimization off, without actually removing the sets themselves (which are presumed to exist in many parts of the code). The default value is ‘false’.

`daikon.PptTopLevel.pairwise_implications`

  Boolean. If true, create implications for all pairwise combinations of conditions, and all pairwise combinations of exit points. If false, create implications for only the first two conditions, and create implications only if there are exactly two exit points. The default value is ‘false’.

`daikon.PptTopLevel.remove_merged_invs`

  Remove invariants at lower program points when a matching invariant is created at a higher program point. For experimental purposes only. The default value is ‘false’.

`daikon.PrintInvariants.old_array_names`

  In the new decl format, print array names as ’a[]’ as opposed to ’a[..]’ This creates names that are more compatible with the old output. This option has no effect in the old decl format. The default value is ‘true’.

`daikon.PrintInvariants.print_implementer_entry_ppts`

  If false, don’t print entry method program points for methods that override or implement another method (i.e., entry program points that have a parent that is a method). Microsoft Code Contracts does not allow contracts on such methods. The default value is ‘true’.

`daikon.PrintInvariants.remove_post_vars`

  If true, remove as many variables as possible that need to be indicated as ’post’. Post variables occur when the subscript for a derived variable with an orig sequence is not orig. For example: orig(a[post(i)]) An equivalent expression involving only orig variables is substituted for the post variable when one exists. The default value is ‘false’.

`daikon.PrintInvariants.replace_prestate`

  This option must be given with "–format Java" option.

  Instead of outputting prestate expressions as "\old(E)" within an invariant, output a variable name (e.g. ‘v1’). At the end of each program point, output the list of variable-to-expression mappings. For example: with this option set to false, a program point might print like this:

      foo.bar.Bar(int):::EXIT
      \old(capacity) == sizeof(this.theArray)

  With the option set to true, it would print like this:

      foo.bar.Bar(int):::EXIT
      v0 == sizeof(this.theArray)
      prestate assignment: v0=capacity

  The default value is ‘true’.

`daikon.PrintInvariants.static_const_infer`

  This enables a different way of treating static constant variables. They are not created into invariants into slices. Instead, they are examined during print time. If a unary invariant contains a value which matches the value of a static constant variable, the value will be replaced by the name of the variable, "if it makes sense". For example, if there is a static constant variable a = 1. And if there exists an invariant x <= 1, x <= a would be the result printed. The default value is ‘false’.

`daikon.ProglangType.convert_to_signed`

  If true, treat 32 bit values whose high bit is on, as a negative number (rather than as a 32 bit unsigned). The default value is ‘false’.

`daikon.VarInfo.constant_fields_simplify`

  If true, the treat static constants (such as MapQuick.GeoPoint.FACTOR) as fields within an object rather than as a single name. Not correct, but used to obtain compatibility with VarInfoName. The default value is ‘true’.

`daikon.VarInfo.declared_type_comparability`

  If true, then variables are only considered comparable if they are declared with the same type. For example, java.util.List is not comparable to java.util.ArrayList and float is not comparable to double. This may miss valid invariants, but significant time can be saved and many variables with different declared types are not comparable (e.g., java.util.Date and java.util.ArrayList). The default value is ‘true’.

`daikon.VarInfoName.direct_orig`

  When true, apply orig directly to variables, do not apply orig to derived variables. For example, create ’size(orig(a[]))’ rather than ’orig(size(a[]))’. The default value is ‘false’.

`daikon.chicory.DaikonVariableInfo.constant_infer`

  Enable experimental techniques on static constants. The default value is ‘false’.

`daikon.suppress.NIS.enabled`

  Boolean. If true, enable non-instantiating suppressions. The default value is ‘true’.

`daikon.suppress.NIS.hybrid_threshhold`

  Int. Less and equal to this number means use the falsified method in the hybrid method of processing falsified invariants, while greater than this number means use the antecedent method. Empirical data shows that number should not be more than 10000. The default value is ‘2500’.

`daikon.suppress.NIS.skip_hashcode_type`

  Boolean. If true, skip variables of file rep type `hashcode` when creating invariants over constants in the antecedent method. The default value is ‘true’.

`daikon.suppress.NIS.suppression_processor`

  Specifies the algorithm that NIS uses to process suppressions. Possible selections are ’HYBRID’, ’ANTECEDENT’, and ’FALSIFIED’. The default is the hybrid algorithm which uses the falsified algorithm when only a small number of suppressions need to be processed and the antecedent algorithm when a large number of suppressions are processed. The default value is ‘HYBRID’.

`daikon.suppress.NIS.suppressor_list`

  Boolean. If true, use the specific list of suppressor related invariant prototypes when creating constant invariants in the antecedent method. The default value is ‘true’.

Next: Enhancing conditional invariant detection, Previous: Configuration options, Up: Enhancing Daikon output [Contents][Index]

### 6.2 Conditional invariants (disjunctions) and implications

Conditional invariants are invariants that are true only part of the time. For instance, consider the absolute value procedure. Its postcondition is

    if arg < 0
      then return == -arg
      else return == arg

The invariant `return == -arg` is a conditional invariant because it depends on the predicate `arg < 0` being true. An implication is a compound invariant that includes both the predicate and the conditional invariant (also called the consequent); an example of an implication is `arg < 0 ==> return == -arg`.

Another type of implication is a context-sensitive invariant — a fact about method A that is true only when A is called by method B, but not true in general about A. You can use the configuration option `daikon.split.ContextSplitterFactory.granularity` to control creation of context-sensitive invariants. Alternately, you can use implications to construct context-sensitive invariants: set a variable that depends on the call site, then compute an implication whose predicate tests that variable. For an example, see the paper Selecting, refining, and evaluating predicates for program analysis (http://plse.cs.washington.edu/daikon/pubs/predicates-tr914-abstract.html).

Daikon must be supplied with the predicate for an implication. Daikon has certain built-in predicates that it uses for finding conditional invariants; examples are which return statement was executed in a procedure and whether a boolean procedure returns true or false. Additionally, Daikon can read predicates from a file called a splitter info (`.spinfo`) file and find implications based on those predicates. The splitter info file can be produced automatically, such as by static analysis of the program using the `CreateSpinfo` and `CreateSpinfoC` programs (see Static analysis for splitters) or by cluster analysis of the traced values in the data trace file. Details of these techniques and usage guides can be found in Enhancing conditional invariant detection. Users can also create splitter info files themselves or can augment automatically-created ones.

To detect conditional invariants and implications:

1. Create the splitter info file, either automatically or by hand.
2. Run Daikon with the `.spinfo` file as one of its arguments. (The order of arguments does not matter.) For example,

       java -cp ${DAIKONDIR}/daikon.jar daikon.Daikon Foo.decls Foo.spinfo Foo.dtrace

The term splitter comes from Daikon’s technique for detecting implications and conditional invariants. For each predicate, Daikon creates two conditional program points — one for program executions that satisfy the condition and one for those that don’t — and splits the data trace into two parts. Invariant detection is then performed on the conditional program points (that is, the parts of the data trace) separately and any invariants detected are reported as conditional invariants (as implications).

To be precise, we say that an invariant holds exclusively if it is discovered on one side of a split, and its negation is discovered on the opposite side. Daikon creates conditional invariants whose predicates are invariants that hold exclusively on one side of a split, and whose consequents are invariants that hold on that side of the split but not on the unsplit program point. If Daikon finds multiple exclusive conditions, it will create biconditional (“if and only if”) invariants between the equivalent conditions. Within the context of the program, each of the exclusive conditions is equivalent to the splitting condition. In particular, if both the splitting condition and its negation are within the grammar of invariants that Daikon detects, the splitting condition may appear as the predicate of the generated conditional invariants. On the other hand, if other equivalent conditions are found, or if the splitting condition is not expressible in Daikon’s grammar, it might not appear in the generated implications.

In some cases, the default policy of selecting predicates from Daikon’s output may be insufficient. For instance, Daikon might not detect any invariant equivalent to the splitting condition, if the splitting condition is sufficiently complex or application-specific. In such situations, Daikon can also use the splitting condition itself, as what is called a dummy invariant. To use dummy invariants, set the configuration option `daikon.split.PptSplitter.dummy_invariant_level` to a non-zero value (see List of configuration options).

Next: Indiscriminate splitting, Up: Conditional invariants [Contents][Index]

#### 6.2.1 Splitter info file format

A splitter info file contains the conditions that Daikon should use to create conditional invariants. Each section in the `.spinfo` file consists of a sequence of non-blank lines; sections are separated by blank lines. There are two types of sections: program point sections and replacement sections. See Example splitter info file, for an example splitter info file.

Next: Replacement sections, Up: Splitter info file format [Contents][Index]

#### 6.2.1.1 Program point sections

Program point sections have a line specifying a program point name followed by lines specifying the condition(s) associated with that program point, each condition on its own line. Additional information about a condition may be specified on indented lines. For example, a typical entry is

    PPT_NAME pptname
    condition1
    condition2
        DAIKON_FORMAT string
        ESC_FORMAT string
    condition3
    ...

pptname can be any string that matches a part of the desired program point name as printed in the `.decls` file. In finding matching program points, Daikon uses the first program point that matches pptname. Caution is necessary when dealing with method names that are prefixes of other method names. For instance, if the class `List` has methods `add` and `addAll`, specifying ‘`PPT_NAME List.add`’ might select either method, depending on which was encountered first. Instead writing ‘`PPT_NAME List.add(`’ will match only the `add` method.

Each condition is a Java expression of boolean type. All variables that appear in the condition must also appear in the declaration of the program point in the `.decls` file. (In other words, all the variables must be in scope at the program point(s) where the Splitter is intended to operate.) The automatically generated Splitter source code fails to compile (but Daikon proceeds without it) if a variable name in a condition is not found at the matching program point.

An indented lines beginning with ‘`DAIKON_FORMAT`’, ‘`JAVA_FORMAT`’, ‘`ESC_FORMAT`’, or ‘`SIMPLIFY_FORMAT`’ specifies how to print the condition. These are optional; for any Daikon output format that is omitted, the Java condition itself is used. The alternate printed representation is used when the splitting condition is used as a dummy invariant; see configuration option `daikon.split.PptSplitter.dummy_invariant_level`.

Previous: Program point sections, Up: Splitter info file format [Contents][Index]

#### 6.2.1.2 Replacement sections

Ordinarily, a splitting condition may not invoke user-defined methods, because when Daikon reads data trace files, it does not have access to the program source. A replace section of the splitter info file can specify the bodies of methods, permitting conditions to invoke those methods. The format is as follows:

    REPLACE
    procedure1
    replacement1
    procedure2
    replacement2
    ...

where replacementi is a Java expression for the body of procedurei. In each condition, Daikon replaces procedure calls by their replacements. A replace section may appear anywhere in the splitter info file.

Next: Example splitter info file, Previous: Splitter info file format, Up: Conditional invariants [Contents][Index]

#### 6.2.2 Indiscriminate splitting

Each condition in an `.spinfo` is associated with a program point. The condition can be used at only that program point by placing the following line in a file that is passed to Daikon via the `--config` flag (see Daikon configuration options):

    daikon.split.SplitterList.all_splitters = false

The default, called indiscriminate splitting, is to use every condition at every program point, regardless of where in the `.spinfo` file the condition appeared.

The advantage of indiscriminate splitting is that a condition that is useful at one program point may also be useful at another — if the same variables are in scope or other variables of the same name are in scope. The disadvantage of indiscriminate splitting is that it slows Daikon down.

Daikon uses a condition only where it can be used. For example, the condition `myArray.length == x` is applicable only at program points that have variables named `myArray` and `x`. To see warnings about places a splitting condition cannot be used (reported as failure to compile splitters at those locations), place the following line in a file that is passed to Daikon via the `--config` flag (see Daikon configuration options):

    daikon.split.SplitterList.all_splitters_errors = true

Previous: Indiscriminate splitting, Up: Conditional invariants [Contents][Index]

#### 6.2.3 Example splitter info file

Below is an implementation of a simple Queue for positive integers and a corresponding `.spinfo` file. The splitter info file is like the one that `CreateSpinfo` would create for that class, but also demonstrates some other features.

Next: Resulting .spinfo file, Up: Example splitter info file [Contents][Index]

#### 6.2.3.1 Example class

    class simpleStack {

      private int[] myArray;
      private int currentSize;

      public simpleStack(int capacity) {
        myArray = new int[capacity];
        currentSize = 0;
      }

      /** Adds an element to the back of the stack, if the stack is
        * not full.
        * Returns true if this succeeds, false otherwise.  */
      public String push(int x) {
        if ( !isFull() && x >= 0) {
          myArray[currentSize] = x;
          currentSize++;
          return true;
        } else {
          return false;
        }
      }

      /** Returns the most recently inserted stack element.
        * Returns -1 if the stack is empty. */
      public int pop() {
        if ( !isEmpty() ) {
          currentSize--;
          return myArray[currentSize];
        } else {
          return -1;
        }
      }

     /** Returns true if the stack is empty, false otherwise. */
      private boolean isEmpty() {
        return (currentSize == 0);
      }

      /** Returns true if the stack is full, false otherwise. */
      private boolean isFull() {
        return (currentSize == myArray.length);
      }
    }

Previous: Example class, Up: Example splitter info file [Contents][Index]

#### 6.2.3.2 Resulting .spinfo file

    REPLACE
    isFull()
    currentSize == myArray.length
    isEmpty()
    currentSize == 0

    PPT_NAME  simpleStack.push
    !isFull() && x >= 0
        DAIKON_FORMAT !isFull() and x >= 0
        SIMPLIFY_FORMAT (AND (NOT (isFull this)) (>= x 0))

    PPT_NAME  simpleStack.pop
    !isEmpty()

    PPT_NAME  simpleStack.isFull
    currentSize == myArray.length - 1

    PPT_NAME  simpleStack.isEmpty
    currentSize == 0

Next: Dynamic abstract type inference (DynComp), Previous: Conditional invariants, Up: Enhancing Daikon output [Contents][Index]

### 6.3 Enhancing conditional invariant detection

The built-in mechanisms (see Conditional invariants) have limitations in the invariants they can find. By supplying splitting conditions to Daikon via a splitter info file, the user can infer more conditional invariants. To ease this task, there are methods to automatically create splitter info files for use by Daikon.

Next: Cluster analysis for splitters, Up: Enhancing conditional invariant detection [Contents][Index]

#### 6.3.1 Static analysis for splitters

In static analysis, all boolean statements in the program source are extracted and used as splitting conditions. The assumption is that conditions that are explicitly tested in the program are likely to affect the program’s behavior and could lead to useful conditional invariants. The simple heuristic of using these conditional statements as predicates for conditional invariant detection is often quite effective.

Next: Static analysis of C for splitters, Up: Static analysis for splitters [Contents][Index]

#### 6.3.1.1 Static analysis of Java for splitters

The `CreateSpinfo` program takes Java source code as input and creates a splitter info file for each Java file; for instance,

    java -cp ${DAIKONDIR}/daikon.jar daikon.tools.jtb.CreateSpinfo Foo.java Bar.java

creates the splitter info files `Foo.spinfo` and `Bar.spinfo`. Given an `-o filename` argument, `CreateSpinfo` puts all the splitters in the specified file instead. The resulting splitter info file(s) contains each boolean expression that appears in the source code.

If you get an error such as

    jtb.ParseException: Encountered ";" at line 253, column 8.
    Was expecting one of: "abstract" ...

then you may have encountered a bug in the JTB library on which `CreateSpinfo` is built. It does not permit empty declarations in a class body. Remove the extra semicolon in your Java file (at the indicated position) and re-rerun `CreateSpinfo`.

Previous: Static analysis of Java for splitters, Up: Static analysis for splitters [Contents][Index]

#### 6.3.1.2 Static analysis of C for splitters

The `CreateSpinfoC` program performs the same function for C source code as `CreateSpinfoC` does for Java. `CreateSpinfoC` can only be run on postprocessed source files—that is, source files contain no `CPP` commands. `CPP` commands are lines starting with ‘`#`’, such as ‘`#include`’. To expand `CPP` commands into legal C, run either `cpp -P` or `gcc -P -E`. For instance, here is how you could use `CreateSpinfoC`:

    cpp -P foo.c foo.c-expanded
    cpp -P bar.c bar.c-expanded
    java -cp ${DAIKONDIR}/daikon.jar daikon.tools.jtb.CreateSpinfoC \
         foo.c-expanded bar.c-expanded

WARNING: The names produced by `CreateSpinfoC` sometimes differ from the names produced by Kvasir. For example, suppose you have a C file that contains a function ‘`foo`’. Then `CreateSpinfoC` may create a `.spinfo` file that mentions a program point named ‘`std.foo`’, whereas Kvasir creates a `.dtrace` file that mentions a program point named ‘`..foo`’. Such a mismatch will cause Daikon to produce no conditional invariants for the given program point. This is a bug that needs to be fixed! (Patches are welcome.) In the meanwhile, you can edit the generated `.spinfo` file to conform to the `.dtrace` file’s naming conventions.

If you get an error such as

    ... Lexical error at line 5, column 1.
    Encountered: "#" (35), after : ""

then you forgot to run `CPP` before running `CreateSpinfoC`.

If you get an error such as

    CreateSpinfoC encountered errors during parse.
    Encountered "__extension__ typedef struct {  ...

then your program uses non-standard C syntax. The ‘`__extension__`’ keyword is supported only by the `gcc` compiler, and isn’t handled by the `CreateSpinfoC` program. You could extend the `CreateSpinfoC` program to handle non-standard `gcc` extensions, or you could remove non-standard `gcc` extensions from your program. The extensions might also result from standard libraries rather than your own program — removing a directives such as ‘`#include <stdio.h>`’ when preprocessing may also resolve the problem.

Next: Random selection for splitters, Previous: Static analysis for splitters, Up: Enhancing conditional invariant detection [Contents][Index]

#### 6.3.2 Cluster analysis for splitters

Cluster analysis is a statistical method that finds groups or clusters in data. The clusters may indicate conditional properties in the program. The cluster analysis mechanism finds clusters in the data trace file, infers invariants over any clusters that it finds, and writes these invariants into a splitter info file. Then, you supply the splitter info file to Daikon in order to infer conditional invariants.

To find splitting conditions using cluster analysis, run the `runcluster.pl` program (found in the `${DAIKONDIR}/scripts` directory) in the following way:

    runcluster.pl [options] dtrace_file ... decls_files ...

The options are:

`-a ALG`
`--algorithm ALG`

  ALG specifies a clustering algorithm. Current options are ‘`km`’ (for kmeans), ‘`hierarchical`’, and ‘`xm`’ (for xmeans). The default is ‘`xm`’.

`-k`

  The number of clusters to use (for algorithms which require this input, which is everything except xmeans). The default is 4.

`--keep`

  Don’t delete the temporary files created by the clustering process. This is a debugging flag.

The `runcluster.pl` script currently supports three clustering programs. They are implementations of the kmeans algorithm, hierarchical clustering, and the xmeans algorithm (kmeans algorithm with efficient discovery of the number of clusters). The kmeans and hierarchical clustering tools are provided in the Daikon distribution. The xmeans code and executable are publicly available at http://www.cs.cmu.edu/~dpelleg/kmeans.html (fill in the license form and mail it in).

Previous: Cluster analysis for splitters, Up: Enhancing conditional invariant detection [Contents][Index]

#### 6.3.3 Random selection for splitters

Random selection can create representative samples of a data set with the added benefit of finding conditional properties and eliminating outliers. Given trace data, the `TraceSelect` tool creates several small subsets of the data by randomly selecting parts of the original trace file. Any invariant that is discovered in the smaller samples but not found over the entire data is a conditional invariant.

To find splitting conditions using random selection, run the `daikon.tools.TraceSelect` program in the following way:

    java -cp ${DAIKONDIR}/daikon.jar daikon.tools.TraceSelect \
        num_reps sample_size [options] \
        dtrace_file decls_files ... [daikon_options]

num_reps is the number of subsets to create, and sample_size is the number of invocations to collect for each method.

The daikon_options are the same options that can be provided to the `daikon.Daikon` program.

The options for `TraceSelect` are:

`-NOCLEAN`

  Don’t delete the temporary trace samples created by the random selection process. This can help for debugging or for using the tool solely to create trace samples instead of calculating invariants over the samples.

`-INCLUDE_UNRETURNED`

  Allows random selection to choose method invocations that entered the method successfully but did not exit normally; either from a thrown Exception or abnormal termination.

`-DO_DIFFS`

  Creates an `.spinfo` file for generating conditional invariants and implications by reporting the invariants that appear in at least one of the samples but not over the entire data set.

Next: Loop invariants, Previous: Enhancing conditional invariant detection, Up: Enhancing Daikon output [Contents][Index]

### 6.4 Dynamic abstract type inference (DynComp)

Abstract types group variables that are used for related purposes in a program. For example, suppose that some `int` variables in your program are array indices, and other `int` variables represent time. Even though these variables have the same type (`int`) in the programming language, they have different abstract types.

Abstract types can be provided as input to Daikon, so that it only infers invariants between values of the same abstract type. This has two benefits. First, it improves Daikon’s performance, often by over an order of magnitude, because it reduces the number of potential invariants that must be checked. Second, it reduces spurious output caused by invariants over unrelated variables. You are strongly recommended to supply abstract types when running Daikon; Daikon does not produce satisfactory output without abstract type information.

Abstract type inference is performed by the front-ends, before Daikon runs. The Daikon distribution includes three tools that infer abstract types (also called comparability types) from program executions.

- The Java DynComp tool produces a comparability file that must then be supplied to the Chicory Java front-end. For examples of using DynComp with Java programs, see Detecting invariants in Java programs. For full details about the DynComp tool for Java, see DynComp for Java.
- The Kvasir front-end for C/C++ binaries by default uses a DynComp mode in which it produces a separate `.decls` file containing comparability information, which must be supplied to Daikon along with the `.dtrace` file. For examples of using DynComp with C programs, see C examples. For full details about the DynComp tool for C/C++, see DynComp for C/C++.
- The Celeriac front-end for .NET programs can compute variable comparability. It does so statically by examining the program text, rather than dynamically by running the program as DynComp does. For full details about variable comparability in Celeriac, see https://github.com/codespecs/daikon-dot-net-front-end.

Previous: Dynamic abstract type inference (DynComp), Up: Enhancing Daikon output [Contents][Index]

### 6.5 Loop invariants

Daikon does not by default output loop invariants. Daikon can detect invariants at any location where it is provided with variable values, but currently Daikon’s front ends do not supply Daikon with variable values at loop heads.

You could extend a front end to output more variable values, or you could write a new front end.

Alternately, here is a way to use the current front ends to produce loop invariants. This workaround requires you to change your program, but it requires no change to Daikon or its front ends.

At the top of a loop (or at any other location in the program at which you would like to obtain invariants), insert a call to a dummy procedure that does no work but returns immediately. Pass, as arguments to the dummy procedure, all variables of interest (including local variables). Daikon will produce (identical) preconditions and postconditions for the dummy procedure; these are properties that held at the call site.

For instance, you might change the original code

      public void calculate(int x) {
        int tmp = 0;
        while (x > 0) {
          // you desire to compute an invariant here
          tmp=tmp+x;
          x=x-1;
        }
      }

into

      public void calculate(int x) {
        int tmp = 0;
        while (x > 0) {
          calculate_loophead(x, tmp);
          tmp=tmp+x;
          x=x-1;
        }
      }

      // dummy procedure
      public void calculate_loophead(int x, int tmp) {
      }

Previous: Dynamic abstract type inference (DynComp), Up: Enhancing Daikon output [Contents][Index]