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

Class CharValue

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

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

public class CharValue
extends NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Character>

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
CharValue(org.sosy_lab.java_smt.api.SolverContext context, char concrete)
CharValue(org.sosy_lab.java_smt.api.SolverContext context, char concrete, org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula formula)
CharValue(org.sosy_lab.java_smt.api.SolverContext context, char concrete, org.sosy_lab.java_smt.api.StringFormula formula)

Method Summary

Modifier and Type	Method	Description
CharValue	asCharValue()
IntValue	asIntValue()
StringValue	asStringValue()
static String	getASCIIchars(int begin, int end)
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 CharValue into a symbolic variable
String	MAKE_SYMBOLIC(long idx)	Turns this IntValue into a symbolic variable
String	MAKE_SYMBOLIC(String namePrefix)	Turns this CharValue into a symbolic variable
org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula	tmp(ArrayList<org.sosy_lab.java_smt.api.StringFormula> chars, org.sosy_lab.java_smt.api.StringFormula s)
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, asDoubleValue, asFloatValue, asLongValue, asNumericalValue, asObjectValue, asShortValue, 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

CharValue

public CharValue(org.sosy_lab.java_smt.api.SolverContext context,
 char concrete)

CharValue

public CharValue(org.sosy_lab.java_smt.api.SolverContext context,
 char concrete,
 org.sosy_lab.java_smt.api.StringFormula formula)

CharValue

public CharValue(org.sosy_lab.java_smt.api.SolverContext context,
 char concrete,
 org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula formula)

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

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 CharValue into a symbolic variable

Overrides:

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

Parameters:

namePrefix -

Returns:

The numerical identifier of this symbolic variable

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC()

Turns this CharValue into a symbolic variable

Overrides:

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

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

Parameters:

idx -

Returns:

The numerical identifier of this symbolic variable

tmp

public org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula tmp(ArrayList<org.sosy_lab.java_smt.api.StringFormula> chars,
 org.sosy_lab.java_smt.api.StringFormula s)

getASCIIchars

public static String getASCIIchars(int begin,
 int end)

asCharValue

public CharValue asCharValue()

Overrides:

asCharValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Character>

asIntValue

public IntValue asIntValue()

Overrides:

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

asStringValue

public StringValue asStringValue()

Overrides:

asStringValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Character>

getConcreteEncoded

public String getConcreteEncoded()

Overrides:

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

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

Returns:

the string representation of the value.