Next: Enhancing Daikon output, Previous: Running Daikon, Up: Top [Contents][Index]

## 5 Daikon output

Daikon outputs the invariants that it discovers in textual form to your terminal. This chapter describes how to interpret those invariants — in other words, what do they mean?

Daikon also creates a `.inv` file that contains the invariants in serialized (binary) form. You can use the `.inv` file to print the invariants (see Printing invariants) in a variety of formats, to insert the invariants in your source code (see Annotate), to perform run-time checking of the invariants (see Runtime-check instrumenter, and InvariantChecker), and to do various other operations. See Tools, for descriptions of such tools.

If you wish to write your own tools for processing invariants, you have two general options. You can parse Daikon’s textual output, or you can write Java code that processes the `.inv` file. The `.inv` file is simply a serialized `PptMap` object. In addition to reading the Javadoc, you can examine how the other tools use this data structure.

Next: Program points, Up: Daikon output [Contents][Index]

### 5.1 Invariant syntax

Daikon can produce output in a variety of formats. Each of the format names can be specified as an argument to the `--format` argument of Daikon (see Options to control Daikon output), `PrintInvariants` (see Printing invariants), and Annotate (see Annotate). When passed on the command line, the format names are case-insensitive: `--format JML` and `--format jml` have the same effect.

You can enhance Daikon to produce output in other formats. See New formatting for invariants in Daikon Developer Manual.

Daikon format

  Daikon’s default format is a mix of Java, mathematical logic, and some additional extensions. It is intended to concisely convey meaning to programmers.

