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

Class JMLBuiltInPropertyResolver

java.lang.Object

de.uka.ilkd.key.speclang.translation.SLExpressionResolver

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

public final class JMLBuiltInPropertyResolver
extends SLExpressionResolver

Resolver for built-in JML operators. Currently only handles array length.

Field Summary

Fields

Modifier and Type	Field and Description
private SeqLDT	seqLDT

Fields inherited from class de.uka.ilkd.key.speclang.translation.SLExpressionResolver

javaInfo, manager, services, specInClass

Constructor Summary

Constructors

Constructor and Description
JMLBuiltInPropertyResolver(JavaInfo javaInfo, SLResolverManager manager, KeYJavaType specInClass)

Method Summary

Modifier and Type	Method and Description
protected boolean	canHandleReceiver(SLExpression receiver)
protected SLExpression	doResolving(SLExpression receiver, java.lang.String name, SLParameters parameters) Resolves property calls on explicit receivers.

Methods inherited from class de.uka.ilkd.key.speclang.translation.SLExpressionResolver

isVisible, resolve

Methods inherited from class java.lang.Object

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

Field Detail

seqLDT

private final SeqLDT seqLDT

Constructor Detail

JMLBuiltInPropertyResolver

public JMLBuiltInPropertyResolver(JavaInfo javaInfo,
                                  SLResolverManager manager,
                                  KeYJavaType specInClass)

Method Detail

canHandleReceiver

protected boolean canHandleReceiver(SLExpression receiver)

Specified by:

canHandleReceiver in class SLExpressionResolver

doResolving

protected SLExpression doResolving(SLExpression receiver,
                                   java.lang.String name,
                                   SLParameters parameters)
                            throws SLTranslationException

Description copied from class: SLExpressionResolver

Resolves property calls on explicit receivers.

Specified by:

doResolving in class SLExpressionResolver

Parameters:

receiver - receiver (may *not* be null)

name - name of the property

parameters - the actual parameters, or null if not applicable

Returns:

a suitable term or collection if successful, null otherwise

Throws:

SLTranslationException