All Classes Interface Summary Class Summary Enum Summary Exception Summary Error Summary Annotation Types Summary
Class |
Description |
AbstractDeclarator |
|
AdditiveExpression |
|
AdditiveExpression |
|
AllocationExpression |
|
AllTestsSuite |
All Daikon's unit tests.
|
AndExpression |
|
ANDExpression |
|
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.
|
Annotate |
Merge Daikon-generated invariants into Java source code as ESC/JML/DBC annotations.
|
AnnotateNullable |
AnnotateNullable reads a Daikon invariant file and determines which reference variables have seen
any null values.
|
AnnotateVisitor |
|
Annotation |
Utility class to parse annotations generated with the Annotate program using the
--wrap_xml flag.
|
Annotation |
|
Annotation.Kind |
A class representing the kind of an annotation.
|
Annotation.MalformedAnnotationException |
Thrown by method get(String annoString) if annoString doesn't represent a well-formed
annotation.
|
AnnotationTypeBody |
|
AnnotationTypeDeclaration |
|
AnnotationTypeMemberDeclaration |
|
ArgumentExpressionList |
|
ArgumentList |
|
Arguments |
|
ArrayDimsAndInits |
|
ArrayInfo |
The ArrayInfo class is a subtype of DaikonVariableInfo used for variable types that are arrays
(i.e., their name ends with "[]").
|
ArrayInitializer |
|
ASCII_CharStream |
An implementation of interface CharStream, where the stream is assumed to
contain only ASCII characters (without unicode processing).
|
AssertStatement |
|
AssignmentExpression |
|
AssignmentOperator |
|
AssignmentOperator |
|
Ast |
Static methods for manipulating the AST.
|
BinaryDerivation |
Abstract class to represent a derived variable that came from two base variables.
|
BinaryDerivationFactory |
Factory to produce BinaryDerivation.
|
BinaryInvariant |
Provides a class that defines the functions that must exist for each two variable invariant.
|
Block |
|
BlockStatement |
|
BooleanLiteral |
|
BreakStatement |
|
BuildJDK |
BuildJDK uses DCInstrument to add comparability instrumentation to Java class files, then
stores the modified files into a directory identified by a (required) command line argument.
|
CallerContextSplitter |
This splitter tests the condition "$caller one of { some set of integers }".
|
CastExpression |
|
CastExpression |
|
CastLookahead |
|
CheckerClass |
Represents a class created by the instrumenter to check invariants.
|
CheckerClasses |
Represents a set of classes created by the instrumenter to check invariants.
|
Chicory |
This is the main class for Chicory which transforms the class files of a program to instrument it
for Daikon.
|
ChicoryPremain |
This class is the entry point for the Chicory instrumentation agent.
|
ChicoryPremain.ChicoryLoader |
Classloader for the BCEL code.
|
ClassInfo |
Keeps information about a class that is useful for writing out decl and/or dtrace information.
|
ClassOrInterfaceBody |
|
ClassOrInterfaceBodyDeclaration |
|
ClassOrInterfaceDeclaration |
|
ClassOrInterfaceType |
|
ClassOrInterfaceTypeDecorateVisitor |
Replaces uses of generic type parameters with versions that do not use generics.
|
Cmd |
|
CmdAssume |
An Assume command pushes some proposition onto the assumption stack of the session.
|
CmdCheck |
A Check command takes a given proposition and asks the Session to prove it.
|
CmdRaw |
A Raw command provides no additional structure, allowing arbitrary commands (as long as they have
no output) to be sent to the prover.
|
CmdUndoAssume |
An UndoAssume command removes an assumption from the assumption stack of the given session.
|
CommandHandler |
A command handler handles a set of commands.
|
Common |
A collection of useful helper methods that are common to many different individual tests.
|
CommonFloatSequence |
Represents sequences of double values that contain a common subset.
|
CommonSequence |
Represents sequences of long values that contain a common subset.
|
CommonStringSequence |
Represents string sequences that contain a common subset.
|
ComparabilityProvider |
|
CompilationUnit |
|
CompleteOneOfScalar |
Tracks every unique value and how many times it occurs.
|
CompleteOneOfScalar.Info |
Information about each value encountered.
|
CompleteOneOfString |
Tracks every unique value and how many times it occurs.
|
CompleteOneOfString.Info |
Information about each value encountered.
|
CompoundStatement |
|
ConditionalAndExpression |
|
ConditionalExpression |
|
ConditionalExpression |
|
ConditionalOrExpression |
|
ConditionPrinter |
|
Configuration |
This class applies settings from a configuration file that lists variable names and values (see
"example-settings.txt" in this directory for an example).
|
Configuration.ConfigException |
Lets callers differentiate between configuration problems and all others.
|
ConfigurationTest |
|
ConsequentCVFPairComparator |
Comparator for sorting invariants.
|
ConsequentCVFPairComparatorTester |
Daikon unit test class.
|
ConsequentCVFSortComparator |
Comparator for sorting invariants.
|
ConsequentCVFSortComparatorTester |
Daikon unit test class.
|
ConsequentExtractorVisitor |
ConsequentExtractorVisitor is a visitor that takes in RootNode tree used by the other
visitors in Diff and only modifies the first inv tree out of the pair of two inv trees (the
second tree is never read or modified).
|
ConsequentPairComparator |
Comparator for pairing invariants.
|
ConsequentSortComparator |
Comparator for sorting invariants.
|
Constant |
|
ConstantExpression |
|
ConstructorDeclaration |
|
ContextSplitterFactory |
This factory creates Splitters from map files.
|
ContextSplitterFactory.MapfileEntry |
Simple record type to store a map file entry.
|
ContextSplitterFactory.PptNameAndSplitters |
Simple record type to store a PptName and Splitter array.
|
ContinueStatement |
|
Converter |
|
CParser |
|
CParserConstants |
|
CParserTokenManager |
|
CreateSpinfo |
Create a splitter info file from Java source.
|
CreateSpinfoC |
|
Daikon |
|
Daikon.BugInDaikon |
Indicates that Daikon has terminated abnormally, indicating a bug in Daikon.
|
Daikon.DaikonTerminationException |
Indicates the need for Daikon to terminate.
|
Daikon.FileIOProgress |
Outputs FileIO progress information.
|
Daikon.FileOptions |
|
Daikon.NormalTermination |
Indicates that Daikon has terminated normally.
|
Daikon.ParseError |
A parser error that should be reported, with better context, by the caller.
|
Daikon.UserError |
Indicates a user error.
|
DaikonClassInfo |
The DaikonClassInfo class is a subtype of DaikonVariableInfo used for variables which represent
the run-time type of a variable.
|
DaikonSimple |
DaikonSimple reads a declaration file and trace file and outputs a list of likely invariants
using the simple incremental algorithm.
|
DaikonSimple.SimpleProcessor |
The SimpleProcessor class processes each sample in the dtrace file.
|
DaikonVariableInfo |
Each DaikonVariableInfo object is a node in the tree structure of the variables in the target
application.
|
DaikonWriter |
DaikonWriter is the parent class of DeclWriter and DTraceWriter.
|
DCInstrument |
Instruments a class file to perform Dynamic Comparability.
|
DCInstrument.JUnitState |
Possible states of JUnit test discovery.
|
DCompClone |
Classes implementing this interface have been instrumented by DynComp and have implemented a
clone method.
|
DCompInstrumented |
Classes implementing this interface have been instrumented by DynComp.
|
DCompMarker |
This is the type of the extra formal parameter in methods that have been instrumented by DynComp.
|
DCompToString |
Classes implementing this interface have been instrumented by DynComp and have implemented a
toString method.
|
DCRuntime |
Runtime support for DynComp, a comparability front end for Chicory.
|
DCRuntime.FieldTag |
Abstract base class for code that gets the tag associated with a particular field.
|
DCRuntime.PrimitiveArrayTag |
Class that gets the list of tags for primitive arrays.
|
DCRuntime.PrimitiveTag |
Class that gets the tag for a primitive instance field.
|
DCRuntime.ReferenceTag |
Class that returns the tag for a reference instance field.
|
DCRuntime.StaticPrimitiveTag |
Class that gets the tag for static primitive fields.
|
DCRuntime.StaticReferenceTag |
Class that gets the tag for a static reference variable.
|
Debug |
Debug class used with the logger to create standardized output.
|
Declaration |
|
DeclarationList |
|
DeclarationSpecifiers |
|
Declarator |
|
DeclReader |
Reads declaration files and provides methods to access the information within them.
|
DeclReader.DeclPpt |
Information about the program point that is contained in the decl file.
|
DeclReader.DeclVarInfo |
Information about variables within a program point.
|
DeclWriter |
DeclWriter writes the .decls file to a stream.
|
DefaultValue |
|
DepthFirstVisitor |
Provides default methods which visit each node in the tree in depth-first order.
|
DepthFirstVisitor |
Provides default methods which visit each node in the tree in depth-first
order.
|
DepthFirstVisitor |
Provides default methods which visit each node in the tree in depth-first
order.
|
Derivation |
Structure that represents a derivation; can generate values and derived variables from base
variables.
|
DerivationFactory |
Factory to create and describe derived variables.
|
DerivedParameterFilter |
Filter for not printing an Invariant if its VarInfos return isDerivedParameterAndUninteresting ==
true.
|
DerivedVariableFilter |
A filter that filters out invariants that contain derived variables of a specified derivation.
|
DetailedStatisticsVisitor |
Computes statistics about the differences between the sets of invariants.
|
DetailedStatisticsVisitorTester |
|
Diff |
Diff is the main class for the invariant diff program.
|
DiffDummyInvariant |
A dummy invariant used for testing purposes.
|
DiffTester |
|
DirectAbstractDeclarator |
|
DirectDeclarator |
|
DiscardCode |
DiscardCode is an enumeration type.
|
DiscardInfo |
A class used for holding a DiscardCode and a string that contains more detailed information about
why an Invariant was discarded, as well as the classname and what would be returned by the
Invariant's format() method.
|
DiscReasonMap |
|
DoStatement |
|
DotNetStringFilter |
Suppress string invariants that are redundant for .NET.
|
DtraceDiff |
This tool is used to find the differences between two dtrace files based on analysis of the
files' content, rather than a straight textual comparison.
|
DtraceDiff.DiffError |
Exception thrown for diffs.
|
DtraceDiffTester |
Daikon unit test class.
|
DtraceNonceFixer |
This tool fixes a Dtrace file whose invocation nonces became inaccurate as a result of a
cat command combining multiple dtrace files.
|
DtracePartitioner |
This class partitions Daikon trace files so that invocations of the same program point are
grouped together for use with random selection.
|
DTraceWriter |
DTraceWriter writes .dtrace program points to an output stream.
|
DummyInvariant |
This is a special invariant used internally by Daikon to represent invariants whose meaning
Daikon doesn't understand.
|
DynamicConstants |
Class that implements dynamic constants optimization.
|
DynamicConstants.ConIndexComparator |
Compares two constants based on the vi_index of their variable.
|
DynamicConstants.Constant |
Class used to indicate, for each variable, whether it is constant (see boolean field
"constant").
|
DynComp |
This is the main class for DynComp.
|
EltLowerBound |
Represents the invariant that each element of a sequence of long values is greater than or
equal to a constant.
|
EltLowerBoundFloat |
Represents the invariant that each element of a sequence of double values is greater than or
equal to a constant.
|
EltNonZero |
Represents the invariant "x !
|
EltNonZeroFloat |
Represents the invariant "x !
|
EltOneOf |
Represents sequences of long values where the elements of the sequence take on only a
few distinct values.
|
EltOneOfFloat |
Represents sequences of double values where the elements of the sequence take on only a
few distinct values.
|
EltOneOfString |
Represents sequences of String values where the elements of the sequence take on only a
few distinct values.
|
EltRangeFloat |
Baseclass for unary range based invariants.
|
EltRangeFloat.EqualMinusOne |
Internal invariant representing double scalars that are equal to minus one.
|
EltRangeFloat.EqualOne |
Internal invariant representing double scalars that are equal to one.
|
EltRangeFloat.EqualZero |
Internal invariant representing double scalars that are equal to zero.
|
EltRangeFloat.GreaterEqual64 |
Internal invariant representing double scalars that are greater than or equal to 64.
|
EltRangeFloat.GreaterEqualZero |
Internal invariant representing double scalars that are greater than or equal to 0.
|
EltRangeInt |
Baseclass for unary range based invariants.
|
EltRangeInt.BooleanVal |
Internal invariant representing longs whose values are always 0 or 1.
|
EltRangeInt.Bound0_63 |
Internal invariant representing longs whose values are between 0 and 63.
|
EltRangeInt.EqualMinusOne |
Internal invariant representing long scalars that are equal to minus one.
|
EltRangeInt.EqualOne |
Internal invariant representing long scalars that are equal to one.
|
EltRangeInt.EqualZero |
Internal invariant representing long scalars that are equal to zero.
|
EltRangeInt.Even |
Invariant representing longs whose values are always even.
|
EltRangeInt.GreaterEqual64 |
Internal invariant representing long scalars that are greater than or equal to 64.
|
EltRangeInt.GreaterEqualZero |
Internal invariant representing long scalars that are greater than or equal to 0.
|
EltRangeInt.PowerOfTwo |
Invariant representing longs whose values are always a power of 2 (exactly one bit is set).
|
EltUpperBound |
Represents the invariant that each element of a sequence of long values is less than or
equal to a constant.
|
EltUpperBoundFloat |
Represents the invariant that each element of a sequence of double values is less than or
equal to a constant.
|
EltwiseFloatComparison |
Abstract base class defined so that the different types of EltwiseIntComparison (and separately
EltwiseFloatComparison), at the current moment those are ==, !
|
EltwiseFloatEqual |
Represents equality between adjacent elements (x[i], x[i+1]) of a double sequence.
|
EltwiseFloatGreaterEqual |
Represents the invariant ≥ between adjacent elements
(x[i], x[i+1]) of a double sequence.
|
EltwiseFloatGreaterThan |
Represents the invariant > between adjacent elements
(x[i], x[i+1]) of a double sequence.
|
EltwiseFloatLessEqual |
Represents the invariant ≤ between adjacent elements
(x[i], x[i+1]) of a double sequence.
|
EltwiseFloatLessThan |
Represents the invariant < between adjacent elements
(x[i], x[i+1]) of a double sequence.
|
EltwiseIntComparison |
Abstract base class defined so that the different types of EltwiseIntComparison (and separately
EltwiseFloatComparison), at the current moment those are ==, !
|
EltwiseIntEqual |
Represents equality between adjacent elements (x[i], x[i+1]) of a long sequence.
|
EltwiseIntGreaterEqual |
Represents the invariant ≥ between adjacent elements
(x[i], x[i+1]) of a long sequence.
|
EltwiseIntGreaterThan |
Represents the invariant > between adjacent elements
(x[i], x[i+1]) of a long sequence.
|
EltwiseIntLessEqual |
Represents the invariant ≤ between adjacent elements
(x[i], x[i+1]) of a long sequence.
|
EltwiseIntLessThan |
Represents the invariant < between adjacent elements
(x[i], x[i+1]) of a long sequence.
|
EmptyStatement |
|
EnumBody |
|
EnumConstant |
|
EnumDeclaration |
|
Enumerator |
|
EnumeratorList |
|
EnumSpecifier |
|
Equality |
Keeps track of sets of variables that are equal.
|
EqualityComparison |
An interface satisfied by equality invariants such as = .
|
EqualityExpression |
|
EqualityExpression |
|
ExclusiveOrExpression |
|
ExclusiveORExpression |
|
ExplicitConstructorInvocation |
|
Expression |
|
Expression |
|
ExpressionStatement |
|
ExtendsList |
|
ExternalDeclaration |
|
ExtractConsequent |
Extract the consequents of all Implication invariants that are predicated by membership in a
cluster, from a .inv file.
|
FieldDeclaration |
|
FieldInfo |
The OjbectInfo class is a subtype of DaikonVariableInfo used for variable types which are class
fields.
|
FileCompiler |
|
FileIO |
File I/O utilities.
|
FileIO.ParentRelation |
Parents in the ppt/variable hierarchy for a particular program point.
|
FileIO.ParseState |
ParseState indicates:
Some global information about the state of the parser while reading a decl or dtrace
file.
|
FileIO.Processor |
A Processor is used to read a dtrace file.
|
FileIO.RecordType |
The type of the record that was most recently read.
|
FileIO.VarDefinition |
Class that holds information from the declaration record (in the file).
|
FloatEqual |
Represents an invariant of == between two double scalars.
|
FloatGreaterEqual |
Represents an invariant of ≥ between two double scalars.
|
FloatGreaterThan |
Represents an invariant of > between two double scalars.
|
FloatLessEqual |
Represents an invariant of ≤ between two double scalars.
|
FloatLessThan |
Represents an invariant of < between two double scalars.
|
FloatNonEqual |
Represents an invariant of !
|
ForInit |
|
FormalParameter |
|
FormalParameters |
|
ForStatement |
|
ForUpdate |
|
FunctionBinary |
Base class for each of the FunctionBinary functions and permutatons.
|
FunctionBinary.BitwiseAndLong_xyz |
Represents the invariant x = BitwiseAnd(y, z) over three long
scalars.
|
FunctionBinary.BitwiseAndLong_yxz |
Represents the invariant y = BitwiseAnd(x, z) over three long
scalars.
|
FunctionBinary.BitwiseAndLong_zxy |
Represents the invariant z = BitwiseAnd(x, y) over three long
scalars.
|
FunctionBinary.BitwiseOrLong_xyz |
Represents the invariant x = BitwiseOr(y, z) over three long
scalars.
|
FunctionBinary.BitwiseOrLong_yxz |
Represents the invariant y = BitwiseOr(x, z) over three long
scalars.
|
FunctionBinary.BitwiseOrLong_zxy |
Represents the invariant z = BitwiseOr(x, y) over three long
scalars.
|
FunctionBinary.BitwiseXorLong_xyz |
Represents the invariant x = BitwiseXor(y, z) over three long
scalars.
|
FunctionBinary.BitwiseXorLong_yxz |
Represents the invariant y = BitwiseXor(x, z) over three long
scalars.
|
FunctionBinary.BitwiseXorLong_zxy |
Represents the invariant z = BitwiseXor(x, y) over three long
scalars.
|
FunctionBinary.DivisionLong_xyz |
Represents the invariant x = Division(y, z) over three long
scalars.
|
FunctionBinary.DivisionLong_xzy |
Represents the invariant x = Division(z, y) over three long
scalars.
|
FunctionBinary.DivisionLong_yxz |
Represents the invariant y = Division(x, z) over three long
scalars.
|
FunctionBinary.DivisionLong_yzx |
Represents the invariant y = Division(z, x) over three long
scalars.
|
FunctionBinary.DivisionLong_zxy |
Represents the invariant z = Division(x, y) over three long
scalars.
|
FunctionBinary.DivisionLong_zyx |
Represents the invariant z = Division(y, x) over three long
scalars.
|
FunctionBinary.GcdLong_xyz |
Represents the invariant x = Gcd(y, z) over three long
scalars.
|
FunctionBinary.GcdLong_yxz |
Represents the invariant y = Gcd(x, z) over three long
scalars.
|
FunctionBinary.GcdLong_zxy |
Represents the invariant z = Gcd(x, y) over three long
scalars.
|
FunctionBinary.LogicalAndLong_xyz |
Represents the invariant x = LogicalAnd(y, z) over three long
scalars.
|
FunctionBinary.LogicalAndLong_yxz |
Represents the invariant y = LogicalAnd(x, z) over three long
scalars.
|
FunctionBinary.LogicalAndLong_zxy |
Represents the invariant z = LogicalAnd(x, y) over three long
scalars.
|
FunctionBinary.LogicalOrLong_xyz |
Represents the invariant x = LogicalOr(y, z) over three long
scalars.
|
FunctionBinary.LogicalOrLong_yxz |
Represents the invariant y = LogicalOr(x, z) over three long
scalars.
|
FunctionBinary.LogicalOrLong_zxy |
Represents the invariant z = LogicalOr(x, y) over three long
scalars.
|
FunctionBinary.LogicalXorLong_xyz |
Represents the invariant x = LogicalXor(y, z) over three long
scalars.
|
FunctionBinary.LogicalXorLong_yxz |
Represents the invariant y = LogicalXor(x, z) over three long
scalars.
|
FunctionBinary.LogicalXorLong_zxy |
Represents the invariant z = LogicalXor(x, y) over three long
scalars.
|
FunctionBinary.LshiftLong_xyz |
Represents the invariant x = Lshift(y, z) over three long
scalars.
|
FunctionBinary.LshiftLong_xzy |
Represents the invariant x = Lshift(z, y) over three long
scalars.
|
FunctionBinary.LshiftLong_yxz |
Represents the invariant y = Lshift(x, z) over three long
scalars.
|
FunctionBinary.LshiftLong_yzx |
Represents the invariant y = Lshift(z, x) over three long
scalars.
|
FunctionBinary.LshiftLong_zxy |
Represents the invariant z = Lshift(x, y) over three long
scalars.
|
FunctionBinary.LshiftLong_zyx |
Represents the invariant z = Lshift(y, x) over three long
scalars.
|
FunctionBinary.MaximumLong_xyz |
Represents the invariant x = Maximum(y, z) over three long
scalars.
|
FunctionBinary.MaximumLong_yxz |
Represents the invariant y = Maximum(x, z) over three long
scalars.
|
FunctionBinary.MaximumLong_zxy |
Represents the invariant z = Maximum(x, y) over three long
scalars.
|
FunctionBinary.MinimumLong_xyz |
Represents the invariant x = Minimum(y, z) over three long
scalars.
|
FunctionBinary.MinimumLong_yxz |
Represents the invariant y = Minimum(x, z) over three long
scalars.
|
FunctionBinary.MinimumLong_zxy |
Represents the invariant z = Minimum(x, y) over three long
scalars.
|
FunctionBinary.ModLong_xyz |
Represents the invariant x = Mod(y, z) over three long
scalars.
|
FunctionBinary.ModLong_xzy |
Represents the invariant x = Mod(z, y) over three long
scalars.
|
FunctionBinary.ModLong_yxz |
Represents the invariant y = Mod(x, z) over three long
scalars.
|
FunctionBinary.ModLong_yzx |
Represents the invariant y = Mod(z, x) over three long
scalars.
|
FunctionBinary.ModLong_zxy |
Represents the invariant z = Mod(x, y) over three long
scalars.
|
FunctionBinary.ModLong_zyx |
Represents the invariant z = Mod(y, x) over three long
scalars.
|
FunctionBinary.MultiplyLong_xyz |
Represents the invariant x = Multiply(y, z) over three long
scalars.
|
FunctionBinary.MultiplyLong_yxz |
Represents the invariant y = Multiply(x, z) over three long
scalars.
|
FunctionBinary.MultiplyLong_zxy |
Represents the invariant z = Multiply(x, y) over three long
scalars.
|
FunctionBinary.PowerLong_xyz |
Represents the invariant x = Power(y, z) over three long
scalars.
|
FunctionBinary.PowerLong_xzy |
Represents the invariant x = Power(z, y) over three long
scalars.
|
FunctionBinary.PowerLong_yxz |
Represents the invariant y = Power(x, z) over three long
scalars.
|
FunctionBinary.PowerLong_yzx |
Represents the invariant y = Power(z, x) over three long
scalars.
|
FunctionBinary.PowerLong_zxy |
Represents the invariant z = Power(x, y) over three long
scalars.
|
FunctionBinary.PowerLong_zyx |
Represents the invariant z = Power(y, x) over three long
scalars.
|
FunctionBinary.RshiftSignedLong_xyz |
Represents the invariant x = RshiftSigned(y, z) over three long
scalars.
|
FunctionBinary.RshiftSignedLong_xzy |
Represents the invariant x = RshiftSigned(z, y) over three long
scalars.
|
FunctionBinary.RshiftSignedLong_yxz |
Represents the invariant y = RshiftSigned(x, z) over three long
scalars.
|
FunctionBinary.RshiftSignedLong_yzx |
Represents the invariant y = RshiftSigned(z, x) over three long
scalars.
|
FunctionBinary.RshiftSignedLong_zxy |
Represents the invariant z = RshiftSigned(x, y) over three long
scalars.
|
FunctionBinary.RshiftSignedLong_zyx |
Represents the invariant z = RshiftSigned(y, x) over three long
scalars.
|
FunctionBinary.RshiftUnsignedLong_xyz |
Represents the invariant x = RshiftUnsigned(y, z) over three long
scalars.
|
FunctionBinary.RshiftUnsignedLong_xzy |
Represents the invariant x = RshiftUnsigned(z, y) over three long
scalars.
|
FunctionBinary.RshiftUnsignedLong_yxz |
Represents the invariant y = RshiftUnsigned(x, z) over three long
scalars.
|
FunctionBinary.RshiftUnsignedLong_yzx |
Represents the invariant y = RshiftUnsigned(z, x) over three long
scalars.
|
FunctionBinary.RshiftUnsignedLong_zxy |
Represents the invariant z = RshiftUnsigned(x, y) over three long
scalars.
|
FunctionBinary.RshiftUnsignedLong_zyx |
Represents the invariant z = RshiftUnsigned(y, x) over three long
scalars.
|
FunctionBinaryFloat |
Base class for each of the FunctionBinaryFloat functions and permutatons.
|
FunctionBinaryFloat.DivisionDouble_xyz |
Represents the invariant x = Division(y, z) over three double
scalars.
|
FunctionBinaryFloat.DivisionDouble_xzy |
Represents the invariant x = Division(z, y) over three double
scalars.
|
FunctionBinaryFloat.DivisionDouble_yxz |
Represents the invariant y = Division(x, z) over three double
scalars.
|
FunctionBinaryFloat.DivisionDouble_yzx |
Represents the invariant y = Division(z, x) over three double
scalars.
|
FunctionBinaryFloat.DivisionDouble_zxy |
Represents the invariant z = Division(x, y) over three double
scalars.
|
FunctionBinaryFloat.DivisionDouble_zyx |
Represents the invariant z = Division(y, x) over three double
scalars.
|
FunctionBinaryFloat.MaximumDouble_xyz |
Represents the invariant x = Maximum(y, z) over three double
scalars.
|
FunctionBinaryFloat.MaximumDouble_yxz |
Represents the invariant y = Maximum(x, z) over three double
scalars.
|
FunctionBinaryFloat.MaximumDouble_zxy |
Represents the invariant z = Maximum(x, y) over three double
scalars.
|
FunctionBinaryFloat.MinimumDouble_xyz |
Represents the invariant x = Minimum(y, z) over three double
scalars.
|
FunctionBinaryFloat.MinimumDouble_yxz |
Represents the invariant y = Minimum(x, z) over three double
scalars.
|
FunctionBinaryFloat.MinimumDouble_zxy |
Represents the invariant z = Minimum(x, y) over three double
scalars.
|
FunctionBinaryFloat.MultiplyDouble_xyz |
Represents the invariant x = Multiply(y, z) over three double
scalars.
|
FunctionBinaryFloat.MultiplyDouble_yxz |
Represents the invariant y = Multiply(x, z) over three double
scalars.
|
FunctionBinaryFloat.MultiplyDouble_zxy |
Represents the invariant z = Multiply(x, y) over three double
scalars.
|
FunctionBinaryFloat.PowerDouble_xyz |
Represents the invariant x = Power(y, z) over three double
scalars.
|
FunctionBinaryFloat.PowerDouble_xzy |
Represents the invariant x = Power(z, y) over three double
scalars.
|
FunctionBinaryFloat.PowerDouble_yxz |
Represents the invariant y = Power(x, z) over three double
scalars.
|
FunctionBinaryFloat.PowerDouble_yzx |
Represents the invariant y = Power(z, x) over three double
scalars.
|
FunctionBinaryFloat.PowerDouble_zxy |
Represents the invariant z = Power(x, y) over three double
scalars.
|
FunctionBinaryFloat.PowerDouble_zyx |
Represents the invariant z = Power(y, x) over three double
scalars.
|
FunctionDefinition |
|
GenericTestClass<A,B extends String,C,U> |
|
GJDepthFirst<R,A> |
Provides default methods which visit each node in the tree in depth-first
order.
|
GJNoArguDepthFirst<R> |
Provides default methods which visit each node in the tree in depth-first
order.
|
GJNoArguVisitor<R> |
All GJ visitors with no argument must implement this interface.
|
GJVisitor<R,A> |
All GJ visitors must implement this interface.
|
GJVoidDepthFirst<A> |
Provides default methods which visit each node in the tree in depth-first
order.
|
GJVoidVisitor<A> |
All GJ void visitors must implement this interface.
|
Global |
|
GuardingImplication |
This is a special implication invariant that guards any invariants that are over variables that
are sometimes missing.
|
HtmlToTexinfo |
Supplies a static method htmlToTexinfo that converts HTML to Texinfo format.
|
HtmlToTexinfoTest |
|
IdentifierList |
|
IfStatement |
|
ImplementsList |
|
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).
|
ImportDeclaration |
|
InclusiveOrExpression |
|
InclusiveORExpression |
|
InitDeclarator |
|
InitDeclaratorList |
|
Initializer |
|
Initializer |
|
InitializerList |
|
InsertCommentFormatter |
InsertCommentFormatter is a visitor that does not actually insert comments, but instead corrects
positioning fields of all the tokens in the tree to accomodate already-inserted comments, while
modifying the formatting as little as possible.
|
InstanceOfExpression |
|
Instrument |
The Instrument class is responsible for modifying another class' bytecode.
|
Instrument |
|
InstrumentHandler |
Instruments a file to check invariant violations at run time.
|
InstrumentVisitor |
Visitor that instruments a Java source file (i.e. adds code at certain places) to check invariant
violations at run time.
|
IntEqual |
Represents an invariant of == between two long scalars.
|
IntGreaterEqual |
Represents an invariant of ≥ between two long scalars.
|
IntGreaterThan |
Represents an invariant of > between two long scalars.
|
IntLessEqual |
Represents an invariant of ≤ between two long scalars.
|
IntLessThan |
Represents an invariant of < between two long scalars.
|
IntNonEqual |
Represents an invariant of !
|
Invariant |
Base implementation for Invariant objects.
|
Invariant.ClassVarnameComparator |
|
Invariant.ClassVarnameFormulaComparator |
Orders invariants by class, then variable names, then formula.
|
Invariant.InvariantComparatorForPrinting |
Compare based on arity, then printed representation.
|
Invariant.Match |
Class used as a key to store invariants in a MAP where their equality depends on the invariant
representing the same invariant (i.e., their class is the same) and the same internal state
(when multiple invariants with the same class are possible).
|
InvariantAddAndCheckTester |
This is a tester for the results of adding or checking an sample to an invariant.
|
InvariantChecker |
InvariantChecker reads an invariant file and trace file.
|
InvariantChecker.InvariantCheckProcessor |
|
InvariantDoclet |
InvariantDoclet is a Javadoc doclet that collects information about the invariants defined within
Daikon.
|
InvariantFilter |
|
InvariantFilters |
|
InvariantFormatTester |
This is a tester for the formatting of invariants in different modes that is configurable by file
input.
|
InvariantInfo |
Container class for holding all info needed to describe an Invariant.
|
InvariantLemma |
InvariantLemmas are Lemmas created by printing a Daikon invariant in Simplify format, sometimes
with some hacks.
|
InvariantStatus |
This class is an enumerated type representing the possible results of adding a sample to an
invariant.
|
InvariantTester |
Daikon unit test class.
|
InvDef |
Class that defines an invariant so that it can be searched for as part of suppression.
|
InvMap |
Maps ppts to lists of invariants.
|
InvMapTester |
|
InvMatch |
Functions that look for relationships between the invariants at different program points.
|
InvNode |
Contains a pair of Invariants.
|
InvTranslate |
Provides a variable translation over an invariant at one program point (perhaps in a different
program) to a similar invariant at a second program point.
|
IsPointer |
IsPointer is an invariant that heuristically determines whether an integer represents a pointer
(a 32-bit memory address).
|
IterationStatement |
|
JavaCharStream |
An implementation of interface CharStream, where the stream is assumed to
contain only ASCII characters (with java-like unicode escape processing).
|
JavaParser |
|
JavaParser.ModifierSet |
|
JavaParserConstants |
|
JavaParserTest |
|
JavaParserTokenManager |
|
Joiner |
|
JumpStatement |
|
LabeledStatement |
|
LabeledStatement |
|
Lemma |
A lemma is an object that wraps a Simplify formula representing some logical statement.
|
LemmaStack |
A stack of Lemmas that shadows the stack of assumptions that Simplify keeps.
|
LinearBinary |
Represents a Linear invariant between two long scalars x and y , of
the form ax + by + c = 0 .
|
LinearBinaryCore |
|
LinearBinaryCoreFloat |
|
LinearBinaryFloat |
Represents a Linear invariant between two double scalars x and y , of
the form ax + by + c = 0 .
|
LinearTernary |
Represents a Linear invariant over three long scalars x ,
y , and z , of the form
ax + by + cz + d = 0 .
|
LinearTernaryCore |
The LinearTernaryCore class is acts as the backend for the invariant (ax + by + cz + d = 0) by
processing samples and computing coefficients.
|
LinearTernaryCore.Flag |
|
LinearTernaryCore.Point |
|
LinearTernaryCoreFloat |
The LinearTernaryCore class is acts as the backend for the invariant (ax + by + cz + d = 0) by
processing samples and computing coefficients.
|
LinearTernaryCoreFloat.Flag |
|
LinearTernaryCoreFloat.Point |
|
LinearTernaryCoreTest |
Daikon unit test class.
|
LinearTernaryFloat |
Represents a Linear invariant over three double scalars x ,
y , and z , of the form
ax + by + cz + d = 0 .
|
ListInfo |
The ListInfo class is a subtype of DaikonVariableInfo used for variable types that implement
java.util.List .
|
Literal |
|
LocalVariableDeclaration |
|
LogHelper |
Standard methods for setting up logging.
|
LogHelper.DaikonLogFormatter |
|
LogicalANDExpression |
|
LogicalCompare |
This is a standalone program that compares the invariants from two versions of (and/or runs of) a
program, and determines using Simplify whether the invariants from one logically imply the
invariants from the other.
|
LogicalORExpression |
|
LowerBound |
Represents the invariant x >= c , where c is a constant and
x is a long scalar.
|
LowerBoundCore |
|
LowerBoundCoreFloat |
|
LowerBoundFloat |
Represents the invariant x >= c , where c is a constant and
x is a double scalar.
|
Main |
Main entrypoint for the instrumenter.
|
MalformedPropertyException |
Thrown when parsing the XML representation of a property, if the property is not well-formed.
|
MarkerAnnotation |
|
MatchCountVisitor |
MatchCountVisitor is a visitor that almost does the opposite of PrintDifferingInvariantsVisitor.
|
Member |
Represents long scalars that are always members of a sequence of long values.
|
MemberFloat |
Represents double scalars that are always members of a sequence of double values.
|
MemberSelector |
|
MemberString |
Represents String scalars that are always members of a sequence of String values.
|
MemberValue |
|
MemberValueArrayInitializer |
|
MemberValuePair |
|
MemberValuePairs |
|
MemMonitor |
|
MergeInvariants |
Merges invariants from multiple invariant files into a single invariant file.
|
MethodDeclaration |
|
MethodDeclarator |
|
MethodInfo |
Keeps information about a method that is useful for writing out decl and/or dtrace information.
|
MinusVisitor |
Computes A - B, where A and B are the two sets of invariants.
|
MinusVisitorTester |
|
MiscSplitters |
|
ModBitTracker |
ModBitTracker maintains a BitSet for each variable at a program point.
|
ModBitTrackerTest |
|
Modifiers |
|
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.
|
MultiDiff |
MultiDiff is an executable application that performs the same functionality as Diff with a
few key change.
|
MultiDiffVisitor |
MultiDiffVisitor is a state-storing NodeVisitor that works across multiple files
regardless of the current two-file infrastructure.
|
MultiplicativeExpression |
|
MultiplicativeExpression |
|
Name |
|
NameList |
|
NIS |
Main class for non-instantiating suppression.
|
NIS.SuppressionProcessor |
Signifies which algorithm is used by NIS to process suppressions.
|
NIS.SuppressState |
Possible states for suppressors and suppressions.
|
NISuppressee |
Defines a suppressee for non-instantiating suppression.
|
NISuppression |
Class that defines a single non-instantiating suppression.
|
NISuppressionSet |
Class that defines a set of non-instantiating suppressions for a single invariant (suppressee).
|
NISuppressor |
Class that defines a suppressor invariant for use in non-instantiating suppressions.
|
Node<CONTENT extends @Nullable Object,CHILD> |
All nodes must subclass this class.
|
Node |
The interface which all syntax tree classes must implement.
|
Node |
|
NodeChoice |
Represents a grammar choice, e.g. ( A | B )
|
NodeChoice |
|
NodeList |
Represents a grammar list, e.g. ( A )+
|
NodeList |
|
NodeListInterface |
The interface which NodeList, NodeListOptional, and NodeSequence
implement.
|
NodeListInterface |
|
NodeListOptional |
Represents an optional grammar list, e.g. ( A )*
|
NodeListOptional |
|
NodeOptional |
Represents an grammar optional node, e.g. ( A )?
|
NodeOptional |
|
NodeSequence |
Represents a sequence of nodes nested within a choice, list,
optional list, or optional, e.g. ( A B )+ or [ C D E ]
|
NodeSequence |
|
NodeToken |
Represents a single token in the grammar.
|
NodeToken |
|
NoDuplicates |
Represents sequences of long that contain no duplicate elements.
|
NoDuplicatesFloat |
Represents sequences of double that contain no duplicate elements.
|
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) .
|
NonPrototype |
|
NonsensicalList |
NonsensicalList is similar to NonsensicalObject but it is used for arrays whose value is
nonsensical.
|
NonsensicalObject |
A NonsensicalObject is used during data trace output for variables whose value is "nonsensical"
to print.
|
NonZero |
Represents long scalars that are non-zero.
|
NonZeroFloat |
Represents double scalars that are non-zero.
|
NormalAnnotation |
|
NullLiteral |
|
NullnessUtil |
Utility class for the Nullness Checker.
|
NumericFloat |
Baseclass for binary numeric invariants.
|
NumericFloat.Divides |
Represents the divides without remainder invariant between two double scalars.
|
NumericFloat.Square |
Represents the square invariant between two double scalars.
|
NumericFloat.ZeroTrack |
Represents the zero tracks invariant between
two double scalars; that is, when x is zero,
y is also zero.
|
NumericInt |
Baseclass for binary numeric invariants.
|
NumericInt.BitwiseAndZero |
Represents the BitwiseAnd == 0 invariant between two long scalars; that is, x and
y have no bits in common.
|
NumericInt.BitwiseComplement |
Represents the bitwise complement invariant between two long scalars.
|
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 .
|
NumericInt.Divides |
Represents the divides without remainder invariant between two long scalars.
|
NumericInt.ShiftZero |
Represents the ShiftZero invariant between two long scalars; that is, x
right-shifted by y is always zero.
|
NumericInt.Square |
Represents the square invariant between two long scalars.
|
NumericInt.ZeroTrack |
Represents the zero tracks invariant between
two long scalars; that is, when x is zero,
y is also zero.
|
ObviousFilter |
|
OneOf |
|
OneOfFloat |
Represents double variables that take on only a few distinct values.
|
OneOfFloatSequence |
Represents double[] variables that take on only a few distinct values.
|
OneOfScalar |
Represents long variables that take on only a few distinct values.
|
OneOfScalarTester |
|
OneOfSequence |
Represents long[] variables that take on only a few distinct values.
|
OneOfSequenceTester |
|
OneOfString |
Represents String variables that take on only a few distinct values.
|
OneOfStringSequence |
Represents String[] variables that take on only a few distinct values.
|
OnlyConstantVariablesFilter |
|
OrigModifier |
OrigModifier is a visitor that places "orig()" around varible names and correspondingly corrects
positioning fields of all the tokens in tree to accomodate the change.
|
OutputFormat |
Enumeration type for output style.
|
PackageDeclaration |
|
PairwiseFloatEqual |
Represents an invariant between corresponding elements of two sequences of double values.
|
PairwiseFloatGreaterEqual |
Represents an invariant between corresponding elements of two sequences of double values.
|
PairwiseFloatGreaterThan |
Represents an invariant between corresponding elements of two sequences of double values.
|
PairwiseFloatLessEqual |
Represents an invariant between corresponding elements of two sequences of double values.
|
PairwiseFloatLessThan |
Represents an invariant between corresponding elements of two sequences of double values.
|
PairwiseIntEqual |
Represents an invariant between corresponding elements of two sequences of long values.
|
PairwiseIntGreaterEqual |
Represents an invariant between corresponding elements of two sequences of long values.
|
PairwiseIntGreaterThan |
Represents an invariant between corresponding elements of two sequences of long values.
|
PairwiseIntLessEqual |
Represents an invariant between corresponding elements of two sequences of long values.
|
PairwiseIntLessThan |
Represents an invariant between corresponding elements of two sequences of long values.
|
PairwiseLinearBinary |
Represents a linear invariant (i.e., y = ax + b ) between the corresponding elements
of two sequences of long values.
|
PairwiseLinearBinaryFloat |
Represents a linear invariant (i.e., y = ax + b ) between the corresponding elements
of two sequences of double values.
|
PairwiseNumericFloat |
Baseclass for binary numeric invariants.
|
PairwiseNumericFloat.Divides |
Represents the divides without remainder invariant between corresponding elements of two sequences of double.
|
PairwiseNumericFloat.Square |
Represents the square invariant between corresponding elements of two sequences of double.
|
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.
|
PairwiseNumericInt |
Baseclass for binary numeric invariants.
|
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.
|
PairwiseNumericInt.BitwiseComplement |
Represents the bitwise complement invariant between corresponding elements of two sequences of long.
|
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[] .
|
PairwiseNumericInt.Divides |
Represents the divides without remainder invariant between corresponding elements of two sequences of long.
|
PairwiseNumericInt.ShiftZero |
Represents the ShiftZero invariant between corresponding elements of two sequences of long; that is, x[]
right-shifted by y[] is always zero.
|
PairwiseNumericInt.Square |
Represents the square invariant between corresponding elements of two sequences of long.
|
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.
|
PairwiseString |
Baseclass for binary numeric invariants.
|
PairwiseString.SubString |
Represents the substring invariant between corresponding elements of two sequences of String.
|
PairwiseStringEqual |
Represents an invariant between corresponding elements of two sequences of String values.
|
PairwiseStringGreaterEqual |
Represents an invariant between corresponding elements of two sequences of String values.
|
PairwiseStringGreaterThan |
Represents an invariant between corresponding elements of two sequences of String values.
|
PairwiseStringLessEqual |
Represents an invariant between corresponding elements of two sequences of String values.
|
PairwiseStringLessThan |
Represents an invariant between corresponding elements of two sequences of String values.
|
ParameterDeclaration |
|
ParameterDoclet |
ParameterDoclet is a JavaDoc doclet that collects information about the run-time configuration
options for the Daikon tools.
|
ParameterInfo |
The ParameterInfo class is a subtype of DaikonVariableInfo used for variable types which are
arguments to procedures.
|
ParameterList |
|
ParameterTypeList |
|
ParentFilter |
Filter for not printing invariants that have a matching invariant at their parent PPT.
|
ParseException |
This exception is thrown when parse errors are encountered.
|
ParseException |
This exception is thrown when parse errors are encountered.
|
ParseResults |
The wrapped result of parsing a .java source file.
|
Pointer |
|
Positive |
Represents the invariant x > 0 where x is a long scalar.
|
PostfixExpression |
|
PostfixExpression |
|
Ppt |
|
Ppt.NameComparator |
|
PptConditional |
|
PptMap |
Maps from a program point name (a String) to a PptTopLevel.
|
PptName |
PptName is an immutable ADT that represents naming data associated with a given program point,
such as the class or method.
|
PptNameMatcher |
Matches program point names with their corresponding MethodDeclaration's (or
ConstructorDeclaration's) in an AST.
|
PptNode |
Contains a pair of Ppts.
|
PptRelation |
Class that builds and describes relations in the ppt hierarchy.
|
PptRelation.PptRelationType |
The different ppt/variable hierarchy relationships.
|
PptSlice |
A Slice is a view of some of the variables for a program point.
|
PptSlice.ArityPptnameComparator |
This class is used for comparing PptSlice objects.
|
PptSlice.ArityVarnameComparator |
This class is used for comparing PptSlice objects.
|
PptSlice0 |
|
PptSlice1 |
Contains all of the invariants over a particular set of 1 variables.
|
PptSlice2 |
Contains all of the invariants over a particular set of 2 variables.
|
PptSlice3 |
Contains all of the invariants over a particular set of 3 variables.
|
PptSliceEquality |
Holds Equality invariants.
|
PptSliceEquality.EqualityComparator |
Order Equality invariants by the indices of leaders.
|
PptSplitter |
PptSplitter contains the splitter and its associated PptConditional ppts.
|
PptTopLevel |
All information about a single program point.
|
PptTopLevel.PptFlags |
Ppt attributes (specified in decl records)
|
PptTopLevel.PptType |
Possible types of program points.
|
PptTopLevel.SimplifyInclusionTester |
Interface used by mark_implied_via_simplify to determine what invariants should be considered
during the logical redundancy tests.
|
PptTopLevel.Stats |
Stores various statistics about a ppt.
|
PptTopLevel.ViewsIteratorIterator |
An iterator whose elements are themselves iterators that return invariants.
|
PreDecrementExpression |
|
PreIncrementExpression |
|
Premain |
This class is the entry point for the DynComp instrumentation agent.
|
Premain.ShutdownThread |
Shutdown thread that writes out the comparability results.
|
PrimaryExpression |
|
PrimaryExpression |
|
PrimaryPrefix |
|
PrimarySuffix |
|
PrimitiveType |
|
PrintableString |
Represents a string that contains only printable ascii characters (values 32 through 126 plus 9
(tab).
|
PrintAllVisitor |
Prints all the invariant pairs, including pairs containing identical invariants.
|
PrintDifferingInvariantsVisitor |
Prints the differing invariant pairs.
|
PrintDifferingInvariantsVisitorTester |
|
Printer |
|
PrintInvariants |
PrintInvariants prints a set of invariants from a .inv file.
|
PrintNullDiffVisitor |
PrintNullDiffVIsitor is a NodeVisitor that only reports an invariant as different when its
existence in one set is not in another set.
|
ProglangType |
Represents the type of a variable, for its declared type, dtrace file representation, and
internal representations.
|
ProglangTypeTest |
Test the ProglangType class.
|
Property |
A program property (currently, derived by Daikon).
|
Property.Kind |
A class representing the kind of an property.
|
Prototype |
The Prototype and NonPrototype qualifiers apply only to Invariant (and its subclasses).
|
PureMethodInfo |
The PureMethodInfo class is a subtype of DaikonVariableInfo used for "variable types" which
correspond to the values of pure method invocations.
|
Quant |
The Quant library provides routines that operate on arrays and collections.
|
Quantify |
Helper classes for quantification for various output formats.
|
Quantify.Constant |
Represents a constant integer.
|
Quantify.ESCQuantification |
Class that represents an ESC quantification over one or two variables.
|
Quantify.FreeVar |
Free variable normally used for quantification.
|
Quantify.Length |
Represents the length of a sequence and an optional offset.
|
Quantify.QuantFlags |
Flags describing how quantifications are to be built.
|
Quantify.QuantifyReturn |
|
Quantify.SimplifyQuantification |
Class that represents an Simplify quantification over one or two variables.
|
Quantify.Term |
Class the represents terms that can be used in variable expressions.
|
Quantify.VarPlusOffset |
Represents a Daikon variable with an optional integer offset.
|
RangeFloat |
Baseclass for unary range based invariants.
|
RangeFloat.EqualMinusOne |
Internal invariant representing double scalars that are equal to minus one.
|
RangeFloat.EqualOne |
Internal invariant representing double scalars that are equal to one.
|
RangeFloat.EqualZero |
Internal invariant representing double scalars that are equal to zero.
|
RangeFloat.GreaterEqual64 |
Internal invariant representing double scalars that are greater than or equal to 64.
|
RangeFloat.GreaterEqualZero |
Internal invariant representing double scalars that are greater than or equal to 0.
|
RangeInt |
Baseclass for unary range based invariants.
|
RangeInt.BooleanVal |
Internal invariant representing longs whose values are always 0 or 1.
|
RangeInt.Bound0_63 |
Internal invariant representing longs whose values are between 0 and 63.
|
RangeInt.EqualMinusOne |
Internal invariant representing long scalars that are equal to minus one.
|
RangeInt.EqualOne |
Internal invariant representing long scalars that are equal to one.
|
RangeInt.EqualZero |
Internal invariant representing long scalars that are equal to zero.
|
RangeInt.Even |
Invariant representing longs whose values are always even.
|
RangeInt.GreaterEqual64 |
Internal invariant representing long scalars that are greater than or equal to 64.
|
RangeInt.GreaterEqualZero |
Internal invariant representing long scalars that are greater than or equal to 0.
|
RangeInt.PowerOfTwo |
Invariant representing longs whose values are always a power of 2 (exactly one bit is set).
|
ReadonlyPrestateFilter |
|
ReadTrace |
A class that gives an example of how to use a FileIO.Processor object to read a trace file.
|
ReadTrace.CollectDataProcessor |
Populates the samples map with all the data read from the file.
|
ReferenceType |
|
RelationalExpression |
|
RelationalExpression |
|
ResultType |
|
ReturnInfo |
A subtype of DaikonVariableInfo used for variables that are returned from procedures.
|
ReturnStatement |
|
ReturnTrueSplitter |
|
Reverse |
Represents two sequences of long where one is in the reverse order of the other.
|
ReverseFloat |
Represents two sequences of double where one is in the reverse order of the other.
|
RootInfo |
This is a subtype of DaikonVariableInfo and is used as a "placeholder" for the root of the tree.
|
RootNode |
The root of the tree.
|
RSIGNEDSHIFT |
|
RUNSIGNEDSHIFT |
|
Runtime |
Runtime support for Chicory, the Daikon front end for Java.
|
Runtime |
If a class has been instrumented with the instrumenter, invariant violations are added to the
violations list.
|
Runtime.BooleanWrap |
wrapper used for boolean arguments.
|
Runtime.ByteWrap |
wrapper used for int arguments.
|
Runtime.CharWrap |
wrapper used for int arguments.
|
Runtime.DoubleWrap |
Wrapper used for double arguments.
|
Runtime.FloatWrap |
wrapper used for int arguments.
|
Runtime.IntWrap |
wrapper used for int arguments.
|
Runtime.LongWrap |
wrapper used for int arguments.
|
Runtime.PrimitiveWrapper |
|
Runtime.ShortWrap |
wrapper used for int arguments.
|
Runtime.TerminationMessage |
Thrown to indicate that main should not print a stack trace, but only print the message itself
to the user.
|
SampleTester |
This tests Daikon's state as samples are processed.
|
SelectionStatement |
|
SeqFloatEqual |
Represents an invariant between a double scalar and a a sequence of double values.
|
SeqFloatGreaterEqual |
Represents an invariant between a double scalar and a a sequence of double values.
|
SeqFloatGreaterThan |
Represents an invariant between a double scalar and a a sequence of double values.
|
SeqFloatLessEqual |
Represents an invariant between a double scalar and a a sequence of double values.
|
SeqFloatLessThan |
Represents an invariant between a double scalar and a a sequence of double values.
|
SeqIndexFloatEqual |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
SeqIndexFloatGreaterEqual |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
SeqIndexFloatGreaterThan |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
SeqIndexFloatLessEqual |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
SeqIndexFloatLessThan |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
SeqIndexFloatNonEqual |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
SeqIndexIntEqual |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
SeqIndexIntGreaterEqual |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
SeqIndexIntGreaterThan |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
SeqIndexIntLessEqual |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
SeqIndexIntLessThan |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
SeqIndexIntNonEqual |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
SeqIntEqual |
Represents an invariant between a long scalar and a a sequence of long values.
|
SeqIntGreaterEqual |
Represents an invariant between a long scalar and a a sequence of long values.
|
SeqIntGreaterThan |
Represents an invariant between a long scalar and a a sequence of long values.
|
SeqIntLessEqual |
Represents an invariant between a long scalar and a a sequence of long values.
|
SeqIntLessThan |
Represents an invariant between a long scalar and a a sequence of long values.
|
SeqSeqFloatEqual |
Represents invariants between two sequences of double values.
|
SeqSeqFloatGreaterEqual |
Represents invariants between two sequences of double values.
|
SeqSeqFloatGreaterThan |
Represents invariants between two sequences of double values.
|
SeqSeqFloatLessEqual |
Represents invariants between two sequences of double values.
|
SeqSeqFloatLessThan |
Represents invariants between two sequences of double values.
|
SeqSeqIntEqual |
Represents invariants between two sequences of long values.
|
SeqSeqIntGreaterEqual |
Represents invariants between two sequences of long values.
|
SeqSeqIntGreaterThan |
Represents invariants between two sequences of long values.
|
SeqSeqIntLessEqual |
Represents invariants between two sequences of long values.
|
SeqSeqIntLessThan |
Represents invariants between two sequences of long values.
|
SeqSeqStringEqual |
Represents invariants between two sequences of String values.
|
SeqSeqStringGreaterEqual |
Represents invariants between two sequences of String values.
|
SeqSeqStringGreaterThan |
Represents invariants between two sequences of String values.
|
SeqSeqStringLessEqual |
Represents invariants between two sequences of String values.
|
SeqSeqStringLessThan |
Represents invariants between two sequences of String values.
|
SequenceFloat |
Abstract base class for comparing double sequences to double variables.
|
SequenceFloatArbitrarySubsequence |
|
SequenceFloatArbitrarySubsequenceFactory |
|
SequenceFloatIntersection |
Intersection between two comparable sequences.
|
SequenceFloatIntersectionFactory |
|
SequenceFloatSubscript |
|
SequenceFloatSubscriptFactory |
|
SequenceFloatSubsequence |
|
SequenceFloatUnion |
Represents the setwise union of two base variables, each of which is a collection.
|
SequenceFloatUnionFactory |
|
SequenceInitial |
This represents a sequence element at a particular offset (such as first, second, penultimate,
last).
|
SequenceInitialFactory |
|
SequenceInitialFactoryFloat |
|
SequenceInitialFloat |
This represents a sequence element at a particular offset (such as first, second, penultimate,
last).
|
SequenceLength |
|
SequenceLengthFactory |
|
SequenceMax |
|
SequenceMin |
|
SequenceMinMaxSumFactory |
|
SequenceScalar |
Abstract base class for comparing long sequences to long variables.
|
SequenceScalarArbitrarySubsequence |
|
SequenceScalarArbitrarySubsequenceFactory |
|
SequenceScalarIntersection |
Intersection between two comparable sequences.
|
SequenceScalarIntersectionFactory |
|
SequenceScalarSubscript |
|
SequenceScalarSubscriptFactory |
|
SequenceScalarSubsequence |
|
SequenceScalarUnion |
Represents the setwise union of two base variables, each of which is a collection.
|
SequenceScalarUnionFactory |
|
SequencesConcat |
Represents the concatenation of two base variables.
|
SequencesConcatFactory |
Factory for SequencesConcat derived variables.
|
SequencesJoin |
Derived variable representing the "join" of two sequences.
|
SequencesJoinFactory |
Factory for SequencesJoin derived variables.
|
SequencesJoinFactoryFloat |
Factory for SequencesJoin derived variables.
|
SequencesJoinFloat |
Derived variable representing the "join" of two sequences.
|
SequencesPredicate |
Derived variable representing the selecting of elements of one sequence based on the values of
another sequence.
|
SequencesPredicateFactory |
Factory for SequencesPredicate derived variables.
|
SequencesPredicateFactoryFloat |
Factory for SequencesPredicate derived variables.
|
SequencesPredicateFloat |
Derived variable representing the selecting of elements of one sequence based on the values of
another sequence.
|
SequenceString |
Abstract base class for comparing String sequences to String variables.
|
SequenceStringArbitrarySubsequence |
|
SequenceStringArbitrarySubsequenceFactory |
|
SequenceStringIntersection |
Intersection between two comparable sequences.
|
SequenceStringIntersectionFactory |
|
SequenceStringSubscript |
|
SequenceStringSubscriptFactory |
|
SequenceStringSubsequence |
|
SequenceStringUnion |
Represents the setwise union of two base variables, each of which is a collection.
|
SequenceStringUnionFactory |
|
SequenceSubsequence |
Derivations of the form A[0..i] or A[i..end], derived from A and i.
|
SequenceSum |
|
Session |
A session is a channel to the Simplify theorem-proving tool.
|
SessionManager |
A SessionManager is a component which handles the threading interaction with the Session.
|
SharedData |
Data that is shared across Chicory.
|
ShiftExpression |
|
ShiftExpression |
|
SimplifyError |
Superclass of all RuntimeExceptions in this package.
|
SimplifyException |
Superclass of all checked exceptions in this package.
|
SimplifyFilter |
|
SimpUtil |
Utility functions for the simplify package.
|
SingleFloat |
Abstract base class for invariants over one variable of type double .
|
SingleFloatSequence |
Abstract base class for invariants over one variable of type double[] .
|
SingleMemberAnnotation |
|
SingleScalar |
Abstract base class for invariants over one numeric (scalar) variable, such as x != 0 .
|
SingleScalarSequence |
Abstract base class for invariants over one variable of type long[] .
|
SingleSequence |
Invariants on a single sequence (array) variable, such as a[] contains no duplicates .
|
SingleString |
Abstract base class for invariants over one variable of type String .
|
SingleStringSequence |
Abstract base class for invariants over one variable of type String[] .
|
SpecifierQualifierList |
|
SpinfoFile |
SpinfoFile stores information parsed from a .spinfo file.
|
SplitDtrace |
Takes one argument: a .dtrace or dtrace.gz file.
|
Splitter |
A Splitter represents a test that can be used to separate all samples into two parts.
|
SplitterExample |
|
SplitterFactory |
|
SplitterFactoryTest |
THIS CLASS WAS GENERATED BY SplitterFactoryTestUpdater.
|
SplitterFactoryTestUpdater |
This class's main method can be used to update both the target files of SplitterFactoryTest and
the code of the SplitterFactoryTest itself.
|
SplitterList |
|
SplitterObject |
A SplitterObject is the starting point for all the information we have about a splitting
condition.
|
Statement |
|
Statement |
|
StatementExpression |
|
StatementExpressionList |
|
StatementList |
|
StaticObjInfo |
The StaticObjInfo class is a subtype of DaikonVariableInfo used as a root for static variables
within a class (which are the only variables visible to static methods).
|
StdString |
Baseclass for binary numeric invariants.
|
StdString.SubString |
Represents the substring invariant between two String scalars.
|
StorageClassSpecifier |
|
StreamRedirectThread |
StreamRedirectThread is a thread that copies its input to its output and terminates when it
completes.
|
StringEqual |
Represents an invariant of == between two String scalars.
|
StringFinder |
Identifies the strings in an C AST
|
StringGreaterEqual |
Represents an invariant of ≥ between two String scalars.
|
StringGreaterThan |
Represents an invariant of > between two String scalars.
|
StringInfo |
The StringInfo class is a subtype of DaikonVariableInfo used for variable types that can be
converted into strings (.toString()).
|
StringLength |
Length of String variables.
|
StringLengthFactory |
|
StringLessEqual |
Represents an invariant of ≤ between two String scalars.
|
StringLessThan |
Represents an invariant of < between two String scalars.
|
StringNonEqual |
Represents an invariant of !
|
StructDeclaration |
|
StructDeclarationList |
|
StructDeclarator |
|
StructDeclaratorList |
|
StructOrUnion |
|
StructOrUnionSpecifier |
|
SubSequence |
Represents two sequences of long values where one sequence is a subsequence of the
other.
|
SubSequenceFloat |
Represents two sequences of double values where one sequence is a subsequence of the
other.
|
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.
|
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.
|
SuperSequence |
Represents two sequences of long values where one sequence is a subsequence of the
other.
|
SuperSequenceFloat |
Represents two sequences of double values where one sequence is a subsequence of the
other.
|
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.
|
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.
|
SwitchLabel |
|
SwitchStatement |
|
SynchronizedStatement |
|
TernaryDerivation |
Abstract class to represent a derived variable that came from three base variables.
|
TernaryDerivationFactory |
Factory to produce TernaryDerivations.
|
TernaryInvariant |
|
TestAnnotate |
Tests that Annotate respects tabs.
|
TestAst |
Tests functionality of some methods in daikon.tools.jtb.Ast.
|
TestAst.ClassOrInterfaceDeclarationHarvester |
|
TestAst.MethodDeclarationHarvester |
|
TestClassOrInterfaceTypeDecorateVisitor |
|
TestClassOrInterfaceTypeDecorateVisitor.UngenerifiedTypeCollector |
|
TestQuant |
|
TestQuant.Bar1 |
|
TestQuant.Bar3 |
|
TestQuant.Bar3a |
|
TestQuant.Bar4 |
|
TestQuant.Bar4f |
|
TestQuant.Baz1 |
|
TestQuant.Baz1f |
|
TestQuant.Baz3 |
|
TestQuant.Baz3a |
|
TestQuant.Baz4 |
|
TestQuant.Foo1 |
|
TestQuant.Foo2 |
|
TestQuant.Foo2f |
|
TestQuant.Foo3 |
|
TestQuant.Foo3a |
|
TestQuant.Foo3af |
|
TestQuant.Foo3f |
|
TestQuant.Foo4 |
|
ThisObjInfo |
The ThisObjInfo class is a subtype of DaikonVariableInfo used for variable types which represent
the "this" object.
|
ThreeFloat |
Abstract base class for invariants over three numeric variables.
|
ThreeScalar |
Abstract base class for invariants over three numeric variables.
|
ThrowStatement |
|
TimeoutException |
Indicates a request timed out.
|
Token |
Describes the input token stream.
|
Token |
Describes the input token stream.
|
Token.GTToken |
|
TokenMgrError |
|
TokenMgrError |
|
TraceSelect |
The TraceSelect tool creates several small subsets of the data by randomly selecting parts of the
original trace file.
|
TranslationUnit |
|
TreeDumper |
|
TreeFormatter |
|
TryStatement |
|
TwoFloat |
Base class for invariants over two variables of type double.
|
TwoScalar |
Base class for invariants over two variables of type long.
|
TwoSequence |
Base class for invariants over two variables of type long[].
|
TwoSequenceFloat |
Base class for invariants over two variables of type double[].
|
TwoSequenceString |
Base class for invariants over two variables of type String[].
|
TwoString |
Base class for invariants over two variables of type String.
|
Type |
|
TypeArgument |
|
TypeArguments |
|
TypeBound |
|
TypeDeclaration |
|
TypedefName |
|
TypeName |
|
TypeParameter |
|
TypeParameters |
|
TypeQualifier |
|
TypeQualifierList |
|
TypeSpecifier |
|
UnaryDerivation |
|
UnaryDerivationFactory |
|
UnaryExpression |
|
UnaryExpression |
|
UnaryExpressionNotPlusMinus |
|
UnaryInvariant |
Exists simply to provide the do-nothing resusurrect_done method and abstract add method.
|
UnaryOperator |
|
UnionInvariants |
UnionInvariants is a command-line tool that will read in one (or more) .inv files
(possibly gzipped) and write their union into a new .inv file (possibly gzipped).
|
UnionVisitor |
Computes A union B, where A and B are the two sets of invariants.
|
UnionVisitorTester |
|
UnjustifiedFilter |
|
UnmodifiedVariableEqualityFilter |
Suppress invariants that merely indicate that a variable was unmodified.
|
UpperBound |
Represents the invariant x <= c , where c is a constant and
x is a long scalar.
|
UpperBoundCore |
|
UpperBoundCoreFloat |
|
UpperBoundFloat |
Represents the invariant x <= c , where c is a constant and
x is a double scalar.
|
ValueAndModified |
This is a temporary structure for grouping elements to be returned from computeValueAndModified,
not for permanent storage.
|
ValueIndex |
An index into a ValueTuple or list of values.
|
ValueSet |
ValueSet stores a set of values.
|
ValueSet.ValueSetFloat |
|
ValueSet.ValueSetFloatArray |
|
ValueSet.ValueSetScalar |
|
ValueSet.ValueSetScalarArray |
|
ValueSet.ValueSetString |
|
ValueSet.ValueSetStringArray |
|
ValueTuple |
This data structure holds a tuple of values for a particular program point.
|
VarComparability |
Represents the comparability of variables, including methods to determine if two
VarComparabilities are comparable.
|
VarComparabilityImplicit |
A VarComparabilityImplicit is an arbitrary integer, and comparisons succeed exactly if the two
integers are equal, except that negative integers compare equal to everything.
|
VarComparabilityNone |
Used when no VarComparability information is available (in the .dtrace file).
|
VarComparabilityTest |
|
VarFlags |
An enumeration of various flags that give information about variables.
|
VariableDeclarator |
|
VariableDeclaratorId |
|
VariableFilter |
|
VariableInitializer |
|
VarIndex |
An index into a list of VarInfo objects.
|
VarInfo |
Represents information about a particular variable for a program point.
|
VarInfo.IndexComparator |
Compare names by index.
|
VarInfo.LangFlags |
|
VarInfo.Pair |
Class used to contain a pair of VarInfos and their sample count.
|
VarInfo.RefType |
|
VarInfo.VarFlags |
|
VarInfo.VarKind |
|
VarInfoAux |
Represents additional information about a VarInfo that front ends tell Daikon.
|
VarInfoName |
VarInfoName represents the "name" of a variable.
|
VarInfoName.AbstractVisitor<T> |
Traverse the tree elements that have exactly one branch (so the traversal order doesn't
matter).
|
VarInfoName.Add |
An integer amount more or less than some other value, like "x+2".
|
VarInfoName.BooleanAndVisitor |
|
VarInfoName.Elements |
The elements of a container, like "term[]".
|
VarInfoName.ElementsFinder |
Use to traverse a tree, find the first (elements ...) node, and report whether it's in pre or
post-state.
|
VarInfoName.Field |
A 'getter' operation for some field, like a.foo.
|
VarInfoName.Finder |
Finds if a given VarInfoName is contained in a set of nodes in the VarInfoName tree using ==
comparison.
|
VarInfoName.FunctionOf |
A function over a term, like "sum(argument)".
|
VarInfoName.FunctionOfN |
A function of multiple parameters.
|
VarInfoName.InorderFlattener |
Use to collect all elements in a tree into an inorder-traversal list.
|
VarInfoName.Intersection |
Intersection of two sequences.
|
VarInfoName.IsAllNonPoststateVisitor |
|
VarInfoName.IsAllPrestateVisitor |
|
VarInfoName.LexicalComparator |
Compare VarInfoNames alphabetically.
|
VarInfoName.NodeFinder |
Use to report whether a node is in a pre- or post-state context.
|
VarInfoName.NoReturnValue |
|
VarInfoName.PostPreConverter |
Replace pre states by normal variables, and normal variables by post states.
|
VarInfoName.Poststate |
The poststate value of a term, like "new(term)".
|
VarInfoName.Prestate |
The prestate value of a term, like "orig(term)" or "\old(term)".
|
VarInfoName.QuantHelper |
Helper for writing parts of quantification expressions.
|
VarInfoName.QuantHelper.FreeVar |
A FreeVar is very much like a Simple, except that it doesn't care if it's in prestate or
poststate for simplify formatting.
|
VarInfoName.QuantHelper.QuantifyReturn |
Record type for return value of the quantify method below.
|
VarInfoName.QuantifierVisitor |
A quantifier visitor can be used to search a tree and return all unquantified sequences (e.g.
|
VarInfoName.Replacer |
A Replacer is a Visitor that makes a copy of a tree, but replaces some node (and its children)
with another.
|
VarInfoName.Simple |
A simple identifier like "a", etc.
|
VarInfoName.SimpleNamesVisitor |
|
VarInfoName.SizeOf |
The size of a contained sequence; form is like "size(sequence)" or "sequence.length".
|
VarInfoName.Slice |
A slice of elements from a sequence, like "sequence[i..j]".
|
VarInfoName.Subscript |
An element from a sequence, like "sequence[index]".
|
VarInfoName.Transformer |
Specifies a function that performs a transformation on VarInfoNames.
|
VarInfoName.TypeOf |
The type of the term, like "term.getClass().getName()" or "\typeof(term)".
|
VarInfoName.Union |
Union of two sequences.
|
VarInfoName.Visitor<T> |
Visitor framework for processing of VarInfoNames.
|
VarInfoNameDriver |
This is called by VarInfoName to parse varInfoNameTestfoo files and then apply various
transformation tests on them.
|
VarInfoNameDriver.Handler |
|
VarInfoNameTest |
This tests various aspects of VarInfoName's and transforming VarInfoName's.
|
VarKind |
An enumeration of the various kinds of variables.
|
VarParent |
Represents a parent of a variable.
|
VIndexBottom |
|
VIndexTop |
|
VIndexUnqualified |
Not an index into a ValueTuple nor into a list of VarInfo objects.
|
Violation |
Represents a violation of a Property .
|
Violation.Time |
Indicates at which program point the violation occurred: at method entry or method exit.
|
Visitor |
All visitors must implement this interface.
|
Visitor |
All visitors must implement this interface.
|
Visitor |
All void visitors must implement this interface.
|
WhileStatement |
|
WildcardBounds |
|
XorInvariantsVisitor |
XorInvariantsVisitor is a visitor that performs a standard Diff on two PptMaps, that is,
finds the set of Invariants in the XOR set of two PptMaps.
|
XorVisitor |
Computes A xor B, where A and B are the two sets of invariants.
|
XorVisitorTester |
|