DBC format

  This format produces output in the design-by-contract (DBC) format expected by Parasoft’s `Jtest` tool (https://www.parasoft.com).

ESC/Java format
ESC format

  The Extended Static Checker for Java (`ESC/Java`) is a programming tool for finding errors in Java programs by checking annotations that are inserted in source code; for more details, see https://www.hpl.hp.com/downloads/crl/jtk/. Daikon’s `ESC/Java` format (which can also be specified as `ESC` format) is intended for use with the original `ESC/Java` tool. Use Daikon’s `JML` format for use with the ESC/Java2 tool.

Java format

  Write output as Java expressions. This means that each invariant is a valid Java expression, if inserted at the correct program point: right after method entry, for method entry invariants; right before method exit, for method exit invariants; or anywhere in the code, for object invariants.

  There are two exceptions. Method exit invariants that refer to ‘`pre-state`’, such as ‘`x == old(x) + 1`’, are output with the tag ‘`\old`’ surrounding the ‘`pre-state`’ expression (e.g. ‘`x == \old(x) + 1`’. Method exit invariants that refer to the return value of the method, such as ‘`return == x + y`’, are output with the tag ‘`\result`’ in place of the return value (e.g. ‘`\result == x + y`’). These expression are obviously not valid Java code.

JML format

  Produces output in JML (Java Modeling Language, https://www.cs.ucf.edu/~leavens/JML/); for details, see the JML Manual. `JML` format lets you use the various JVM tools on Daikon invariants, including run-time assertion checking and the ESC/Java2 tool.

Simplify format

  Produces output in the format expected by the Simplify automated theorem prover; for details, see the Simplify distribution.

CSharpContract format

  Produces C# output for use with Microsoft’s Code Contracts https://www.microsoft.com/en-us/research/project/code-contracts/. The format employs some extension/utility methods to improve contract readability; the library containing these methods can be found at https://github.com/twschiller/daikon-code-contract-extensions.

Next: Variable names, Previous: Invariant syntax, Up: Daikon output [Contents][Index]

### 5.2 Program points

A program point is a specific place in the source code, such as immediately before a particular line of code. Daikon’s output is organized by program points.

For example, `foo():::ENTER` is the point at the entry to procedure `foo()`; the invariants at that point are the preconditions for the `foo()` method, properties that are always true when the procedure is invoked.

Likewise, `foo():::EXIT` is the program point at the procedure exit, and invariants there are postconditions. When there are multiple exit points from a procedure (for instance, because of multiple `return` statements), the different exits are differentiated by suffixing them with their line numbers; for instance, `StackAr.top():::EXIT79`. The exit point lacking a line number (in this example, `StackAr.top():::EXIT`) collects the postconditions that are true at every numbered exit point. This is an example of a program point that represents a collection of locations in the program source rather than a single location. This concept is represented in Daikon by the dataflow hierarchy, see Dataflow hierarchy in Daikon Developer Manual.

The Java instrumenter Chicory selects names for program points that include an indication of the argument and return types for each method. These signatures are presented in `Class.getName` format: one character for each primitive type (‘`B`’ for byte, ‘`C`’ for character, ‘`Z`’ for boolean, etc.); ‘`Lclassname;`’ for object types; and a ‘`[`’ prefix for each level of array nesting.

Up: Program points [Contents][Index]

#### 5.2.1 OBJECT and CLASS program points

Two program point tags that have special meaning to Daikon’s hierarchy organization are `:::OBJECT` and `:::CLASS`. The `:::OBJECT` tag indicates object invariants (sometimes called representation invariants or class invariants) over all the instance (member) fields and static fields of the class. These properties always hold for any object of the given class, from the point of view of a client or user. These properties hold at entry to and exit from every public method of the class (except not the entry to constructors, when fields are not yet initialized).

The `:::CLASS` tag is just like `:::OBJECT`, but only for static variables, which have only one value for all objects. Static fields and instance fields are often used for different purposes. Daikon’s separation of the two types of fields permits programmers to see the properties over the static fields without knowing which are the static fields and pick them out of the `:::OBJECT` program point.

(By contrast, `ESC/Java` and `JML` make class invariants hold even at the entry and exit of private methods. Their designers believe that most private methods preserve the class invariant and are called only when the class invariant holds. `ESC/Java` and `JML` require an explicit helper annotation to indicate a private method for which the class invariant does not hold.)

A trace file does not contain samples for the `:::OBJECT` and `:::CLASS` program points. Variable values for these artificial program points are constructed from samples that do appear in a trace file. For example, an object invariant is a property that holds at entry to and exit from every public method of the class, so the `:::OBJECT` program point is constructed from samples at those points.

Next: Interpreting output, Previous: Program points, Up: Daikon output [Contents][Index]

### 5.3 Variable names

A front end produces a trace file that associates trace variable names with values. Trace variable names need not be exactly the same as the variables in the program. The trace may contain values that are not held in any program variables; in this case, the front end must make up a name to express that value (see below for examples).

Daikon ignores variable names when inferring invariants; it uses the names only when performing output. (Thus, the only practical restriction on trace names is that the `VarInfoName parse` method must be able to parse the name.)

By convention, trace variables are similar to program variables and field accesses. For example, `w` and `x.y.z` are legal trace variables. (So are ‘`a[i]`’, and ‘`a[0].next`’, but these are usually handled as derived variables instead; see below.) As in languages such as Java and C, a period character represents field access and square brackets represent selecting an element of a sequence.

In addition to variables that appear in the trace file, Daikon creates additional variables, called derived variables, by combining trace variables. For example, for any array `a` and integer `i`, Daikon creates a derived variable `a[i]`. This is not a variable in the program (and this expression might not even appear in the source code), but it may still be useful to compute invariants over this expression. For a list of derived variables and how to control Daikon’s use of them, see Options to enable/disable derived variables.

Some trace variables and derived variables may represent meaningless expressions; in such a circumstance, the value is said to be nonsensical (see Nonsensical values in Daikon Developer Manual).

The remainder of this section describes conventions for naming expressions. Those that cannot be named by simple C/Java expressions are primarily related to arrays and sequences. (In part, these special expressions are necessary because Daikon can only handle variables of scalar (integer, floating-point, boolean, String) and array-of-scalar types. Daikon cannot handle structs, classes, or multidimensional arrays or structures, but such data structures can be represented as scalars and arrays by choosing variable names that indicate their relationship.)

- `a[i]` array access. `a` and `i` are themselves arbitrary variable names, of array and integral type, respectively.
- `a[-1]` from-end array access. `a[-1]` denotes the last element of array `a`; it is syntactic sugar for `a[a.length-1]`.
- `a[]` array contents. For array-valued expression `a`, all of its elements, as a sequence. Simply using the expression `a` means the identity (address or hashcode) of the array, not a list of its elements. For two arrays `a` and `b`, ‘`a=b`’ implies ‘`a[]=b[]`’, but ‘`a[]=b[]`’ does not imply ‘`a=b`’.
- `x.y`, `x->y` field access. When field access is applied to a structure/class, it has the usual meaning of selecting one field from the structure/class.

  When field access is applied to an array, it means to map the field access across the elements of the array. For example, if `a` is an array, then `a[].foo` is the sequence consisting of the `foo` fields of each of the elements of `a`. Likewise, `a[].foo.bar` contains the `bar` fields of `a[].foo`. By contrast, `a.foo` does not make sense, because one cannot ask for the `foo` field of an address, and `a[].foo[]` would be a two-dimensional array.

- As in Java, `x.getClass()` is the run-time type of `x`, which may differ from its declared type.
- `a.length` is the length (number of elements) of array `a`; this is not necessarily the number of initialized or used elements.
- `s.toString` is the string value of String `s`, namely a sequence of characters.
- `Classname.varname` static class variable. Static variables of a class have names of the form ‘`classname.varname`’
- `orig(x)` refers to the value of variable `x` upon entry to a procedure (because the procedure body might modify the value of `x`). These variables appear only at `:::EXIT` program points. Typically, `orig()` variables do not appear in the trace, but are automatically created by Daikon when it matches up `:::ENTER` and `:::EXITnn` program points. See orig variable example.

  This variable prints as `orig` when using Daikon output format (see Invariant syntax), but may print differently in other formats (such as `\old`).

- `post(x)` refers to the value of variable `x` upon exit from a procedure. Such a value is usually written simply `x`; the `post` prefix is needed only within an `orig` expression, when the post-state value needs to be referenced. Just as `orig` may be used only in a post-state context and specifies an expression to be evaluated in the ‘`pre-state`’, `post` may be used only in a ‘`pre-state`’ context and specifies an expression to be evaluated in the post-state. See orig variable example.
- `/globalVar` C global variable. In C output, global variables with external linkage are prefixed with a slash. For instance, global `/x` is distinct from procedure parameter `/x`. (In Java programs, variables can be distinguished by prefixing them with `this.` or, for class-static variables, a class name.)
- `myfile_c/staticVar` C static variable. In C output, file-static variables have names of the form ‘`filename/varname`’, where periods (‘`.`’) in the filename are converted into underscores (‘`_`’). For example, ‘`Global_c/x`’ is the name for a file-static variable `x` declared in the file `Global.c`).
- `myfile_c@funcname/funcStaticVar` C function-scoped static variable. In C output, for static variables which are declared within functions, an at-sign ‘`@`’ separates the filename and the function name and then a slash separates the function name and variable name (e.g., ‘`Global_c@main/funcStaticVar`’ for a static variable `funcStaticVar` declared within the function `main` in the file `Global.c`).

Daikon’s current front ends do not produce output for local variables, only for variables visible from outside a procedure. (Also see the `--std-visibility` option to Chicory, Chicory options.) More generally, Daikon’s front ends produce output at procedure exit and entry, not within the procedure. Thus, Daikon’s output forms a specification from the view of a client of a procedure. If you wish to compute invariants over local variables, you can extend one of Daikon’s front ends (or request us to do so). An alternative that permits computing invariants at arbitrary locations is to call a dummy procedure, passing all the variables of interest. The dummy procedure’s pre and postconditions will be identical and will represent the invariants at the point of call.

The array introduction operator `[]` can made Daikon variables look slightly odd, but it is intended to assist in interpreting the variables and to provide an indication that the variable name cannot be substituted directly in a program as an expression.

Each array introduction operator `[]` increases the dimensionality of the variable, and each array indexing operation `[i]` decreases it. Since all Daikon variables are scalars or one-dimensional arrays, these operators must be matched up, or have at most one more `[]` than `[i]`. (There is one exception: according to a strict interpretation of the rules, the C/Java expression `a[i]` would turn into the Daikon variable `a[][i]`, since it does not change the dimensionality of any expression it appears in. However, that would be even more confusing, and the point is to avoid confusion, so by convention Daikon front ends use just `a[i]`, not `a[][i]`. Strictly speaking, none of the `[]` operators is necessary, since a user with a perfect knowledge of the type of each program variable and field could use that to infer the type of any Daikon expression.)

Up: Variable names [Contents][Index]

#### 5.3.1 orig() variable example

This section gives an example of use of `orig()` and `post()` variables and arrays.

Suppose you have initially that (in Java syntax)

    int i = 0;
    int[] a = new int[] { 22, 23 };
    int[] b = new int[] { 46, 47 };

and then you run the following:

    // pre-state values at this point
    a[0] = 24;
    a[1] = 25
    a = b;
    a[0] = 48;
    a[1] = 49;
    i = 1;
    // post-state values at this point

The values of various variables are as follows:

`orig(a[i]) = 22`

  The value of `a[i]` in the ‘`pre-state`’: {22, 23}[0]

`orig(a[])[orig(i)] = 22`

  This is the same as orig(a[i]): {22, 23}[0].

`orig(a[])[i] = 23`

  The value of `a[]` in the ‘`pre-state`’ (which is an array object, not a reference), indexed by the post-state value of i: {22, 23}[1]

`orig(a)[orig(i)] = 24`

  `orig(a)` is the original value of the reference `a`, not `a``'s` original elements: {24, 25}[0]

`orig(a)[i] = 25`

  The original pointer value of a, indexed by the post-state value of i: {24, 25}[1]

`a[orig(i)] = 48`

  In the post-state, `a` indexed by the original value of `i`: {48, 49}[0]

`a[i] = 49`

  The value of `a[i]` in the post-state.

`b = orig(b) = some hashcode`

  The identity of the array `b` has not changed.

`b[] = [48, 49]`
`orig(b[]) = [46, 47]`

  For an array `b`, ‘`b=orig(b)`’ does not imply ‘`b[]=orig(b[])`’.

`orig(a[post(i)]) = 23`

  The ‘`pre-state`’ value of `a[1]` (because the post-state value of `i` is 1): {22, 23}[1]

Next: Invariant list, Previous: Variable names, Up: Daikon output [Contents][Index]

### 5.4 Interpreting Daikon output

If nothing gets printed before the ‘`Exiting`’ line, then Daikon found no invariants. You can get a little bit more information by using the `--output_num_samples` flag to Daikon (see Options to control Daikon output).

Daikon’s output is predicated on the assumption that all expressions that get evaluated are sensible. For instance, if Daikon prints ‘`a.b == 0`’, then that means that if ‘`a.b`’ is sensible (that is, ‘`a`’ is non-null), then its value is zero. When ‘`a`’ is ‘`null`’, then ‘`a.b`’ is called nonsensical. Daikon’s output ignores all nonsensical values. If you would like the assumptions to be printed explicitly, then set the `daikon.Daikon.guardNulls` configuration option (see General configuration options).

Next: Equal variables, Up: Interpreting output [Contents][Index]

#### 5.4.1 Redundant invariants

By default, Daikon does not display redundant invariants — those that are implied by other invariants in the output — because such results would merely clutter the output without adding any valuable information. For instance, if Daikon reports ‘`x==y`’, then it never also reports ‘`x-1==y-1`’. You can control this behavior to some extent by disabling invariant filters; see Invariant filters. (You can also print all invariants, even redundant ones, by saving the invariants to a `.inv` file and then using the `PrintInvariants` (see Printing invariants) or Diff (see Invariant Diff) programs to print the results.)

Next: Has only one value variables, Previous: Redundant invariants, Up: Interpreting output [Contents][Index]

#### 5.4.2 Equal variables

If two variables `x` and `y` are equal, then any invariant about `x` is also true about `y`. Daikon chooses one variable (the leader) from the set of equal variables, and only prints invariants over the leader.

Suppose that `a = b = c`. Then Daikon will print `a = b` and `a = c`, but not `b = c`. Furthermore, Daikon might print `a > d`, but would not print `b > d` or `c > d`.

You can control which variables are in an equality set; see Variable comparability in Daikon Developer Manual.

Next: Object inequality, Previous: Equal variables, Up: Interpreting output [Contents][Index]

#### 5.4.3 Has only one value variables

The output ‘`var has only one value`’ in Daikon’s output means that every time that variable var was encountered, it had the same value. Daikon ordinarily reports the actual value, as in ‘`var == 22`’. Typically, the “has only one value” output means that the variable is a hashcode or address — that is, its declared type is ‘`hashcode`’ (see Variable declarations in Daikon Developer Manual). For example, ‘`var == 0x38E8A`’ is not very illuminating, but it is still interesting that var was never rebound to a different object.

Note that ‘`var has only one value`’ is different from saying that var is unmodified.

A variable might have only one value but not be reported as unmodified because the variable is not a parameter to a procedure — for instance, if a routine always returns the same object, or in a class invariant. A variable can be reported as unmodified but not have only one value because the variable is never modified during any execution of the procedure, but has different values on different invocations of the procedure.

Previous: Has only one value variables, Up: Interpreting output [Contents][Index]

#### 5.4.4 Object inequality

Daikon may report ‘`x < y`’ where the operator ‘`<`’ is not applicable to the type of ‘`x`’ and ‘`y`’, as in ‘`myString < otherString`’.

In this case, the invariant means that the first expression is always less than the second, according to the ‘`Comparable.compareTo`’ method.

Next: Invariant filters, Previous: Interpreting output, Up: Daikon output [Contents][Index]

### 5.5 Invariant list

The following is a list of all of the invariants that Daikon detects. Each invariant has a configuration enable switch. By default most invariants are enabled. Any that are not enabled by default are indicated below. Some invariants also have additional configuration switches that control their behavior. These are indicated below as well. See Options to enable/disable specific invariants.

AndJoiner

  This is a special invariant used internally by Daikon to represent an antecedent invariant in an implication where that antecedent consists of two invariants anded together.

CommonFloatSequence

  Represents sequences of double values that contain a common subset. Prints as `{e1, e2, e3, ...} subset of x[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.CommonFloatSequence.enabled`’.

  See also the following configuration option:

  - ‘`daikon.inv.unary.sequence.CommonFloatSequence.hashcode_seqs`’
CommonSequence

  Represents sequences of long values that contain a common subset. Prints as `{e1, e2, e3, ...} subset of x[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.CommonSequence.enabled`’.

  See also the following configuration option:

  - ‘`daikon.inv.unary.sequence.CommonSequence.hashcode_seqs`’
CommonStringSequence

  Represents string sequences that contain a common subset. Prints as `{s1, s2, s3, ...} subset of x[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.stringsequence.CommonStringSequence.enabled`’.

CompleteOneOfScalar

  Tracks every unique value and how many times it occurs. Prints as either `x has no values` or as `x has values: v1 v2 v3 ...`. The set has no maximum size; it may be arbitrarily large.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.scalar.CompleteOneOfScalar.enabled`’.

CompleteOneOfString

  Tracks every unique value and how many times it occurs. Prints as either `x has no values` or as `x has values: "v1" "v2" "v3" ...`. The set has no maximum size; it may be arbitrarily large.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.string.CompleteOneOfString.enabled`’.

DummyInvariant

  This is a special invariant used internally by Daikon to represent invariants whose meaning Daikon doesn’t understand. The only operation that can be performed on a DummyInvariant is to print it. In particular, the invariant cannot be tested against a sample: the invariant is always assumed to hold and is always considered to be statistically justified.

  The main use for a dummy invariant is to represent a splitting condition that appears in a `.spinfo` file. The `.spinfo` file can indicate an arbitrary Java expression, which might not be equivalent to any invariant in Daikon’s grammar.

  Ordinarily, Daikon uses splitting conditions to split data, then seeks to use that split data to form conditional invariants out of its standard built-in invariants. If you wish the expression in the .spinfo file to be printed as an invariant, whether or not it is itself discovered by Daikon during invariant detection, then the configuration option `daikon.split.PptSplitter.dummy_invariant_level` must be set, and formatting information must be supplied in the splitter info file.

EltLowerBound

  Represents the invariant that each element of a sequence of long values is greater than or equal to a constant. Prints as `x[] elements >= c`.

  See also the following configuration options:

  - ‘`daikon.inv.unary.sequence.EltLowerBound.minimal_interesting`’
  - ‘`daikon.inv.unary.sequence.EltLowerBound.maximal_interesting`’
EltLowerBoundFloat

  Represents the invariant that each element of a sequence of double values is greater than or equal to a constant. Prints as `x[] elements >= c`.

  See also the following configuration options:

  - ‘`daikon.inv.unary.sequence.EltLowerBoundFloat.minimal_interesting`’
  - ‘`daikon.inv.unary.sequence.EltLowerBoundFloat.maximal_interesting`’
EltNonZero

  Represents the invariant "x != 0" where x represents all of the elements of a sequence of long. Prints as `x[] elements != 0`.

EltNonZeroFloat

  Represents the invariant "x != 0" where x represents all of the elements of a sequence of double. Prints as `x[] elements != 0`.

EltOneOf

  Represents sequences of long values where the elements of the sequence take on only a few distinct values. Prints as either `x[] elements == c` (when there is only one value), or as `x[] elements one of {c1, c2, c3}` (when there are multiple values).

  May print as `x[] elements has only one value` when `x` is an array of hashcodes (pointers) – this is because the numerical value of the hashcode (pointer) is uninteresting.

  See also the following configuration options:

  - ‘`daikon.inv.unary.sequence.EltOneOf.size`’
  - ‘`daikon.inv.unary.sequence.EltOneOf.omit_hashcode_values_Simplify`’
EltOneOfFloat

  Represents sequences of double values where the elements of the sequence take on only a few distinct values. Prints as either `x[] elements == c` (when there is only one value), or as `x[] elements one of {c1, c2, c3}` (when there are multiple values).

  See also the following configuration option:

  - ‘`daikon.inv.unary.sequence.EltOneOfFloat.size`’
EltOneOfString

  Represents sequences of String values where the elements of the sequence take on only a few distinct values. Prints as either `x[] elements == c` (when there is only one value), or as `x[] elements one of {c1, c2, c3}` (when there are multiple values).

  See also the following configuration option:

  - ‘`daikon.inv.unary.stringsequence.EltOneOfString.size`’
EltRangeFloat.EqualMinusOne

  Internal invariant representing double scalars that are equal to minus one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeFloat.EqualOne

  Internal invariant representing double scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeFloat.EqualZero

  Internal invariant representing double scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeFloat.GreaterEqual64

  Internal invariant representing double scalars that are greater than or equal to 64. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

EltRangeFloat.GreaterEqualZero

  Internal invariant representing double scalars that are greater than or equal to 0. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

EltRangeInt.BooleanVal

  Internal invariant representing longs whose values are always 0 or 1. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeInt.Bound0_63

  Internal invariant representing longs whose values are between 0 and 63. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

EltRangeInt.EqualMinusOne

  Internal invariant representing long scalars that are equal to minus one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeInt.EqualOne

  Internal invariant representing long scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeInt.EqualZero

  Internal invariant representing long scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeInt.Even

  Invariant representing longs whose values are always even. Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf invariants it is printed. Prints as `x is even`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.EltRangeInt.Even.enabled`’.

EltRangeInt.GreaterEqual64

  Internal invariant representing long scalars that are greater than or equal to 64. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

EltRangeInt.GreaterEqualZero

  Internal invariant representing long scalars that are greater than or equal to 0. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

EltRangeInt.PowerOfTwo

  Invariant representing longs whose values are always a power of 2 (exactly one bit is set). Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf invariants it is printed. Prints as `x is a power of 2`.

EltUpperBound

  Represents the invariant that each element of a sequence of long values is less than or equal to a constant. Prints as `x[] elements <= c`.

  See also the following configuration options:

  - ‘`daikon.inv.unary.sequence.EltUpperBound.minimal_interesting`’
  - ‘`daikon.inv.unary.sequence.EltUpperBound.maximal_interesting`’
EltUpperBoundFloat

  Represents the invariant that each element of a sequence of double values is less than or equal to a constant. Prints as `x[] elements <= c`.

  See also the following configuration options:

  - ‘`daikon.inv.unary.sequence.EltUpperBoundFloat.minimal_interesting`’
  - ‘`daikon.inv.unary.sequence.EltUpperBoundFloat.maximal_interesting`’
EltwiseFloatEqual

  Represents equality between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as `x[] elements are equal`.

EltwiseFloatGreaterEqual

  Represents the invariant >= between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as `x[] sorted by >=`.

EltwiseFloatGreaterThan

  Represents the invariant > between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as `x[] sorted by >`.

EltwiseFloatLessEqual

  Represents the invariant <= between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as `x[] sorted by <=`.

EltwiseFloatLessThan

  Represents the invariant < between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as `x[] sorted by <`.

EltwiseIntEqual

  Represents equality between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as `x[] elements are equal`.

EltwiseIntGreaterEqual

  Represents the invariant >= between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as `x[] sorted by >=`.

EltwiseIntGreaterThan

  Represents the invariant > between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as `x[] sorted by >`.

EltwiseIntLessEqual

  Represents the invariant <= between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as `x[] sorted by <=`.

EltwiseIntLessThan

  Represents the invariant < between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as `x[] sorted by <`.

Equality

  Keeps track of sets of variables that are equal. Other invariants are instantiated for only one member of the Equality set, the leader. If variables `x`, `y`, and `z` are members of the Equality set and `x` is chosen as the leader, then the Equality will internally convert into binary comparison invariants that print as `x == y` and `x == z`.

FloatEqual

  Represents an invariant of == between two double scalars. Prints as `x == y`.

FloatGreaterEqual

  Represents an invariant of >= between two double scalars. Prints as `x >= y`.

FloatGreaterThan

  Represents an invariant of > between two double scalars. Prints as `x > y`.

FloatLessEqual

  Represents an invariant of <= between two double scalars. Prints as `x <= y`.

FloatLessThan

  Represents an invariant of < between two double scalars. Prints as `x < y`.

FloatNonEqual

  Represents an invariant of != between two double scalars. Prints as `x != y`.

FunctionBinary.BitwiseAndLong_{xyz, yxz, zxy}

  Represents the invariant `x = BitwiseAnd(y, z)` over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.BitwiseOrLong_{xyz, yxz, zxy}

  Represents the invariant `x = BitwiseOr(y, z)` over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.BitwiseXorLong_{xyz, yxz, zxy}

  Represents the invariant `x = BitwiseXor(y, z)` over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.DivisionLong_{xyz, xzy, yxz, yzx, zxy, zyx}

  Represents the invariant `x = Division(y, z)` over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.GcdLong_{xyz, yxz, zxy}

  Represents the invariant `x = Gcd(y, z)` over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.LogicalAndLong_{xyz, yxz, zxy}

  Represents the invariant `x = LogicalAnd(y, z)` over three long scalars. For logical operations, Daikon treats 0 as false and all other values as true. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.LogicalOrLong_{xyz, yxz, zxy}

  Represents the invariant `x = LogicalOr(y, z)` over three long scalars. For logical operations, Daikon treats 0 as false and all other values as true. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.LogicalXorLong_{xyz, yxz, zxy}

  Represents the invariant `x = LogicalXor(y, z)` over three long scalars. For logical operations, Daikon treats 0 as false and all other values as true. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.LshiftLong_{xyz, xzy, yxz, yzx, zxy, zyx}

  Represents the invariant `x = Lshift(y, z)` over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.MaximumLong_{xyz, yxz, zxy}

  Represents the invariant `x = Maximum(y, z)` over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.MinimumLong_{xyz, yxz, zxy}

  Represents the invariant `x = Minimum(y, z)` over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.ModLong_{xyz, xzy, yxz, yzx, zxy, zyx}

  Represents the invariant `x = Mod(y, z)` over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.MultiplyLong_{xyz, yxz, zxy}

  Represents the invariant `x = Multiply(y, z)` over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.PowerLong_{xyz, xzy, yxz, yzx, zxy, zyx}

  Represents the invariant `x = Power(y, z)` over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.RshiftSignedLong_{xyz, xzy, yxz, yzx, zxy, zyx}

  Represents the invariant `x = RshiftSigned(y, z)` over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.RshiftUnsignedLong_{xyz, xzy, yxz, yzx, zxy, zyx}

  Represents the invariant `x = RshiftUnsigned(y, z)` over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinaryFloat.DivisionDouble_{xyz, xzy, yxz, yzx, zxy, zyx}

  Represents the invariant `x = Division(y, z)` over three double scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinaryFloat.MaximumDouble_{xyz, yxz, zxy}

  Represents the invariant `x = Maximum(y, z)` over three double scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinaryFloat.MinimumDouble_{xyz, yxz, zxy}

  Represents the invariant `x = Minimum(y, z)` over three double scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinaryFloat.MultiplyDouble_{xyz, yxz, zxy}

  Represents the invariant `x = Multiply(y, z)` over three double scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

GuardingImplication

  This is a special implication invariant that guards any invariants that are over variables that are sometimes missing. For example, if the invariant `a.x = 0` is true, the guarded implication is `a != null => a.x = 0`.

Implication

  The Implication invariant class is used internally within Daikon to handle invariants that are only true when certain other conditions are also true (splitting).

IntEqual

  Represents an invariant of == between two long scalars. Prints as `x == y`.

IntGreaterEqual

  Represents an invariant of >= between two long scalars. Prints as `x >= y`.

IntGreaterThan

  Represents an invariant of > between two long scalars. Prints as `x > y`.

IntLessEqual

  Represents an invariant of <= between two long scalars. Prints as `x <= y`.

IntLessThan

  Represents an invariant of < between two long scalars. Prints as `x < y`.

IntNonEqual

  Represents an invariant of != between two long scalars. Prints as `x != y`.

  See also the following configuration option:

  - ‘`daikon.inv.binary.twoScalar.IntNonEqual.integral_only`’
IsPointer

  IsPointer is an invariant that heuristically determines whether an integer represents a pointer (a 32-bit memory address). Since both a 32-bit integer and an address have the same representation, sometimes a a pointer can be mistaken for an integer. When this happens, several scalar invariants are computed for integer variables. Most of them would not make any sense for pointers. Determining whether a 32-bit variable is a pointer can thus spare the computation of many irrelevant invariants.

  The basic approach is to discard the invariant if any values that are not valid pointers are encountered. By default values between -100,000 and 100,000 (except 0) are considered to be invalid pointers. This approach has been experimentally confirmed on Windows x86 executables.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.scalar.IsPointer.enabled`’.

LinearBinary

  Represents a Linear invariant between two long scalars `x` and `y`, of the form `ax + by + c = 0`. The constants `a`, `b` and `c` are mutually relatively prime, and the constant `a` is always positive.

LinearBinaryFloat

  Represents a Linear invariant between two double scalars `x` and `y`, of the form `ax + by + c = 0`. The constants `a`, `b` and `c` are mutually relatively prime, and the constant `a` is always positive.

LinearTernary

  Represents a Linear invariant over three long scalars `x`, `y`, and `z`, of the form `ax + by + cz + d = 0`. The constants `a`, `b`, `c`, and `d` are mutually relatively prime, and the constant `a` is always positive.

LinearTernaryFloat

  Represents a Linear invariant over three double scalars `x`, `y`, and `z`, of the form `ax + by + cz + d = 0`. The constants `a`, `b`, `c`, and `d` are mutually relatively prime, and the constant `a` is always positive.

LowerBound

  Represents the invariant `x >= c`, where `c` is a constant and `x` is a long scalar.

  See also the following configuration options:

  - ‘`daikon.inv.unary.scalar.LowerBound.minimal_interesting`’
  - ‘`daikon.inv.unary.scalar.LowerBound.maximal_interesting`’
LowerBoundFloat

  Represents the invariant `x >= c`, where `c` is a constant and `x` is a double scalar.

  See also the following configuration options:

  - ‘`daikon.inv.unary.scalar.LowerBoundFloat.minimal_interesting`’
  - ‘`daikon.inv.unary.scalar.LowerBoundFloat.maximal_interesting`’
Member

  Represents long scalars that are always members of a sequence of long values. Prints as `x in y[]` where `x` is a long scalar and `y[]` is a sequence of long.

MemberFloat

  Represents double scalars that are always members of a sequence of double values. Prints as `x in y[]` where `x` is a double scalar and `y[]` is a sequence of double.

MemberString

  Represents String scalars that are always members of a sequence of String values. Prints as `x in y[]` where `x` is a String scalar and `y[]` is a sequence of String.

Modulus

  Represents the invariant `x == r (mod m)` where `x` is a long scalar variable, `r` is the (constant) remainder, and `m` is the (constant) modulus.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.scalar.Modulus.enabled`’.

NoDuplicates

  Represents sequences of long that contain no duplicate elements. Prints as `x[] contains no duplicates`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.NoDuplicates.enabled`’.

NoDuplicatesFloat

  Represents sequences of double that contain no duplicate elements. Prints as `x[] contains no duplicates`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.NoDuplicatesFloat.enabled`’.

NonModulus

  Represents long scalars that are never equal to `r (mod m)` where all other numbers in the same range (i.e., all the values that `x` doesn’t take from `min(x)` to `max(x)`) are equal to `r (mod m)`. Prints as `x != r (mod m)`, where `r` is the remainder and `m` is the modulus.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.scalar.NonModulus.enabled`’.

NonZero

  Represents long scalars that are non-zero. Prints as `x != 0`, or as `x != null` for pointer types.

NonZeroFloat

  Represents double scalars that are non-zero. Prints as `x != 0`.

NumericFloat.Divides

  Represents the divides without remainder invariant between two double scalars. Prints as `x % y == 0`.

NumericFloat.Square

  Represents the square invariant between two double scalars. Prints as `x = y**2`.

NumericFloat.ZeroTrack

  Represents the zero tracks invariant between two double scalars; that is, when `x` is zero, `y` is also zero. Prints as `x = 0 => y = 0`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoScalar.NumericFloat.ZeroTrack.enabled`’.

NumericInt.BitwiseAndZero

  Represents the BitwiseAnd == 0 invariant between two long scalars; that is, `x` and `y` have no bits in common. Prints as `x & y == 0`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoScalar.NumericInt.BitwiseAndZero.enabled`’.

NumericInt.BitwiseComplement

  Represents the bitwise complement invariant between two long scalars. Prints as `x = ~y`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoScalar.NumericInt.BitwiseComplement.enabled`’.

NumericInt.BitwiseSubset

  Represents the bitwise subset invariant between two long scalars; that is, the bits of `y` are a subset of the bits of `x`. Prints as `x = y | x`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoScalar.NumericInt.BitwiseSubset.enabled`’.

NumericInt.Divides

  Represents the divides without remainder invariant between two long scalars. Prints as `x % y == 0`.

NumericInt.ShiftZero

  Represents the ShiftZero invariant between two long scalars; that is, `x` right-shifted by `y` is always zero. Prints as `x >> y = 0`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoScalar.NumericInt.ShiftZero.enabled`’.

NumericInt.Square

  Represents the square invariant between two long scalars. Prints as `x = y**2`.

NumericInt.ZeroTrack

  Represents the zero tracks invariant between two long scalars; that is, when `x` is zero, `y` is also zero. Prints as `x = 0 => y = 0`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoScalar.NumericInt.ZeroTrack.enabled`’.

OneOfFloat

  Represents double variables that take on only a few distinct values. Prints as either `x == c` (when there is only one value) or as `x one of {c1, c2, c3}` (when there are multiple values).

  See also the following configuration option:

  - ‘`daikon.inv.unary.scalar.OneOfFloat.size`’
OneOfFloatSequence

  Represents double[] variables that take on only a few distinct values. Prints as either `x == c` (when there is only one value) or as `x one of {c1, c2, c3}` (when there are multiple values).

  See also the following configuration option:

  - ‘`daikon.inv.unary.sequence.OneOfFloatSequence.size`’
OneOfScalar

  Represents long variables that take on only a few distinct values. Prints as either `x == c` (when there is only one value) or as `x one of {c1, c2, c3}` (when there are multiple values).

  May print as `x has only one value` when `x` is a hashcode (pointer) – this is because the numerical value of the hashcode (pointer) is uninteresting.

  See also the following configuration options:

  - ‘`daikon.inv.unary.scalar.OneOfScalar.size`’
  - ‘`daikon.inv.unary.scalar.OneOfScalar.omit_hashcode_values_Simplify`’
OneOfSequence

  Represents long[] variables that take on only a few distinct values. Prints as either `x == c` (when there is only one value) or as `x one of {c1, c2, c3}` (when there are multiple values).

  See also the following configuration options:

  - ‘`daikon.inv.unary.sequence.OneOfSequence.size`’
  - ‘`daikon.inv.unary.sequence.OneOfSequence.omit_hashcode_values_Simplify`’
OneOfString

  Represents String variables that take on only a few distinct values. Prints as either `x == c` (when there is only one value) or as `x one of {c1, c2, c3}` (when there are multiple values).

  See also the following configuration option:

  - ‘`daikon.inv.unary.string.OneOfString.size`’
OneOfStringSequence

  Represents String[] variables that take on only a few distinct values. Prints as either `x == c` (when there is only one value) or as `x one of {c1, c2, c3}` (when there are multiple values).

  See also the following configuration option:

  - ‘`daikon.inv.unary.stringsequence.OneOfStringSequence.size`’
PairwiseFloatEqual

  Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] == y[]`.

PairwiseFloatGreaterEqual

  Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] >= y[]`.

PairwiseFloatGreaterThan

  Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] > y[]`.

PairwiseFloatLessEqual

  Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] <= y[]`.

