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

Class ShortValue

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,Short>

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

public class ShortValue
extends NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Short>

Wrapper for shorts to represent symbolic and concrete information on the symbolic stack

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
ShortValue(org.sosy_lab.java_smt.api.SolverContext context, short concrete)	Creates a new ShortValue that has no prior symbolic information and only contains a specific value
ShortValue(org.sosy_lab.java_smt.api.SolverContext context, short concrete, org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula formula)	Creates a new ShortValue that has prior symbolic information and contains a specific value

Method Summary

Modifier and Type	Method	Description
IntValue	asIntValue()
NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Short>	asNumericalValue()
ShortValue	asShortValue()
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 ShortValue into a symbolic variable
String	MAKE_SYMBOLIC(long idx)	Turns this IntValue into a symbolic variable
String	MAKE_SYMBOLIC(String namePrefix)	Turns this ShortValue 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, asByteValue, asCharValue, asDoubleValue, asFloatValue, asLongValue, asObjectValue, 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

ShortValue

public ShortValue(org.sosy_lab.java_smt.api.SolverContext context,
 short concrete)

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

Parameters:

context - The SolverContext

concrete - The concrete short value

ShortValue

public ShortValue(org.sosy_lab.java_smt.api.SolverContext context,
 short concrete,
 org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula formula)

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

Parameters:

context - The SolverContext

concrete - The concrete short value

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

Method Details

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC(String namePrefix)

Turns this ShortValue into a symbolic variable

Overrides:

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

Parameters:

namePrefix -

Returns:

The numerical identifier of this symbolic variable

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC()

Turns this ShortValue into a symbolic variable

Overrides:

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

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,Short>

Parameters:

idx -

Returns:

The numerical identifier of this symbolic variable

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,Short>

Parameters:

upper - If the upper or lower bound should be created

Returns:

The BooleanFormula that represents the bounds check

asNumericalValue

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

Overrides:

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

asShortValue

public ShortValue asShortValue()

Overrides:

asShortValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Short>

asIntValue

public IntValue asIntValue()

Overrides:

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

getConcreteEncoded

public String getConcreteEncoded()

Overrides:

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

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,Short>

Returns:

the string representation of the value.