de.uka.ilkd.key.speclang.jml.translation

Class JMLTranslator.JMLFieldAccessExpressionTranslationMethod

java.lang.Object

de.uka.ilkd.key.speclang.jml.translation.JMLTranslator.JMLFieldAccessExpressionTranslationMethod

All Implemented Interfaces:

JMLTranslationMethod

Enclosing class:

JMLTranslator

private abstract class JMLTranslator.JMLFieldAccessExpressionTranslationMethod
extends java.lang.Object
implements JMLTranslationMethod

Abstract super-class for translation methods which enumerate fields such as \reach.

Author:

bruns

Constructor Summary

Constructors

Modifier	Constructor and Description
private	JMLFieldAccessExpressionTranslationMethod()

Method Summary

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.

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.speclang.jml.translation.JMLTranslationMethod

translate

Constructor Detail

JMLFieldAccessExpressionTranslationMethod

private JMLFieldAccessExpressionTranslationMethod()

Method Detail

getFields

protected Term getFields(SLTranslationExceptionManager excManager,
                         Term t,
                         Services services)
                  throws SLTranslationException

Creates an "all-objects" term from a store-ref term.

Parameters:

t - store-ref term, needs to be a union of singletons

services -

Returns:

allObjects term (see LocSetADT)

Throws:

SLTranslationException - in case t is not a store-ref term cosisting of unions of singletons