de.uka.ilkd.key.java.recoderext

Class JMLTransformer

java.lang.Object

recoder.kit.Transformation

recoder.kit.TwoPassTransformation

de.uka.ilkd.key.java.recoderext.RecoderModelTransformer

de.uka.ilkd.key.java.recoderext.JMLTransformer

public final class JMLTransformer
extends RecoderModelTransformer

RecodeR transformation that parses JML comments, and attaches code-like specifications (ghost fields, set statements, model methods) directly to the RecodeR AST. Note that internally, this class is highly similar to the class speclang.jml.SpecExtractor; if you change one of these classes, you probably need to change the other as well.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	JMLTransformer.TypeDeclarationCollector

Nested classes/interfaces inherited from class de.uka.ilkd.key.java.recoderext.RecoderModelTransformer

RecoderModelTransformer.FinalOuterVarsCollector, RecoderModelTransformer.TransformerCache

Field Summary

Fields

Modifier and Type	Field and Description
private static ImmutableList<java.lang.String>	javaMods
private static java.lang.String	JML JML markers left and right.
private static java.lang.String	JMR
private java.util.HashMap<TypeDeclaration,java.util.List<? extends Constructor>>	typeDeclaration2Constructores
private java.util.HashMap<TypeDeclaration,java.util.List<Method>>	typeDeclaration2Methods
private static ImmutableSet<PositionedString>	warnings

Fields inherited from class de.uka.ilkd.key.java.recoderext.RecoderModelTransformer

cache, services

Fields inherited from class recoder.kit.Transformation

EQUIVALENCE, IDENTITY, NO_PROBLEM

Constructor Summary

Constructors

Constructor and Description
JMLTransformer(CrossReferenceServiceConfiguration services, RecoderModelTransformer.TransformerCache cache) Creates a transformation that adds JML specific elements, for example ghost fields and model method declarations.

Method Summary

Modifier and Type	Method and Description
ProblemReport	analyze()
private java.lang.String	concatenate(Comment[] comments) Concatenates the passed comments in a position-preserving way.
private ProgramElement[]	getChildren(ProgramElement pe) Returns the children of the passed program element.
private Comment[]	getCommentsAndSetParent(ProgramElement pe)
private java.lang.String	getJMLModString(ImmutableList<java.lang.String> mods) Puts the JML modifiers from the passed list into a string enclosed in JML markers.
static ImmutableSet<PositionedString>	getWarningsOfLastInstance()
void	makeExplicit() invokes model transformation for each top level type declaration in any compilation unit.
protected void	makeExplicit(TypeDeclaration td) The method is called for each type declaration of the compilation unit and initiates the syntactical transformation.
private PositionedString	prependJavaMods(ImmutableList<java.lang.String> mods, PositionedString ps) Prepends the Java (i.e., non-JML) modifiers from the passed list to the passed PositionedString.
private void	transformClasslevelComments(TypeDeclaration td, java.lang.String fileName)
private void	transformFieldDecl(TextualJMLFieldDecl decl, Comment[] originalComments)
private void	transformMergePointDecl(TextualJMLMergePointDecl stat, Comment[] originalComments)
private void	transformMethodDecl(TextualJMLMethodDecl decl, Comment[] originalComments)
private void	transformMethodlevelComments(MethodDeclaration md, java.lang.String fileName)
private void	transformMethodlevelCommentsHelper(ProgramElement pe, java.lang.String fileName)
private void	transformSetStatement(TextualJMLSetStatement stat, Comment[] originalComments)
private void	updatePositionInformation(ProgramElement pe, Position pos) Recursively adds the passed position to the starting positions of the passed program element and its children.

Methods inherited from class de.uka.ilkd.key.java.recoderext.RecoderModelTransformer

assign, attach, attribute, classDeclarations, containingClass, containingMethod, declare, declare, getAllSupertypes, getDefaultValue, getId, getLocalClass2FinalVar, getUnits, isVisible, transform

Methods inherited from class recoder.kit.TwoPassTransformation

execute

Methods inherited from class recoder.kit.Transformation

attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsBody, attachAsCondition, attachAsGuard, attachAsInitializer, attachAsLabel, attachAsMessage, attachAsPrefix, attachAsPrefix, attachAsPrefix, attachAsPrefix, attachAsUpdate, detach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsBody, doAttachAsCondition, doAttachAsGuard, doAttachAsInitializer, doAttachAsLabel, doAttachAsMessage, doAttachAsPrefix, doAttachAsPrefix, doAttachAsPrefix, doAttachAsPrefix, doAttachAsUpdate, doDetach, doReplace, getChangeHistory, getCrossReferenceSourceInfo, getNameInfo, getProblemReport, getProgramFactory, getServiceConfiguration, getSourceFileRepository, getSourceInfo, replace, rollback, setProblemReport, setServiceConfiguration, toString

