Package | Description |
---|---|
de.uka.ilkd.key.java.abstraction |
This package contains the meta model abstractions as used by the
semantical services.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.expression.literal |
This package contains representations for the various Java literal types.
|
de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
Modifier and Type | Method and Description |
---|---|
Literal |
PrimitiveType.getDefaultValue()
returns the default value of the given type
according to JLS ???4.5.5
ATTENTION: usually for byte and short this should be (byte) 0
(rsp.
|
Literal |
KeYJavaType.getDefaultValue()
Returns the default value of the given type
according to JLS Sect.
|
Literal |
NullType.getDefaultValue()
returns the default value of the given type
according to JLS Sect.
|
Literal |
Type.getDefaultValue()
returns the default value of the given type
according to JLS Sect.
|
Modifier and Type | Method and Description |
---|---|
Literal |
ArrayDeclaration.getDefaultValue()
returns the default value of the given type
according to JLS Sect.
|
Literal |
TypeDeclaration.getDefaultValue()
returns the default value of the given type
according to JLS 4.5.5
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractIntegerLiteral
This class is a superclass for integer literals (Int, Long, Char).
|
class |
BooleanLiteral
Boolean literal.
|
class |
CharLiteral
Char literal.
|
class |
DoubleLiteral
Double literal.
|
class |
EmptyMapLiteral |
class |
EmptySeqLiteral |
class |
EmptySetLiteral |
class |
FloatLiteral
Float literal.
|
class |
FreeLiteral |
class |
IntLiteral
Int literal.
|
class |
LongLiteral
Long literal.
|
class |
NullLiteral
Null literal.
|
class |
RealLiteral
JML \real literal.
|
class |
StringLiteral |
Modifier and Type | Method and Description |
---|---|
Term |
DoubleLDT.translateLiteral(Literal lit,
Services services) |
Term |
CharListLDT.translateLiteral(Literal lit,
Services services) |
Term |
FreeLDT.translateLiteral(Literal lit,
Services services) |
Term |
MapLDT.translateLiteral(Literal lit,
Services services) |
Term |
RealLDT.translateLiteral(Literal lit,
Services services) |
Term |
BooleanLDT.translateLiteral(Literal lit,
Services services) |
Term |
PermissionLDT.translateLiteral(Literal lit,
Services services) |
Term |
LocSetLDT.translateLiteral(Literal lit,
Services services) |
Term |
IntegerLDT.translateLiteral(Literal lit,
Services services) |
Term |
HeapLDT.translateLiteral(Literal lit,
Services services) |
Term |
FloatLDT.translateLiteral(Literal lit,
Services services) |
Term |
SeqLDT.translateLiteral(Literal lit,
Services services) |
abstract Term |
LDT.translateLiteral(Literal lit,
Services services)
translates a given literal to its logic counterpart
|
Modifier and Type | Method and Description |
---|---|
Literal |
ProgramConstant.getCompileTimeConstant() |
Constructor and Description |
---|
ProgramConstant(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
Literal compileTimeConstant) |
Copyright © 2003-2019 The KeY-Project.