PairwiseFloatLessThan

  Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] < y[]`.

PairwiseIntEqual

  Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] == y[]`.

PairwiseIntGreaterEqual

  Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] >= y[]`.

PairwiseIntGreaterThan

  Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] > y[]`.

PairwiseIntLessEqual

  Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] <= y[]`.

PairwiseIntLessThan

  Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] < y[]`.

PairwiseLinearBinary

  Represents a linear invariant (i.e., `y = ax + b`) between the corresponding elements of two sequences of long values. Each `(x[i], y[i])` pair is examined. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]` and so forth. Prints as `y[] = a * x[] + b`.

PairwiseLinearBinaryFloat

  Represents a linear invariant (i.e., `y = ax + b`) between the corresponding elements of two sequences of double values. Each `(x[i], y[i])` pair is examined. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]` and so forth. Prints as `y[] = a * x[] + b`.

PairwiseNumericFloat.Divides

  Represents the divides without remainder invariant between corresponding elements of two sequences of double. Prints as `x[] % y[] == 0`.

PairwiseNumericFloat.Square

  Represents the square invariant between corresponding elements of two sequences of double. Prints as `x[] = y[]**2`.

PairwiseNumericFloat.ZeroTrack

  Represents the zero tracks invariant between corresponding elements of two sequences of double; that is, when `x[]` is zero, `y[]` is also zero. Prints as `x[] = 0 => y[] = 0`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.PairwiseNumericFloat.ZeroTrack.enabled`’.

PairwiseNumericInt.BitwiseAndZero

  Represents the BitwiseAnd == 0 invariant between corresponding elements of two sequences of long; that is, `x[]` and `y[]` have no bits in common. Prints as `x[] & y[] == 0`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseAndZero.enabled`’.

