de.uka.ilkd.key.java

Class SchemaRecoder2KeYConverter

java.lang.Object

de.uka.ilkd.key.java.Recoder2KeYConverter

de.uka.ilkd.key.java.SchemaRecoder2KeYConverter

public class SchemaRecoder2KeYConverter
extends Recoder2KeYConverter

This is an extension of the usual Recoder2KeYConverter that supports schema variables. Some entities have to be treated differently, but most conversions are handled identically (via the superclass).

Author:

MU

Field Summary

Fields

Modifier and Type	Field and Description
private static KeYJavaType	typeSVType the type that is used for schema variables types.

Fields inherited from class de.uka.ilkd.key.java.Recoder2KeYConverter

locClass2finalVar

Constructor Summary

Constructors

Constructor and Description
SchemaRecoder2KeYConverter(SchemaRecoder2KeY rec2key, Services services, NamespaceSet namespaceSet) create a new schema-recoder-to-key converter.

Method Summary

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)

Methods inherited from class de.uka.ilkd.key.java.Recoder2KeYConverter

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

Methods inherited from class java.lang.Object

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

Field Detail

typeSVType

private static KeYJavaType typeSVType

the type that is used for schema variables types.

Constructor Detail

SchemaRecoder2KeYConverter

public SchemaRecoder2KeYConverter(SchemaRecoder2KeY rec2key,
                                  Services services,
                                  NamespaceSet namespaceSet)

create a new schema-recoder-to-key converter. It must be associated with a schema recoder2key.

Parameters:

rec2key - the object to associate to

namespaceSet - namespaces to resolve entity names

services - services to be used

Method Detail

convert

public ProgramTransformer convert(RKeYMetaConstruct mc)

convert a program meta construct creating a new object corresponding to the name. If you add a ProgramTransformer to the system you will most propably have to register it here.

convert

public ProgramTransformer convert(RKeYMetaConstructExpression mc)

translate schema variables to ProgramMetaConstructs. If you have an expression meta construct you will have to add it here.

convert

public ProgramTransformer convert(RKeYMetaConstructType mc)

translate schema variables to ProgramMetaConstructs. If you have a type meta construct you will have to add it here.

convert

public MethodFrame convert(RMethodCallStatement l)

method-call-statements are expanded to method-frames

convert

public LoopScopeBlock convert(LoopScopeBlock l)

convert

public MethodBodyStatement convert(RMethodBodyStatement l)

translate method body statements.

convert

public ContextStatementBlock convert(ContextStatementBlock csb)

translate Context statement blocks

convert

public ExecutionContext convert(ExecutionContext ec)

translate exection contexts

Overrides:

convert in class Recoder2KeYConverter

convert

public SchemaVariable convert(ExpressionSVWrapper svw)

convert

public SchemaVariable convert(StatementSVWrapper svw)

convert

public SchemaVariable convert(LabelSVWrapper svw)

convert

public MergePointStatement convert(MergePointStatement l)

Overrides:

convert in class Recoder2KeYConverter

convert

public SchemaVariable convert(MethodSignatureSVWrapper svw)

convert

public SchemaVariable convert(TypeSVWrapper svw)

convert

public SchemaVariable convert(ExecCtxtSVWrapper svw)

convert

public SchemaVariable convert(CatchSVWrapper svw)

convert

public SchemaVariable convert(ProgramVariableSVWrapper svw)

convert

public ThisReference convert(ThisReference tr)

for some reason the this and super references have to be treated differently here.

Overrides:

convert in class Recoder2KeYConverter

convert

public SuperReference convert(SuperReference sr)

Description copied from class: Recoder2KeYConverter

Convert a super referene. Special handling because the initializing Expressions and the ReferencePrefix accessPath might not be disjunct.

Overrides:

convert in class Recoder2KeYConverter

convert

public LocalVariableDeclaration convert(LocalVariableDeclaration lvd)

local variable declarations have to be treated differently if they have schema vars in them.

Overrides:

convert in class Recoder2KeYConverter

convertVarSpecWithSVType

protected VariableSpecification convertVarSpecWithSVType(VariableSpecification recoderVarspec)

convert

public TypeReference convert(TypeReference tr)

convert a recoder TypeReference to a KeY TypeReference (checks dimension and hands it over)

Overrides:

convert in class Recoder2KeYConverter

convert

public VariableSpecification convert(VariableSpecification recoderVarspec)

convert a recoder VariableSpecification to a KeY VariableSpecification (checks dimension and hands it over and insert in hashmap)

Overrides:

convert in class Recoder2KeYConverter

convert

public Expression convert(FieldReference fr)

Description copied from class: Recoder2KeYConverter

converts a recoder field reference. A ProgramVariable is created replacing the field reference.

Overrides:

convert in class Recoder2KeYConverter

Parameters:

fr - the recoder field reference.

convert

public MethodReference convert(MethodReference mr)

Description copied from class: Recoder2KeYConverter

converts a recoder method reference. A de.uka.ilkd.key.logic.op.ProgramMethod is created replacing the method reference.

Overrides:

convert in class Recoder2KeYConverter

Parameters:

mr - the recoder method reference.

Returns:

the Method the KeY Dependance

convert

public For convert(For f)

converts a For.

Overrides:

convert in class Recoder2KeYConverter

Parameters:

f - the For of recoder

Returns:

the For of KeY