public class SchemaRecoder2KeYConverter extends Recoder2KeYConverter
Recoder2KeYConverter
that supports
schema variables.
Some entities have to be treated differently, but most conversions are
handled identically (via the superclass).Modifier and Type | Field and Description |
---|---|
private static KeYJavaType |
typeSVType
the type that is used for schema variables types.
|
locClass2finalVar
Constructor and Description |
---|
SchemaRecoder2KeYConverter(SchemaRecoder2KeY rec2key,
Services services,
NamespaceSet namespaceSet)
create a new schema-recoder-to-key converter.
|
Modifier and Type | Method and Description |
---|---|
SchemaVariable |
convert(CatchSVWrapper svw) |
ContextStatementBlock |
convert(ContextStatementBlock csb)
translate Context statement blocks
|
SchemaVariable |
convert(ExecCtxtSVWrapper svw) |
ExecutionContext |
convert(ExecutionContext ec)
translate exection contexts
|
SchemaVariable |
convert(ExpressionSVWrapper svw) |
Expression |
convert(FieldReference fr)
converts a recoder field reference.
|
For |
convert(For f)
converts a For.
|
SchemaVariable |
convert(LabelSVWrapper svw) |
LocalVariableDeclaration |
convert(LocalVariableDeclaration lvd)
local variable declarations have to be treated differently if they have
schema vars in them.
|
LoopScopeBlock |
convert(LoopScopeBlock l) |
MergePointStatement |
convert(MergePointStatement l) |
MethodReference |
convert(MethodReference mr)
converts a recoder method reference.
|
SchemaVariable |
convert(MethodSignatureSVWrapper svw) |
SchemaVariable |
convert(ProgramVariableSVWrapper svw) |
ProgramTransformer |
convert(RKeYMetaConstruct mc)
convert a program meta construct creating a new object corresponding to
the name.
|
ProgramTransformer |
convert(RKeYMetaConstructExpression mc)
translate schema variables to ProgramMetaConstructs.
|
ProgramTransformer |
convert(RKeYMetaConstructType mc)
translate schema variables to ProgramMetaConstructs.
|
MethodBodyStatement |
convert(RMethodBodyStatement l)
translate method body statements.
|
MethodFrame |
convert(RMethodCallStatement l)
method-call-statements are expanded to method-frames
|
SchemaVariable |
convert(StatementSVWrapper svw) |
SuperReference |
convert(SuperReference sr)
Convert a super referene.
|
ThisReference |
convert(ThisReference tr)
for some reason the this and super references have to be treated
differently here.
|
TypeReference |
convert(TypeReference tr)
convert a recoder TypeReference to a KeY TypeReference (checks dimension
and hands it over)
|
SchemaVariable |
convert(TypeSVWrapper svw) |
VariableSpecification |
convert(VariableSpecification recoderVarspec)
convert a recoder VariableSpecification to a KeY VariableSpecification
(checks dimension and hands it over and insert in hashmap)
|
protected VariableSpecification |
convertVarSpecWithSVType(VariableSpecification recoderVarspec) |
callConvert, collectChildren, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convert, convertBody, convertGuard, convertLoopInitializers, convertUpdates, getMapping, insertToMap, makeAdmissibleName, process, processCompilationUnit, processDefaultConstructor
private static KeYJavaType typeSVType
public SchemaRecoder2KeYConverter(SchemaRecoder2KeY rec2key, Services services, NamespaceSet namespaceSet)
rec2key
- the object to associate tonamespaceSet
- namespaces to resolve entity namesservices
- services to be usedpublic ProgramTransformer convert(RKeYMetaConstruct mc)
public ProgramTransformer convert(RKeYMetaConstructExpression mc)
public ProgramTransformer convert(RKeYMetaConstructType mc)
public MethodFrame convert(RMethodCallStatement l)
public LoopScopeBlock convert(LoopScopeBlock l)
public MethodBodyStatement convert(RMethodBodyStatement l)
public ContextStatementBlock convert(ContextStatementBlock csb)
public ExecutionContext convert(ExecutionContext ec)
convert
in class Recoder2KeYConverter
public SchemaVariable convert(ExpressionSVWrapper svw)
public SchemaVariable convert(StatementSVWrapper svw)
public SchemaVariable convert(LabelSVWrapper svw)
public MergePointStatement convert(MergePointStatement l)
convert
in class Recoder2KeYConverter
public SchemaVariable convert(MethodSignatureSVWrapper svw)
public SchemaVariable convert(TypeSVWrapper svw)
public SchemaVariable convert(ExecCtxtSVWrapper svw)
public SchemaVariable convert(CatchSVWrapper svw)
public SchemaVariable convert(ProgramVariableSVWrapper svw)
public ThisReference convert(ThisReference tr)
convert
in class Recoder2KeYConverter
public SuperReference convert(SuperReference sr)
Recoder2KeYConverter
convert
in class Recoder2KeYConverter
public LocalVariableDeclaration convert(LocalVariableDeclaration lvd)
convert
in class Recoder2KeYConverter
protected VariableSpecification convertVarSpecWithSVType(VariableSpecification recoderVarspec)
public TypeReference convert(TypeReference tr)
convert
in class Recoder2KeYConverter
public VariableSpecification convert(VariableSpecification recoderVarspec)
convert
in class Recoder2KeYConverter
public Expression convert(FieldReference fr)
Recoder2KeYConverter
convert
in class Recoder2KeYConverter
fr
- the recoder field reference.public MethodReference convert(MethodReference mr)
Recoder2KeYConverter
convert
in class Recoder2KeYConverter
mr
- the recoder method reference.public For convert(For f)
convert
in class Recoder2KeYConverter
f
- the For of recoder