public class JavaIntegerSemanticsHelper
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private SLTranslationExceptionManager |
excManager |
private IntegerLDT |
integerLDT |
private TermBuilder |
tb |
private TypeConverter |
tc |
Constructor and Description |
---|
JavaIntegerSemanticsHelper(Services services,
SLTranslationExceptionManager excManager) |
private final TermBuilder tb
private final SLTranslationExceptionManager excManager
private final TypeConverter tc
private final IntegerLDT integerLDT
public JavaIntegerSemanticsHelper(Services services, SLTranslationExceptionManager excManager)
private void raiseError(java.lang.String message) throws SLTranslationException
SLTranslationException
private void raiseError(java.lang.String message, java.lang.Exception e) throws SLTranslationException
SLTranslationException
private KeYJavaType getPromotedType(SLExpression a, SLExpression b)
private KeYJavaType getPromotedType(SLExpression a)
private boolean isBigint(KeYJavaType resultType)
private boolean isLong(KeYJavaType resultType)
public boolean isIntegerTerm(SLExpression a) throws SLTranslationException
SLTranslationException
public SLExpression buildPromotedOrExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildPromotedAndExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildPromotedXorExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildPromotedNegExpression(SLExpression a) throws SLTranslationException
SLTranslationException
public SLExpression buildAddExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildSubExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildMulExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildDivExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildModExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildRightShiftExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildLeftShiftExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildUnsignedRightShiftExpression(SLExpression a, SLExpression b) throws SLTranslationException
SLTranslationException
public SLExpression buildUnaryMinusExpression(SLExpression a) throws SLTranslationException
SLTranslationException
public SLExpression buildPromotedUnaryPlusExpression(SLExpression a) throws SLTranslationException
SLTranslationException
public SLExpression buildCastExpression(KeYJavaType resultType, SLExpression a) throws SLTranslationException
SLTranslationException