class FieldPrinter
extends java.lang.Object
StorePrinter
and SelectPrinter
.Modifier and Type | Field and Description |
---|---|
protected LogicPrinter |
lp |
Constructor and Description |
---|
FieldPrinter(LogicPrinter lp) |
Modifier and Type | Method and Description |
---|---|
protected java.lang.String |
getPrettySyntaxForFieldConstant(Term objectTerm,
Term fieldTerm)
Determine the syntax in which a field constant is printed when associated
with the object represented by
objectTerm Default is the name of
the field. |
protected boolean |
isBuiltinObjectProperty(Term fieldTerm) |
private boolean |
isCanonicField(Term objectTerm,
Term fieldTerm,
JavaInfo javaInfo) |
protected boolean |
isFieldConstant(Term fieldTerm) |
protected static boolean |
isFieldConstant(Term fieldTerm,
HeapLDT heapLDT) |
protected boolean |
isJavaFieldConstant(Term fieldTerm) |
protected static boolean |
isJavaFieldConstant(Term fieldTerm,
HeapLDT heapLDT,
Services services)
Find out whether a
Term represents a field symbol, declared in a
Java class. |
protected boolean |
isStaticFieldConstant(Term objectTerm,
Term fieldTerm) |
protected final LogicPrinter lp
FieldPrinter(LogicPrinter lp)
protected java.lang.String getPrettySyntaxForFieldConstant(Term objectTerm, Term fieldTerm)
objectTerm
Default is the name of
the field. In case the field is hidden by another field, the name of the
field is preceeded by the corresponding class name.
Example default: object.field Example hidden field:
object.(package.class::field)
Remark: This method is declared static because it is also used in method
StorePrinter#printStoreOnFieldConstant(de.uka.ilkd.key.logic.Term, de.uka.ilkd.key.logic.Term, de.uka.ilkd.key.logic.Term, de.uka.ilkd.key.logic.Term, boolean)
protected boolean isFieldConstant(Term fieldTerm)
protected static boolean isJavaFieldConstant(Term fieldTerm, HeapLDT heapLDT, Services services)
Term
represents a field symbol, declared in a
Java class.fieldTerm
- The target field.protected boolean isJavaFieldConstant(Term fieldTerm)
protected boolean isBuiltinObjectProperty(Term fieldTerm)