de.uka.ilkd.key.speclang.translation

Class JavaIntegerSemanticsHelper

java.lang.Object

de.uka.ilkd.key.speclang.translation.JavaIntegerSemanticsHelper

public class JavaIntegerSemanticsHelper
extends java.lang.Object

Helper class for sl-parsers dealing with Java's type promotion for integers.

Field Summary

Fields

Modifier and Type	Field and Description
private SLTranslationExceptionManager	excManager
private IntegerLDT	integerLDT
private TermBuilder	tb
private TypeConverter	tc

Constructor Summary

Constructors

Constructor and Description
JavaIntegerSemanticsHelper(Services services, SLTranslationExceptionManager excManager)

Method Summary

Modifier and Type	Method and Description
SLExpression	buildAddExpression(SLExpression a, SLExpression b)
SLExpression	buildCastExpression(KeYJavaType resultType, SLExpression a)
SLExpression	buildDivExpression(SLExpression a, SLExpression b)
SLExpression	buildLeftShiftExpression(SLExpression a, SLExpression b)
SLExpression	buildModExpression(SLExpression a, SLExpression b)
SLExpression	buildMulExpression(SLExpression a, SLExpression b)
SLExpression	buildPromotedAndExpression(SLExpression a, SLExpression b)
SLExpression	buildPromotedNegExpression(SLExpression a)
SLExpression	buildPromotedOrExpression(SLExpression a, SLExpression b)
SLExpression	buildPromotedUnaryPlusExpression(SLExpression a)
SLExpression	buildPromotedXorExpression(SLExpression a, SLExpression b)
SLExpression	buildRightShiftExpression(SLExpression a, SLExpression b)
SLExpression	buildSubExpression(SLExpression a, SLExpression b)
SLExpression	buildUnaryMinusExpression(SLExpression a)
SLExpression	buildUnsignedRightShiftExpression(SLExpression a, SLExpression b)
private KeYJavaType	getPromotedType(SLExpression a)
private KeYJavaType	getPromotedType(SLExpression a, SLExpression b)
private boolean	isBigint(KeYJavaType resultType)
boolean	isIntegerTerm(SLExpression a)
private boolean	isLong(KeYJavaType resultType)
private void	raiseError(java.lang.String message)
private void	raiseError(java.lang.String message, java.lang.Exception e)

Methods inherited from class java.lang.Object

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

Field Detail

tb

private final TermBuilder tb

excManager

private final SLTranslationExceptionManager excManager

tc

private final TypeConverter tc

integerLDT

private final IntegerLDT integerLDT

Constructor Detail

JavaIntegerSemanticsHelper

public JavaIntegerSemanticsHelper(Services services,
                                  SLTranslationExceptionManager excManager)

Method Detail

raiseError

private void raiseError(java.lang.String message)
                 throws SLTranslationException

Throws:

SLTranslationException

raiseError

private void raiseError(java.lang.String message,
                        java.lang.Exception e)
                 throws SLTranslationException

Throws:

SLTranslationException

getPromotedType

private KeYJavaType getPromotedType(SLExpression a,
                                    SLExpression b)

getPromotedType

private KeYJavaType getPromotedType(SLExpression a)

isBigint

private boolean isBigint(KeYJavaType resultType)

isLong

private boolean isLong(KeYJavaType resultType)

isIntegerTerm

public boolean isIntegerTerm(SLExpression a)
                      throws SLTranslationException

Throws:

SLTranslationException

buildPromotedOrExpression

public SLExpression buildPromotedOrExpression(SLExpression a,
                                              SLExpression b)
                                       throws SLTranslationException

Throws:

SLTranslationException

buildPromotedAndExpression

public SLExpression buildPromotedAndExpression(SLExpression a,
                                               SLExpression b)
                                        throws SLTranslationException

Throws:

SLTranslationException

buildPromotedXorExpression

public SLExpression buildPromotedXorExpression(SLExpression a,
                                               SLExpression b)
                                        throws SLTranslationException

Throws:

SLTranslationException

buildPromotedNegExpression

public SLExpression buildPromotedNegExpression(SLExpression a)
                                        throws SLTranslationException

Throws:

SLTranslationException

buildAddExpression

public SLExpression buildAddExpression(SLExpression a,
                                       SLExpression b)
                                throws SLTranslationException

Throws:

SLTranslationException

buildSubExpression

public SLExpression buildSubExpression(SLExpression a,
                                       SLExpression b)
                                throws SLTranslationException

Throws:

SLTranslationException

buildMulExpression

public SLExpression buildMulExpression(SLExpression a,
                                       SLExpression b)
                                throws SLTranslationException

Throws:

SLTranslationException

buildDivExpression

public SLExpression buildDivExpression(SLExpression a,
                                       SLExpression b)
                                throws SLTranslationException

Throws:

SLTranslationException

buildModExpression

public SLExpression buildModExpression(SLExpression a,
                                       SLExpression b)
                                throws SLTranslationException

Throws:

SLTranslationException

buildRightShiftExpression

public SLExpression buildRightShiftExpression(SLExpression a,
                                              SLExpression b)
                                       throws SLTranslationException

Throws:

SLTranslationException

buildLeftShiftExpression

public SLExpression buildLeftShiftExpression(SLExpression a,
                                             SLExpression b)
                                      throws SLTranslationException

Throws:

SLTranslationException

buildUnsignedRightShiftExpression

public SLExpression buildUnsignedRightShiftExpression(SLExpression a,
                                                      SLExpression b)
                                               throws SLTranslationException

Throws:

SLTranslationException

buildUnaryMinusExpression

public SLExpression buildUnaryMinusExpression(SLExpression a)
                                       throws SLTranslationException

Throws:

SLTranslationException

buildPromotedUnaryPlusExpression

public SLExpression buildPromotedUnaryPlusExpression(SLExpression a)
                                              throws SLTranslationException

Throws:

SLTranslationException

buildCastExpression

public SLExpression buildCastExpression(KeYJavaType resultType,
                                        SLExpression a)
                                 throws SLTranslationException

Throws:

SLTranslationException