PairwiseNumericInt.BitwiseComplement

  Represents the bitwise complement invariant between corresponding elements of two sequences of long. Prints as `x[] = ~y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseComplement.enabled`’.

PairwiseNumericInt.BitwiseSubset

  Represents the bitwise subset invariant between corresponding elements of two sequences of long; that is, the bits of `y[]` are a subset of the bits of `x[]`. Prints as `x[] = y[] | x[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseSubset.enabled`’.

PairwiseNumericInt.Divides

  Represents the divides without remainder invariant between corresponding elements of two sequences of long. Prints as `x[] % y[] == 0`.

PairwiseNumericInt.ShiftZero

  Represents the ShiftZero invariant between corresponding elements of two sequences of long; that is, `x[]` right-shifted by `y[]` is always zero. Prints as `x[] >> y[] = 0`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.PairwiseNumericInt.ShiftZero.enabled`’.

PairwiseNumericInt.Square

  Represents the square invariant between corresponding elements of two sequences of long. Prints as `x[] = y[]**2`.

PairwiseNumericInt.ZeroTrack

  Represents the zero tracks invariant between corresponding elements of two sequences of long; that is, when `x[]` is zero, `y[]` is also zero. Prints as `x[] = 0 => y[] = 0`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.PairwiseNumericInt.ZeroTrack.enabled`’.

