private abstract class JMLTranslator.JMLFieldAccessExpressionTranslationMethod extends java.lang.Object implements JMLTranslationMethod
\reach
.Modifier | Constructor and Description |
---|---|
private |
JMLFieldAccessExpressionTranslationMethod() |
Modifier and Type | Method and Description |
---|---|
protected Term |
getFields(SLTranslationExceptionManager excManager,
Term t,
Services services)
Creates an "all-objects" term from a store-ref term.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
translate
private JMLFieldAccessExpressionTranslationMethod()
protected Term getFields(SLTranslationExceptionManager excManager, Term t, Services services) throws SLTranslationException
t
- store-ref term, needs to be a union of singletonsservices
- LocSetADT
)SLTranslationException
- in case t
is not a store-ref term cosisting of unions of singletons