Package daikon.inv

Class InvDef

Object

InvDef

public class InvDef
extends Object

Class that defines an invariant so that it can be searched for as part of suppression.

Field Summary

Fields

Modifier and Type	Field	Description
static Logger	debug	Debug tracer.
static long[]	elts_minus_one	The array {-1}.
static long[]	elts_minus_one_and_plus_one	The array {-1, 1}.
static double[]	elts_minus_one_and_plus_one_float	The array {-1.0, 1.0}.
static double[]	elts_minus_one_float	The array {-1.0}.
static long[]	elts_one	The array {1}.
static double[]	elts_one_float	The array {1.0}.
static long[]	elts_zero	The array {0}.
static double[]	elts_zero_float	The array {0.0}.

Constructor Summary

Constructors

Constructor	Description
InvDef(VarInfo v1, VarInfo v2, Class<? extends Invariant> cls)
InvDef(VarInfo v1, Class<? extends Invariant> cls)	Create a new InvDef with one variable.
InvDef(VarInfo v1, Class<? extends Invariant> cls, @Nullable Object state)	Create a new InvDef with one variable and the given state

Method Summary

Modifier and Type	Method	Description
boolean	check(Invariant inv)
@Nullable Invariant	find()	Looks for this invariant (in this ppt).
String	toString()

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

debug

public static final Logger debug

Debug tracer.

elts_zero

public static final long[] elts_zero

The array {0}.

elts_zero_float

public static final double[] elts_zero_float

The array {0.0}.

elts_minus_one

public static final long[] elts_minus_one

The array {-1}.

elts_minus_one_float

public static final double[] elts_minus_one_float

The array {-1.0}.

elts_minus_one_and_plus_one

public static final long[] elts_minus_one_and_plus_one

The array {-1, 1}.

elts_minus_one_and_plus_one_float

public static final double[] elts_minus_one_and_plus_one_float

The array {-1.0, 1.0}.

elts_one

public static final long[] elts_one

The array {1}.

elts_one_float

public static final double[] elts_one_float

The array {1.0}.

Constructor Detail

InvDef

public InvDef(VarInfo v1,
              Class<? extends Invariant> cls)

Create a new InvDef with one variable.

Parameters:

v1 - the variable

cls - the class of the invariant to be defined

InvDef

public InvDef(VarInfo v1,
              Class<? extends Invariant> cls,
              @Nullable Object state)

Create a new InvDef with one variable and the given state

Parameters:

v1 - the variable

cls - the class of the invariant to be defined

state - the state of the invariant

InvDef

public InvDef(VarInfo v1,
              VarInfo v2,
              Class<? extends Invariant> cls)

Method Detail

toString

@SideEffectFree
public String toString(@GuardSatisfied InvDef this)

Overrides:

toString in class Object

check

public boolean check(Invariant inv)

find

public @Nullable Invariant find()

Looks for this invariant (in this ppt). Returns the invariant if it finds it, null otherwise.