PairwiseString.SubString

  Represents the substring invariant between corresponding elements of two sequences of String. Prints as `x[] is a substring of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.PairwiseString.SubString.enabled`’.

PairwiseStringEqual

  Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] == y[]`.

PairwiseStringGreaterEqual

  Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] >= y[]`.

PairwiseStringGreaterThan

  Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] > y[]`.

PairwiseStringLessEqual

  Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] <= y[]`.

PairwiseStringLessThan

  Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each `(x[i], y[i])` pair. Thus, `x[0]` is compared to `y[0]`, `x[1]` to `y[1]`, and so forth. Prints as `x[] < y[]`.

Positive

  Represents the invariant `x > 0` where `x` is a long scalar. This exists only as an example for the purposes of the manual. It isn’t actually used (it is replaced by the more general invariant LowerBound).

PrintableString

  Represents a string that contains only printable ascii characters (values 32 through 126 plus 9 (tab).

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.string.PrintableString.enabled`’.

RangeFloat.EqualMinusOne

  Internal invariant representing double scalars that are equal to minus one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeFloat.EqualOne

  Internal invariant representing double scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeFloat.EqualZero

  Internal invariant representing double scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeFloat.GreaterEqual64

  Internal invariant representing double scalars that are greater than or equal to 64. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

RangeFloat.GreaterEqualZero

  Internal invariant representing double scalars that are greater than or equal to 0. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

RangeInt.BooleanVal

  Internal invariant representing longs whose values are always 0 or 1. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeInt.Bound0_63

  Internal invariant representing longs whose values are between 0 and 63. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

RangeInt.EqualMinusOne

  Internal invariant representing long scalars that are equal to minus one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeInt.EqualOne

  Internal invariant representing long scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeInt.EqualZero

  Internal invariant representing long scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeInt.Even

  Invariant representing longs whose values are always even. Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf invariants it is printed. Prints as `x is even`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.scalar.RangeInt.Even.enabled`’.

RangeInt.GreaterEqual64

  Internal invariant representing long scalars that are greater than or equal to 64. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

RangeInt.GreaterEqualZero

  Internal invariant representing long scalars that are greater than or equal to 0. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

RangeInt.PowerOfTwo

  Invariant representing longs whose values are always a power of 2 (exactly one bit is set). Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf invariants it is printed. Prints as `x is a power of 2`.

Reverse

  Represents two sequences of long where one is in the reverse order of the other. Prints as `x[] is the reverse of y[]`.

ReverseFloat

  Represents two sequences of double where one is in the reverse order of the other. Prints as `x[] is the reverse of y[]`.

SeqFloatEqual

  Represents an invariant between a double scalar and a a sequence of double values. Prints as `x[] elements == y` where `x` is a double sequence and `y` is a double scalar.

SeqFloatGreaterEqual

  Represents an invariant between a double scalar and a a sequence of double values. Prints as `x[] elements >= y` where `x` is a double sequence and `y` is a double scalar.

SeqFloatGreaterThan

  Represents an invariant between a double scalar and a a sequence of double values. Prints as `x[] elements > y` where `x` is a double sequence and `y` is a double scalar.

SeqFloatLessEqual

  Represents an invariant between a double scalar and a a sequence of double values. Prints as `x[] elements <= y` where `x` is a double sequence and `y` is a double scalar.

SeqFloatLessThan

  Represents an invariant between a double scalar and a a sequence of double values. Prints as `x[] elements < y` where `x` is a double sequence and `y` is a double scalar.

SeqIndexFloatEqual

  Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as `x[i] == i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexFloatEqual.enabled`’.

SeqIndexFloatGreaterEqual

  Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as `x[i] >= i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexFloatGreaterEqual.enabled`’.

SeqIndexFloatGreaterThan

  Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as `x[i] > i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexFloatGreaterThan.enabled`’.

SeqIndexFloatLessEqual

  Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as `x[i] <= i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexFloatLessEqual.enabled`’.

SeqIndexFloatLessThan

  Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as `x[i] < i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexFloatLessThan.enabled`’.

SeqIndexFloatNonEqual

  Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as `x[i] != i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexFloatNonEqual.enabled`’.

SeqIndexIntEqual

  Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as `x[i] == i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexIntEqual.enabled`’.

SeqIndexIntGreaterEqual

  Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as `x[i] >= i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexIntGreaterEqual.enabled`’.

SeqIndexIntGreaterThan

  Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as `x[i] > i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexIntGreaterThan.enabled`’.

SeqIndexIntLessEqual

  Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as `x[i] <= i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexIntLessEqual.enabled`’.

SeqIndexIntLessThan

  Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as `x[i] < i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexIntLessThan.enabled`’.

SeqIndexIntNonEqual

  Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as `x[i] != i`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.unary.sequence.SeqIndexIntNonEqual.enabled`’.

SeqIntEqual

  Represents an invariant between a long scalar and a a sequence of long values. Prints as `x[] elements == y` where `x` is a long sequence and `y` is a long scalar.

SeqIntGreaterEqual

  Represents an invariant between a long scalar and a a sequence of long values. Prints as `x[] elements >= y` where `x` is a long sequence and `y` is a long scalar.

SeqIntGreaterThan

  Represents an invariant between a long scalar and a a sequence of long values. Prints as `x[] elements > y` where `x` is a long sequence and `y` is a long scalar.

SeqIntLessEqual

  Represents an invariant between a long scalar and a a sequence of long values. Prints as `x[] elements <= y` where `x` is a long sequence and `y` is a long scalar.

SeqIntLessThan

  Represents an invariant between a long scalar and a a sequence of long values. Prints as `x[] elements < y` where `x` is a long sequence and `y` is a long scalar.

SeqSeqFloatEqual

  Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] == y[] lexically`.

  If order doesn’t matter for each variable, then the sequences are compared to see if they are set equivalent. Prints as `x[] == y[]`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqFloatGreaterEqual

  Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] >= y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqFloatGreaterThan

  Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] > y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqFloatLessEqual

  Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] <= y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqFloatLessThan

  Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] < y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntEqual

  Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] == y[] lexically`.

  If order doesn’t matter for each variable, then the sequences are compared to see if they are set equivalent. Prints as `x[] == y[]`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntGreaterEqual

  Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] >= y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntGreaterThan

  Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] > y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntLessEqual

  Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] <= y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntLessThan

  Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] < y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqStringEqual

  Represents invariants between two sequences of String values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] == y[] lexically`.

  If order doesn’t matter for each variable, then the sequences are compared to see if they are set equivalent. Prints as `x[] == y[]`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqStringGreaterEqual

  Represents invariants between two sequences of String values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] >= y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqStringGreaterThan

  Represents invariants between two sequences of String values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] > y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqStringLessEqual

  Represents invariants between two sequences of String values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] <= y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqStringLessThan

  Represents invariants between two sequences of String values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as `x[] < y[] lexically`.

  If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

