de.uka.ilkd.key.java

Class KeYRecoderMapping

java.lang.Object

de.uka.ilkd.key.java.KeYRecoderMapping

public class KeYRecoderMapping
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.HashMap<java.lang.Object,java.lang.Object>	map maps a recoder programelement (or something similar, e.g.
private boolean	parsedSpecial have special classes been parsed in
private java.util.HashMap<java.lang.Object,java.lang.Object>	revMap maps a KeY programelement to the Recoder-equivalent
private KeYJavaType	superArrayType a pseudo super class for all arrays used to declare length

Constructor Summary

Constructors

Constructor and Description
KeYRecoderMapping()
KeYRecoderMapping(java.util.HashMap<java.lang.Object,java.lang.Object> map, java.util.HashMap<java.lang.Object,java.lang.Object> revMap, KeYJavaType superArrayType, boolean parsedSpecial) creates a KeYRecoderMapping object.

Method Summary

Modifier and Type	Method and Description
KeYRecoderMapping	copy()
java.util.Set<java.lang.Object>	elemsKeY()
java.util.Set<java.lang.Object>	elemsRec()
KeYJavaType	getSuperArrayType()
boolean	mapped(java.lang.Object rec)
boolean	parsedSpecial() As long as we do not support lemmata we need the source code of some 'java.lang' classes.
void	parsedSpecial(boolean b) As long as we do not support lemmata we need the source code of some 'java.lang' classes.
void	put(java.lang.Object rec, java.lang.Object key)
void	setSuperArrayType(KeYJavaType superArrayType)
int	size()
ModelElement	toKeY(ModelElement pe) returns a matching ModelElement (KeY) to a given recoder.ModelElement
ProgramElement	toKeY(ProgramElement pe) returns a matching ProgramElement (KeY) to a given ProgramElement (Recoder)
ModelElement	toRecoder(ModelElement pe) returns the Recoder-equivalent to a given ModelElement (KeY).
ProgramElement	toRecoder(ProgramElement pe) returns the Recoder-equivalent to a given ProgramElement (KeY).

Methods inherited from class java.lang.Object

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

Field Detail

parsedSpecial

private boolean parsedSpecial

have special classes been parsed in

map

private java.util.HashMap<java.lang.Object,java.lang.Object> map

maps a recoder programelement (or something similar, e.g. Type) to the KeY-equivalent

revMap

private java.util.HashMap<java.lang.Object,java.lang.Object> revMap

maps a KeY programelement to the Recoder-equivalent

superArrayType

private KeYJavaType superArrayType

a pseudo super class for all arrays used to declare length

Constructor Detail

KeYRecoderMapping

public KeYRecoderMapping()

KeYRecoderMapping

KeYRecoderMapping(java.util.HashMap<java.lang.Object,java.lang.Object> map,
                  java.util.HashMap<java.lang.Object,java.lang.Object> revMap,
                  KeYJavaType superArrayType,
                  boolean parsedSpecial)

creates a KeYRecoderMapping object. Used for cloning and testing.

Parameters:

map - a HashMap mapping ProgramElements in Recoder to ProgramElements in KeY

revMap - the reverse map (KeY->Recoder)

parsedSpecial - boolean indicating if the special classes have been parsed in

Method Detail

toKeY

public ProgramElement toKeY(ProgramElement pe)

returns a matching ProgramElement (KeY) to a given ProgramElement (Recoder)

Parameters:

pe - a recoder.java.ProgramElement

toKeY

public ModelElement toKeY(ModelElement pe)

returns a matching ModelElement (KeY) to a given recoder.ModelElement

Parameters:

pe - a recoder.ModelElement

toRecoder

public ProgramElement toRecoder(ProgramElement pe)

returns the Recoder-equivalent to a given ProgramElement (KeY). If there's no RecodeR equivalent to program element pe, an assertion failure "Program Element not known" is emitted.

Parameters:

pe - a JavaProgramElement

toRecoder

public ModelElement toRecoder(ModelElement pe)

returns the Recoder-equivalent to a given ModelElement (KeY). If there's no Recoder-equivalent to the ModelElement pe a debug message "Model Element not known" is printed.

Parameters:

pe - a ModelElement

put

public void put(java.lang.Object rec,
                java.lang.Object key)

mapped

public boolean mapped(java.lang.Object rec)

elemsKeY

public java.util.Set<java.lang.Object> elemsKeY()

elemsRec

public java.util.Set<java.lang.Object> elemsRec()

setSuperArrayType

public void setSuperArrayType(KeYJavaType superArrayType)

getSuperArrayType

public KeYJavaType getSuperArrayType()

copy

public KeYRecoderMapping copy()

parsedSpecial

public boolean parsedSpecial()

As long as we do not support lemmata we need the source code of some 'java.lang' classes. These are parsed in using method parseSpecial of Recoder2KeY. To avoid multiple readings this method indicates whether the special have been parsed in or not.

Returns:

true if special classes have been parsed in

size

public int size()

parsedSpecial

public void parsedSpecial(boolean b)

As long as we do not support lemmata we need the source code of some 'java.lang' classes. These are parsed in using method parseSpecial of Recoder2KeY. To avoid multiple readings this method sets a flag whether the special have been parsed in or not

Parameters:

b - boolean indicating if the special classes have been parsed in