Package daikon.derive.binary
Class SequenceStringSubscript
- Object
-
- Derivation
-
- BinaryDerivation
-
- SequenceStringSubscript
-
- All Implemented Interfaces:
Serializable
,Cloneable
public final class SequenceStringSubscript extends BinaryDerivation
- See Also:
- Serialized Form
-
-
Field Summary
Fields Modifier and Type Field Description static Logger
debug
General debug tracer.static boolean
dkconfig_enabled
Boolean.int
index_shift
-
Fields inherited from class BinaryDerivation
base1, base2
-
Fields inherited from class Derivation
dkconfig_disable_derived_variables, missing_array_bounds
-
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description int
complexity()
Adds one to the default complexity if index_shift is not 0.ValueAndModified
computeValueAndModifiedImpl(ValueTuple full_vt)
Actual implementation once mods are handled.String
csharp_name(String index)
Returns the CSHARPCONTRACT name for sequence subscript.String
esc_name(String index)
Returns the ESC name for sequence subscript.boolean
isSameFormula(Derivation other)
Returns true iff other and this represent the same derivation (modulo the variable they are applied to).String
jml_name(String index)
Returns the JML name for sequence subscript.protected VarInfo
makeVarInfo()
Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().VarInfo
sclvar()
VarInfo
seq_enclosing_var()
VarInfo
seqvar()
String
simplify_name()
Return the simplify name for sequence subscript.String
toString()
-
Methods inherited from class BinaryDerivation
canBeMissing, clone, computeValueAndModified, derivedDepth, getBase, getBases, isDerivedFromNonCanonical, isParam, switchVars, var1, var2
-
Methods inherited from class Derivation
get_array_var, get_lower_bound, get_upper_bound, getVarInfo, inside_csharp_name, inside_esc_name, inside_jml_name, is_prestate_version, makeVarInfo_common_setup, missingOutOfBounds, shift_str
-
-
-
-
Field Detail
-
dkconfig_enabled
public static boolean dkconfig_enabled
Boolean. True iff SequenceStringSubscript derived variables should be generated.
-
index_shift
public final int index_shift
-
-
Method Detail
-
seq_enclosing_var
public VarInfo seq_enclosing_var()
-
computeValueAndModifiedImpl
public ValueAndModified computeValueAndModifiedImpl(ValueTuple full_vt)
Description copied from class:BinaryDerivation
Actual implementation once mods are handled.- Specified by:
computeValueAndModifiedImpl
in classBinaryDerivation
-
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 classDerivation
-
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 classDerivation
- Parameters:
other
- the Derivation to compare to- Returns:
- true iff other and this represent the same derivation
-
esc_name
@SideEffectFree public String esc_name(String index)
Returns the ESC name for sequence subscript.- Overrides:
esc_name
in classDerivation
-
jml_name
public String jml_name(String index)
Returns the JML name for sequence subscript.- Overrides:
jml_name
in classDerivation
-
csharp_name
@SideEffectFree public String csharp_name(String index)
Returns the CSHARPCONTRACT name for sequence subscript.- Overrides:
csharp_name
in classDerivation
-
simplify_name
@SideEffectFree public String simplify_name()
Return the simplify name for sequence subscript.- Overrides:
simplify_name
in classDerivation
-
complexity
public int complexity()
Adds one to the default complexity if index_shift is not 0.- Overrides:
complexity
in classDerivation
-
-