Methods inherited from class java.lang.Object

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

Field Detail

JML

private static final java.lang.String JML

JML markers left and right.

See Also:

Constant Field Values

JMR

private static final java.lang.String JMR

See Also:

Constant Field Values

javaMods

private static final ImmutableList<java.lang.String> javaMods

warnings

private static ImmutableSet<PositionedString> warnings

typeDeclaration2Methods

private final java.util.HashMap<TypeDeclaration,java.util.List<Method>> typeDeclaration2Methods

typeDeclaration2Constructores

private final java.util.HashMap<TypeDeclaration,java.util.List<? extends Constructor>> typeDeclaration2Constructores

Constructor Detail

JMLTransformer

public JMLTransformer(CrossReferenceServiceConfiguration services,
                      RecoderModelTransformer.TransformerCache cache)

Creates a transformation that adds JML specific elements, for example ghost fields and model method declarations.

Parameters:

services - the CrossReferenceServiceConfiguration to access model information

cache - a cache object that stores information which is needed by and common to many transformations. it includes the compilation units, the declared classes, and information for local classes.

Method Detail

concatenate

private java.lang.String concatenate(Comment[] comments)

Concatenates the passed comments in a position-preserving way. (see also JMLSpecExtractor::concatenate(), which does the same thing for KeY ASTs)

prependJavaMods

private PositionedString prependJavaMods(ImmutableList<java.lang.String> mods,
                                         PositionedString ps)

Prepends the Java (i.e., non-JML) modifiers from the passed list to the passed PositionedString. Inserts whitespace in place of the JML modifiers (in order to preserve position information).

getJMLModString

private java.lang.String getJMLModString(ImmutableList<java.lang.String> mods)

Puts the JML modifiers from the passed list into a string enclosed in JML markers.

updatePositionInformation

private void updatePositionInformation(ProgramElement pe,
                                       Position pos)

Recursively adds the passed position to the starting positions of the passed program element and its children.

getChildren

private ProgramElement[] getChildren(ProgramElement pe)

Returns the children of the passed program element.

getCommentsAndSetParent

private Comment[] getCommentsAndSetParent(ProgramElement pe)

transformFieldDecl

private void transformFieldDecl(TextualJMLFieldDecl decl,
                                Comment[] originalComments)
                         throws SLTranslationException

Throws:

SLTranslationException

transformMethodDecl

private void transformMethodDecl(TextualJMLMethodDecl decl,
                                 Comment[] originalComments)
                          throws SLTranslationException

Throws:

SLTranslationException

transformSetStatement

private void transformSetStatement(TextualJMLSetStatement stat,
                                   Comment[] originalComments)
                            throws SLTranslationException

Throws:

SLTranslationException

transformMergePointDecl

private void transformMergePointDecl(TextualJMLMergePointDecl stat,
                                     Comment[] originalComments)
                              throws SLTranslationException

Throws:

SLTranslationException

transformClasslevelComments

private void transformClasslevelComments(TypeDeclaration td,
                                         java.lang.String fileName)
                                  throws SLTranslationException

Throws:

SLTranslationException

transformMethodlevelCommentsHelper

private void transformMethodlevelCommentsHelper(ProgramElement pe,
                                                java.lang.String fileName)
                                         throws SLTranslationException

Throws:

SLTranslationException

transformMethodlevelComments

private void transformMethodlevelComments(MethodDeclaration md,
                                          java.lang.String fileName)
                                   throws SLTranslationException

Throws:

SLTranslationException

makeExplicit

protected void makeExplicit(TypeDeclaration td)

Description copied from class: RecoderModelTransformer

The method is called for each type declaration of the compilation unit and initiates the syntactical transformation. If you want to descend in inner classes you have to implement the recursion by yourself.

Specified by:

makeExplicit in class RecoderModelTransformer

analyze

public ProblemReport analyze()

Overrides:

analyze in class TwoPassTransformation

makeExplicit

public void makeExplicit()

Description copied from class: RecoderModelTransformer

invokes model transformation for each top level type declaration in any compilation unit. Not for inner classes.

Overrides:

makeExplicit in class RecoderModelTransformer

getWarningsOfLastInstance

public static ImmutableSet<PositionedString> getWarningsOfLastInstance()