Package daikon.derive.ternary

Class SequenceScalarArbitrarySubsequence

Object

Derivation

TernaryDerivation

SequenceScalarArbitrarySubsequence

All Implemented Interfaces:

Serializable, Cloneable

public final class SequenceScalarArbitrarySubsequence
extends TernaryDerivation

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field	Description
static boolean	dkconfig_enabled	Boolean.
boolean	left_closed
boolean	right_closed

Fields inherited from class Derivation

debug, dkconfig_disable_derived_variables, missing_array_bounds

Method Summary

Modifier and Type	Method	Description
ValueAndModified	computeValueAndModified(ValueTuple full_vt)	Returns a pair of: the derived value and whether the variable counts as modified.
String	csharp_name(String index)	Returns the csharp name.
VarInfo	endvar()
String	esc_name(String index)	Returns the ESC name.
VarInfo	get_array_var()	Returns the array variable for this slice.
Quantify.Term	get_lower_bound()	Returns the lower bound of the slice.
Quantify.Term	get_upper_bound()	Returns the upper bound of the slice.
boolean	isSameFormula(Derivation other)	Returns true iff other and this represent the same derivation (modulo the variable they are applied to).
protected VarInfo	makeVarInfo()	Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().
VarInfo	seqvar()
VarInfo	startvar()

Methods inherited from class TernaryDerivation

canBeMissing, clone, derivedDepth, getBase, getBases, isDerivedFromNonCanonical, isParam, switchVars

Methods inherited from class Derivation

complexity, getVarInfo, inside_csharp_name, inside_esc_name, inside_jml_name, is_prestate_version, jml_name, makeVarInfo_common_setup, missingOutOfBounds, shift_str, simplify_name

Methods inherited from class Object

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

Field Detail

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff SequenceScalarArbitrarySubsequence derived variables should be generated.

left_closed

public final boolean left_closed

right_closed

public final boolean right_closed

Method Detail

seqvar

public VarInfo seqvar()

startvar

public VarInfo startvar()

endvar

public VarInfo endvar()

computeValueAndModified

public ValueAndModified computeValueAndModified(ValueTuple full_vt)

Description copied from class: Derivation

Returns a pair of: the derived value and whether the variable counts as modified.

Specified by:

computeValueAndModified in class TernaryDerivation

Parameters:

full_vt - the set of values in a program point that will be used to derive the value

Returns:

a pair of: the derived value and whether the variable counts as modified

makeVarInfo

protected VarInfo makeVarInfo()

Description copied from class: Derivation

Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().

Specified by:

makeVarInfo in class Derivation

get_lower_bound

public Quantify.Term get_lower_bound()

Returns the lower bound of the slice.

Overrides:

get_lower_bound in class Derivation

get_upper_bound

public Quantify.Term get_upper_bound()

Returns the upper bound of the slice.

Overrides:

get_upper_bound in class Derivation

get_array_var

public VarInfo get_array_var()

Returns the array variable for this slice.

Overrides:

get_array_var in class Derivation

isSameFormula

@Pure
public boolean isSameFormula(Derivation other)

Description copied from class: Derivation

Returns true iff other and this represent the same derivation (modulo the variable they are applied to). Default implentation will just checks run-time type, but subclasses with state (e.g. SequenceInitial index) should match that, too.

Specified by:

isSameFormula in class Derivation

Parameters:

other - the Derivation to compare to

Returns:

true iff other and this represent the same derivation

csharp_name

@SideEffectFree
public String csharp_name(String index)

Returns the csharp name.

Overrides:

csharp_name in class Derivation

esc_name

@SideEffectFree
public String esc_name(String index)

Returns the ESC name.

Overrides:

esc_name in class Derivation