StdString.SubString

  Represents the substring invariant between two String scalars. Prints as `x is a substring of y`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoString.StdString.SubString.enabled`’.

StringEqual

  Represents an invariant of == between two String scalars. Prints as `x == y`.

StringGreaterEqual

  Represents an invariant of >= between two String scalars. Prints as `x >= y`.

StringGreaterThan

  Represents an invariant of > between two String scalars. Prints as `x > y`.

StringLessEqual

  Represents an invariant of <= between two String scalars. Prints as `x <= y`.

StringLessThan

  Represents an invariant of < between two String scalars. Prints as `x < y`.

StringNonEqual

  Represents an invariant of != between two String scalars. Prints as `x != y`.

SubSequence

  Represents two sequences of long values where one sequence is a subsequence of the other. Prints as `x[] is a subsequence of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.SubSequence.enabled`’.

SubSequenceFloat

  Represents two sequences of double values where one sequence is a subsequence of the other. Prints as `x[] is a subsequence of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.SubSequenceFloat.enabled`’.

SubSet

  Represents two sequences of long values where one of the sequences is a subset of the other; that is each element of one sequence appears in the other. Prints as either `x[] is a subset of y[]` or as `x[] is a superset of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.SubSet.enabled`’.

SubSetFloat

  Represents two sequences of double values where one of the sequences is a subset of the other; that is each element of one sequence appears in the other. Prints as either `x[] is a subset of y[]` or as `x[] is a superset of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.SubSetFloat.enabled`’.

SuperSequence

  Represents two sequences of long values where one sequence is a subsequence of the other. Prints as `x[] is a subsequence of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.SuperSequence.enabled`’.

SuperSequenceFloat

  Represents two sequences of double values where one sequence is a subsequence of the other. Prints as `x[] is a subsequence of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.SuperSequenceFloat.enabled`’.

SuperSet

  Represents two sequences of long values where one of the sequences is a subset of the other; that is each element of one sequence appears in the other. Prints as either `x[] is a subset of y[]` or as `x[] is a superset of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.SuperSet.enabled`’.

SuperSetFloat

  Represents two sequences of double values where one of the sequences is a subset of the other; that is each element of one sequence appears in the other. Prints as either `x[] is a subset of y[]` or as `x[] is a superset of y[]`.

  This invariant is not enabled by default. See the configuration option ‘`daikon.inv.binary.twoSequence.SuperSetFloat.enabled`’.

UpperBound

  Represents the invariant `x <= c`, where `c` is a constant and `x` is a long scalar.

  See also the following configuration options:

  - ‘`daikon.inv.unary.scalar.UpperBound.minimal_interesting`’
  - ‘`daikon.inv.unary.scalar.UpperBound.maximal_interesting`’
UpperBoundFloat

  Represents the invariant `x <= c`, where `c` is a constant and `x` is a double scalar.

  See also the following configuration options:

  - ‘`daikon.inv.unary.scalar.UpperBoundFloat.minimal_interesting`’
  - ‘`daikon.inv.unary.scalar.UpperBoundFloat.maximal_interesting`’

Previous: Invariant list, Up: Daikon output [Contents][Index]

### 5.6 Invariant filters

Invariant filters are used to suppress the printing of invariants that are true, but not considered “interesting” — usually because the invariants are considered obvious or redundant in a given context.

The following is a list of the invariant filters that Daikon supports. Each of these filters has a corresponding configuration enable switch; by default, all filters are enabled. See Options to enable/disable filters, for details.

- DerivedParameterFilter: suppress parameter-derived postcondition invariants

  This filter suppresses invariants at procedure exit points that are uninteresting because they refer to ‘`pre-state`’ variables derived from pass-by-value parameters. For example, suppose that `param` is a parameter to a Java method. If `param` itself is modified, that change won’t be visible to a caller, so it’s uninteresting to print. If `param` points to an object, and that object is changed, that is visible, but only if `param` hasn’t changed; otherwise, the invariant would report a change in some object other than the one that was passed in.

- ObviousFilter: suppress “obvious”, or redundant, invariants — that is, invariants that are implied by some other invariant

  This filter suppresses any invariant that is a logical consequence of other invariants that are printed. This keeps the output from becoming cluttered with redundant facts. Some examples are:

  - If ‘`size(args[])==0`’ is shown, then ‘`size(args[])-1==-1`’ is obvious and will not be displayed by default.
  - If ‘`this.topOfStack < size(this.theArray[])-1`’ is shown, then ‘`this.topOfStack < size(this.theArray[])`’ is obvious and will not be displayed by default.

  To suppress even more invariants, use the `--suppress_redundant` command-line option; see Options to control invariant detection.

- OnlyConstantVariablesFilter: suppress invariants containing only constants

  This filter suppresses comparison invariants in which all of the variables being compared were observed to be constant. In the current version of Daikon, most such invariants are not even created in the first place, because constants are detected on an early pass over the data. However, Daikon will note that all of the invariants that had any particular constant value were also equal to each other: such invariants will be suppressed by this filter.

- ParentFilter: filter invariants that match a parent program point invariant

  A controlled invariant is an invariant that is “controlled” — or implied — by a parent program point in the dataflow hierarchy. For example, for Java instrumented code each class is associated with an object program point, which contain invariants that are found at the entry and exit of all public methods. So in addition to the usual program points such as `StackAr.StackAr(int):::ENTER` and `StackAr.isEmpty():::EXIT48`, Daikon outputs invariants for the artificial program point `StackAr:::OBJECT`. The invariants for `StackAr:::OBJECT` control the invariants for `StackAr.StackAr(int):::ENTER` and `StackAr.isEmpty():::EXIT48`, because the former imply the latter. Because of this redundancy, controlled invariants are not displayed by default. Note that if for some reason, the controlling invariant is not displayed (for example, because it’s unjustified), then the controlled invariant will be displayed.

- SimplifyFilter: eliminate redundant invariants using Simplify

  Daikon contains built-in test that remove most redundant (logically implied) invariants from its output; see

  Daikon can use the Simplify theorem-prover to eliminate even more implied invariants than Daikon’s built-in tests are able to eliminate. Simplify must be installed in order to take advantage of this filter (see Installing Simplify).

  If you don’t also specify the `--suppress_redundant` command-line option (see Options to control invariant detection) to enable Simplify processing, this filter doesn’t do anything.

- UnjustifiedFilter: suppress unjustified invariants

  For every invariant, Daikon estimates the probability of that invariant happening by chance. If that probability is less than the limit, then the invariant is deemed to be an actual invariant, not just a chance occurrence. Currently the limit is .01. So by default, only invariants with probabilities of less than 1% are shown. See the `--conf_limit` option (Options to control invariant detection).

- UnmodifiedVariableEqualityFilter: suppress invariants that merely indicate that a variable was unmodified

  This filter is only useful for `ESC` output.

Previous: Invariant list, Up: Daikon output [Contents][Index]