Package de.uzl.its.swat.symbolic.value.reference.lang

Class StringValue

java.lang.Object

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

de.uzl.its.swat.symbolic.value.reference.ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

de.uzl.its.swat.symbolic.value.reference.lang.StringValue

public class StringValue
extends ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

Field Summary

Fields inherited from class de.uzl.its.swat.symbolic.value.reference.ObjectValue

address, ADDRESS_UNKNOWN, className

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

concrete, context, formula, inc, name, symbol

Constructor Summary

Constructors

Constructor	Description
StringValue(org.sosy_lab.java_smt.api.SolverContext context, String concrete, int address)
StringValue(org.sosy_lab.java_smt.api.SolverContext context, String concrete, org.sosy_lab.java_smt.api.StringFormula formula, int address)

Method Summary

Modifier and Type	Method	Description
StringValue	asObjectValue()
StringValue	asStringValue()
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
Object	getConcrete()
String	getConcreteEncoded()
org.sosy_lab.java_smt.api.BooleanFormula	IF_ACMPEQ(ObjectValue o2)	Compares if two references are identical
org.sosy_lab.java_smt.api.BooleanFormula	IF_ACMPNE(ObjectValue o2)	Compares if two references are not identical
Value<?,?>	invokeMethod(String name, org.objectweb.asm.Type[] desc, Value<?,?>[] args)	Handles method invocation for Java's String (Java 16).
String	MAKE_SYMBOLIC()
String	MAKE_SYMBOLIC(long idx)	Turns this IntValue into a symbolic variable
String	MAKE_SYMBOLIC(String namePrefix)
String	toString()	Returns the string representation of the value.

Methods inherited from class de.uzl.its.swat.symbolic.value.reference.ObjectValue

asArrayValue, asFloatValue, asIntValue, asObjectArrayValue, equals, getAddress, getField, getFields, getnFields, IFNONNULL, IFNULL, setAddress, setField, setFields

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

asBooleanValue, asByteValue, asCharValue, asDoubleValue, asLongValue, asNumericalValue, asShortValue, getName, getType, initSymbolic, initSymbolic, reset

Methods inherited from class java.lang.Object

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

Constructor Details

StringValue

public StringValue(org.sosy_lab.java_smt.api.SolverContext context,
 String concrete,
 int address)

StringValue

public StringValue(org.sosy_lab.java_smt.api.SolverContext context,
 String concrete,
 org.sosy_lab.java_smt.api.StringFormula formula,
 int address)

Method Details

IF_ACMPNE

public org.sosy_lab.java_smt.api.BooleanFormula IF_ACMPNE(ObjectValue o2)

Compares if two references are not identical

Overrides:

IF_ACMPNE in class ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

Parameters:

o2 - The other string

Returns:

A BooleanFormula representing the result

IF_ACMPEQ

public org.sosy_lab.java_smt.api.BooleanFormula IF_ACMPEQ(ObjectValue o2)

Compares if two references are identical

Overrides:

IF_ACMPEQ in class ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

Parameters:

o2 - The other string

Returns:

A BooleanFormula representing the result

getConcrete

public Object getConcrete()

Overrides:

getConcrete in class ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC(String namePrefix)

Overrides:

MAKE_SYMBOLIC in class ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

MAKE_SYMBOLIC

public String MAKE_SYMBOLIC()

Overrides:

MAKE_SYMBOLIC in class ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

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.StringFormula,String>

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.StringFormula,String>

Parameters:

upper - If the upper or lower bound should be created

Returns:

The BooleanFormula that represents the bounds check

invokeMethod

public Value<?,?> invokeMethod(String name,
 org.objectweb.asm.Type[] desc,
 Value<?,?>[] args)

Handles method invocation for Java's String (Java 16).

Overrides:

invokeMethod in class ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

Parameters:

name - The name of the method that is called

desc - The Type descriptions for all Arguments

args - The Value's representing the arguments

Returns:

The return Value of the Method, or a PlaceHolder::instance if the Method is not implemented or void should be returned

getConcreteEncoded

public String getConcreteEncoded()

Overrides:

getConcreteEncoded in class Value<org.sosy_lab.java_smt.api.StringFormula,String>

asStringValue

public StringValue asStringValue()

Overrides:

asStringValue in class Value<org.sosy_lab.java_smt.api.StringFormula,String>

asObjectValue

public StringValue asObjectValue()

Overrides:

asObjectValue in class ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

toString

public String toString()

Description copied from class: Value

Returns the string representation of the value. Should be implemented by each inheriting class.

Overrides:

toString in class ObjectValue<org.sosy_lab.java_smt.api.StringFormula,String>

Returns:

the string representation of the value