Package de.uzl.its.swat.symbolic.value.primitive.numeric.integral

Class ByteValue

java.lang.Object

de.uzl.its.swat.symbolic.value.Value<T,K>

de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

de.uzl.its.swat.symbolic.value.primitive.numeric.integral.ByteValue

public class ByteValue
extends NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

Wrapper to represent byte values on the symbolic stack. Can contain concrete and symbolic information.

Field Summary

Fields inherited from class de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue

imgr

Fields inherited from class de.uzl.its.swat.symbolic.value.Value

concrete, context, formula, inc, name, symbol

Constructor Summary

Constructors

Constructor	Description
ByteValue(org.sosy_lab.java_smt.api.SolverContext context, byte concrete)	Creates a new ByteValue that has no prior symbolic information and only contains a specific value
ByteValue(org.sosy_lab.java_smt.api.SolverContext context, byte concrete, org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula formula)	Creates a new ByteValue that has prior symbolic information and contains a specific value

Method Summary

Modifier and Type	Method	Description
ByteValue	asByteValue()
IntValue	asIntValue()
NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>	asNumericalValue()
org.sosy_lab.java_smt.api.BooleanFormula	getBounds(boolean upper)	Creates a formula that asserts that this symbolic value is withing the bounds of this type
String	getConcreteEncoded()
String	MAKE_SYMBOLIC()	Turns this ByteValue into a symbolic variable
String	MAKE_SYMBOLIC(long idx)	Turns this IntValue into a symbolic variable
String	MAKE_SYMBOLIC(String namePrefix)	Turns this ByteValue into a symbolic variable
String	toString()	Returns the string representation of the value used to visualize the stack.

Methods inherited from class de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue

genericToString, wrapByte, wrapCharacter, wrapInteger, wrapLong, wrapShort

Methods inherited from class de.uzl.its.swat.symbolic.value.Value

asBooleanValue, asCharValue, asDoubleValue, asFloatValue, asLongValue, asObjectValue, asShortValue, asStringValue, getConcrete, getName, getType, initSymbolic, initSymbolic, reset

Methods inherited from class java.lang.Object

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

Constructor Details

ByteValue

public ByteValue(org.sosy_lab.java_smt.api.SolverContext context,
 byte concrete)

Creates a new ByteValue that has no prior symbolic information and only contains a specific value

Parameters:

context - The SolverContext

concrete - The concrete byte value

ByteValue

public ByteValue(org.sosy_lab.java_smt.api.SolverContext context,
 byte concrete,
 org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula formula)

Creates a new ByteValue that has prior symbolic information and contains a specific value

Parameters:

context - The SolverContext

concrete - The concrete byte value

formula - The symbolic formula representing prior symbolic information about this byte

Method Details

getBounds

public org.sosy_lab.java_smt.api.BooleanFormula getBounds(boolean upper)

Creates a formula that asserts that this symbolic value is withing the bounds of this type

Overrides:

getBounds in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

Parameters:

upper - If the upper or lower bound should be created

Returns:

The BooleanFormula that represents the bounds check

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC(String namePrefix)

Turns this ByteValue into a symbolic variable

Overrides:

MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

Parameters:

namePrefix -

Returns:

The numerical identifier of this symbolic variable

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC(long idx)

Turns this IntValue into a symbolic variable

Overrides:

MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

Parameters:

idx -

Returns:

The numerical identifier of this symbolic variable

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC()

Turns this ByteValue into a symbolic variable

Overrides:

MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

Returns:

The numerical identifier of this symbolic variable

asNumericalValue

public NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte> asNumericalValue()

Overrides:

asNumericalValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

asIntValue

public IntValue asIntValue()

Overrides:

asIntValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

asByteValue

public ByteValue asByteValue()

Overrides:

asByteValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

getConcreteEncoded

public String getConcreteEncoded()

Overrides:

getConcreteEncoded in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

toString

public String toString()

Returns the string representation of the value used to visualize the stack. The representation is not complete.

Overrides:

toString in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Byte>

Returns:

the string representation of the value.