[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 section Printing invariants) in a variety of formats, to insert the invariants in your source code (see section Annotate), to perform run-time checking of the invariants (see Runtime-check instrumenter (runtimechecker), and InvariantChecker), and to do various other operations. See Tools for use with Daikon, 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.
5.1 Invariant syntax | ||
5.2 Program points | ||
5.3 Variable names | ||
5.4 Interpreting Daikon output | ||
5.5 Invariant list | ||
5.6 Invariant filters |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 section Options to control Daikon output), PrintInvariants (see section Printing invariants), and Annotate (see section 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 (./developer)New formatting for invariants section ‘New formatting for invariants’ in Daikon Developer Manual.
Daikon’s default format is a mix of Java, mathematical logic, and some additional extensions. It is intended to concisely convey meaning to programmers.
This format produces output in the design-by-contract (DBC) format expected by Parasoft’s Jtest tool (http://www.parasoft.com).
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 http://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.
Write output as Java expressions. This means that each invariant would be 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.
Produces output in JML (Java Modeling Language, http://www.jmlspecs.org); for details, see the JML Manual. JML format lets you use the various JML tools on Daikon invariants, including runtime assertion checking and the ESC/Java2 tool.
Produces output in the format expected by the Simplify automated theorem prover; for details, see the Simplify distribution.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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
(./developer)Dataflow hierarchy section ‘Dataflow hierarchy’ in Daikon Developer Manual.
Two other 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.)
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 the JVML format: one character for each primitive type (‘B’ for byte, ‘C’ for character, ‘Z’ for boolean (so as not to clash with byte), etc.); ‘Lclassname;’ for object types; and a ‘[’ prefix for each level of array nesting.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 (./developer)Nonsensical values section ‘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 multi-dimensional 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.
x.getClass()
is the runtime 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 section orig() variable example.
This variable prints as orig
when using Daikon output format
(see section 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 may be used only in a
pre-state context and specifies an expression to be evaluated in the
post-state. See section 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.)
5.3.1 orig() variable example |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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]
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 section 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 section General configuration options).
5.4.1 Redundant invariants | ||
5.4.2 Equal variables | ||
5.4.3 Has only one value variables |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 section 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 section Printing invariants) or Diff (see section Invariant Diff) programs to print the results.)
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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; (./developer)Variable comparability section ‘Variable comparability’ in Daikon Developer Manual.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 this means that the variable is a hashcode or address — that is, its declared type is ‘hashcode’ (see (./developer)Variable declarations section ‘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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 section Options to enable/disable specific invariants.
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.
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:
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:
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’.
Tracks every unique value and how many times it occurs.
This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.scalar.CompleteOneOfScalar.enabled’.
Tracks every unique value and how many times it occurs.
This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.string.CompleteOneOfString.enabled’.
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.
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, then the configuration option ‘daikon.split.PptSplitter.dummy_invariant_level’ must be set, and formatting information must be supplied in the splitter info file.
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:
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:
Represents the invariant "x != 0" where x represents all of the elements of a sequence of long. Prints as ‘x[] elements != 0’.
Represents the invariant "x != 0" where x represents all of the elements of a sequence of double. Prints as ‘x[] elements != 0’.
Represents sequences of long values where the elements of the sequence 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:
Represents sequences of double values where the elements of the sequence 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:
Represents sequences of String values where the elements of the sequence 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:
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
Internal invariant representing double scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing
Internal invariant representing double scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.
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
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
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.
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.
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
Internal invariant representing long scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing
Internal invariant representing long scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.
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.
This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.EltRangeInt.Even.enabled’.
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
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
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.
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:
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:
Represents equality between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] elements are equal’.
Represents the invariant ">=" between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] sorted by ">="’.
Represents the invariant ">" between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] sorted by ">"’.
Represents the invariant "<=" between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] sorted by "<="’.
Represents the invariant "<" between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] sorted by "<"’.
Represents equality between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] elements are equal’.
Represents the invariant ">=" between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] sorted by ">="’.
Represents the invariant ">" between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] sorted by ">"’.
Represents the invariant "<=" between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] sorted by "<="’.
Represents the invariant "<" between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] sorted by "<"’.
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’.
Represents an invariant of "==" between two double scalars.
Represents an invariant of ">=" between two double scalars.
Represents an invariant of ">" between two double scalars.
Represents an invariant of "<=" between two double scalars.
Represents an invariant of "<" between two double scalars.
Represents an invariant of "!=" between two double scalars.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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’.
The Implication invariant class is used internally within Daikon to handle invariants that are only true when certain other conditions are also true (splitting).
Represents an invariant of "==" between two long scalars.
Represents an invariant of ">=" between two long scalars.
Represents an invariant of ">" between two long scalars.
Represents an invariant of "<=" between two long scalars.
Represents an invariant of "<" between two long scalars.
Represents an invariant of "!=" between two long scalars.
See also the following configuration option:
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,00 (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’.
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.
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.
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.
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.
Represents the invariant ‘x >= c’, where ‘c’ is a constant and ‘x’ is a long scalar.
See also the following configuration options:
Represents the invariant ‘x >= c’, where ‘c’ is a constant and ‘x’ is a double scalar.
See also the following configuration options:
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.
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.
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.
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’.
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’.
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’.
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’.
Represents long scalars that are non-zero. Prints as ‘x != 0’, or as ‘x != null’ for pointer types.
Represents double scalars that are non-zero. Prints as ‘x != 0’.
Represents the divides without remainder invariant between two double scalars. Prints as ‘x % y == 0’.
Represents the square invariant between two double scalars. Prints as ‘x = y**2’.
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’.
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’.
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’.
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’.
Represents the divides without remainder invariant between two long scalars. Prints as ‘x % y == 0’.
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’.
Represents the square invariant between two long scalars. Prints as ‘x = y**2’.
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’.
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:
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:
Represents long scalars that take on only a few distinct values. Prints as either ‘x == c’ (when there is only one value), ‘x one of {c1, c2, c3}’ (when there are multiple values), or ‘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:
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:
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:
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:
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[]’.
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[]’.
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[]’.
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[]’.
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[]’.
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[]’.
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[]’.
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[]’.
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[]’.
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[]’.
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’.
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’.
Represents the divides without remainder invariant between corresponding elements of two sequences of double. Prints as ‘x[] % y[] == 0’.
Represents the square invariant between corresponding elements of two sequences of double. Prints as ‘x[] = y[]**2’.
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’.
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’.
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’.
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’.
Represents the divides without remainder invariant between corresponding elements of two sequences of long. Prints as ‘x[] % y[] == 0’.
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’.
Represents the square invariant between corresponding elements of two sequences of long. Prints as ‘x[] = y[]**2’.
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’.
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’.
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[]’.
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[]’.
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[]’.
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[]’.
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[]’.
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).
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’.
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
Internal invariant representing double scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing
Internal invariant representing double scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.
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
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
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.
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.
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
Internal invariant representing long scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing
Internal invariant representing long scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.
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.
This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.scalar.RangeInt.Even.enabled’.
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
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
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.
Represents two sequences of long where one is in the reverse order of the other. Prints as ‘x[] is the reverse of y[]’.
Represents two sequences of double where one is in the reverse order of the other. Prints as ‘x[] is the reverse of y[]’.
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.
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.
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.
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.
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.
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’.
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’.
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’.
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’.
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’.
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’.
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’.
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’.
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’.
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’.
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’.
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’.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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’.
Represents an invariant of "==" between two String scalars.
Represents an invariant of ">=" between two String scalars.
Represents an invariant of ">" between two String scalars.
Represents an invariant of "<=" between two String scalars.
Represents an invariant of "<" between two String scalars.
Represents an invariant of "!=" between two String scalars.
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’.
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’.
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’.
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’.
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’.
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’.
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’.
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’.
Represents the invariant ‘x <= c’, where ‘c’ is a constant and ‘x’ is a long scalar.
See also the following configuration options:
Represents the invariant ‘x <= c’, where ‘c’ is a constant and ‘x’ is a double scalar.
See also the following configuration options:
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 section Options to enable/disable filters, for details.
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.
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:
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.
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.
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 separately obtained (from http://www.hpl.hp.com/downloads/crl/jtk/) and installed in order to take advantage of this filter.
If you don’t also specify the ‘--suppress_redundant’ command-line option (see section Options to control invariant detection) to enable Simplify processing, this filter doesn’t do anything.
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 (see section Options to control invariant detection).
This filter is only useful for ESC output.