public class Model extends Object
Modifier and Type | Field and Description |
---|---|
private Map<String,String> |
constants
Maps constant names to constant values.
|
private boolean |
empty |
private List<Heap> |
heaps
List of heaps.
|
private List<LocationSet> |
locsets
List of location sets.
|
private Map<String,String> |
reversedConstants
Maps constant values to constant names.
|
private List<Sequence> |
sequences
List of sequences.
|
private ProblemTypeInformation |
types
Type information from the SMT specification.
|
Constructor and Description |
---|
Model() |
Modifier and Type | Method and Description |
---|---|
void |
addAliases()
For all values it adds the names of the constants which have the same values.
|
void |
addConstant(String key,
String value)
Adds a constant to the model.
|
void |
addHeap(Heap e)
Adds a heap to the model.
|
void |
addLocationSet(LocationSet e)
Adds a location set to the model.
|
void |
addSequence(Sequence s)
Adds a sequence set to the model.
|
private void |
fillReversedTable()
Fills the reversed constants table.
|
ObjectVal |
findObject(String ref) |
private String |
formatAny(String val,
SMTSort s)
Transforms a binary value of an any to a human readable form: #sn, where s
is the first letter of the actual sort name and n is the decimal value of
corresponding to the any value after the removal of the three type bits
and the fill up bits.
|
private String |
getAliasedName(String original) |
Map<String,String> |
getConstants() |
List<Heap> |
getHeaps() |
List<LocationSet> |
getLocsets() |
Set<ObjectVal> |
getNecessaryPrestateObjects(String location) |
ObjectVal |
getObject(String name,
Heap heap) |
Set<ObjectVal> |
getReachableObjects(String name,
Heap heap) |
List<Sequence> |
getSequences() |
ProblemTypeInformation |
getTypes() |
boolean |
isEmpty() |
Set<ObjectVal> |
pointsTo(String name,
Heap heap) |
String |
processAnyValue(String val)
Transforms a binary value of an any to a human readable form: #sn, where s
is the first letter of the actual sort name and n is the decimal value of
corresponding to the any value after the removal of the three type bits
and the fill up bits.
|
void |
processArrayValues()
Transforms the values of array fields of objects from binary/hexidecimal to human readable form.
|
void |
processConstantsAndFieldValues()
Transforms the values of constants and object fields from binary/hexadecimal to a human readable from.
|
String |
processConstantValue(String val,
SMTSort s)
Transforms a constant value from binary/hexadecimal form to a human redable form.
|
private void |
processLocSetNames()
Rewrites the values of location sets from binary/hexadecimal to a human readable form.
|
private String |
processObjectID(String objectID)
Transforms an Object id from binary form to #on, where n is a decimal number.
|
void |
processObjectNames()
Rewrite the object names from binary/hexadecimal to a human readable form.
|
private String |
processSeqID(String sequenceID)
Transforms a sequence id from binary form to #sn, where n is a decimal number.
|
void |
processSequenceNames()
Rewrite the sequence names from binary/hexadecimal to a human readable form.
|
void |
processSeqValues()
Transforms values of sequences from binary/hexadecimal to human readable form
|
static String |
removePipes(String s) |
void |
removeUnnecessaryObjects() |
void |
setEmpty(boolean empty) |
void |
setTypes(ProblemTypeInformation types) |
String |
toString() |
private boolean empty
private Map<String,String> constants
private Map<String,String> reversedConstants
private List<LocationSet> locsets
private ProblemTypeInformation types
public boolean isEmpty()
public void setEmpty(boolean empty)
private String processObjectID(String objectID)
objectID
- object id in binary formprivate String processSeqID(String sequenceID)
sequenceID
- sequence id in binary formprivate void processLocSetNames()
public void processObjectNames()
public void processSequenceNames()
public List<LocationSet> getLocsets()
public ProblemTypeInformation getTypes()
public void setTypes(ProblemTypeInformation types)
types
- the types to setprivate void fillReversedTable()
public void addConstant(String key, String value)
key
- the constant namevalue
- the constant valuepublic void addHeap(Heap e)
e
- The heap to be addedpublic void addLocationSet(LocationSet e)
e
- The location set to be added.public void addSequence(Sequence s)
s
- The sequence to be added.private String formatAny(String val, SMTSort s)
val
- original any values
- actual sort of the any sortpublic String processConstantValue(String val, SMTSort s)
val
- binary/hexadecimal value of constants
- sort of constantpublic String processAnyValue(String val)
val
- the original any value in binary/hexadecimalpublic void processArrayValues()
public void processSeqValues()
public void addAliases()
public void removeUnnecessaryObjects()
public void processConstantsAndFieldValues()