public final class JMLTransformer extends RecoderModelTransformer
Modifier and Type | Class and Description |
---|---|
private static class |
JMLTransformer.TypeDeclarationCollector |
RecoderModelTransformer.FinalOuterVarsCollector, RecoderModelTransformer.TransformerCache
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 |
cache, services
EQUIVALENCE, IDENTITY, NO_PROBLEM
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.
|
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.
|
assign, attach, attribute, classDeclarations, containingClass, containingMethod, declare, declare, getAllSupertypes, getDefaultValue, getId, getLocalClass2FinalVar, getUnits, isVisible, transform
execute
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
private static final java.lang.String JML
private static final java.lang.String JMR
private static final ImmutableList<java.lang.String> javaMods
private static ImmutableSet<PositionedString> warnings
private final java.util.HashMap<TypeDeclaration,java.util.List<Method>> typeDeclaration2Methods
private final java.util.HashMap<TypeDeclaration,java.util.List<? extends Constructor>> typeDeclaration2Constructores
public JMLTransformer(CrossReferenceServiceConfiguration services, RecoderModelTransformer.TransformerCache cache)
services
- the CrossReferenceServiceConfiguration to access model
informationcache
- 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.private java.lang.String concatenate(Comment[] comments)
private PositionedString prependJavaMods(ImmutableList<java.lang.String> mods, PositionedString ps)
private java.lang.String getJMLModString(ImmutableList<java.lang.String> mods)
private void updatePositionInformation(ProgramElement pe, Position pos)
private ProgramElement[] getChildren(ProgramElement pe)
private Comment[] getCommentsAndSetParent(ProgramElement pe)
private void transformFieldDecl(TextualJMLFieldDecl decl, Comment[] originalComments) throws SLTranslationException
SLTranslationException
private void transformMethodDecl(TextualJMLMethodDecl decl, Comment[] originalComments) throws SLTranslationException
SLTranslationException
private void transformSetStatement(TextualJMLSetStatement stat, Comment[] originalComments) throws SLTranslationException
SLTranslationException
private void transformMergePointDecl(TextualJMLMergePointDecl stat, Comment[] originalComments) throws SLTranslationException
SLTranslationException
private void transformClasslevelComments(TypeDeclaration td, java.lang.String fileName) throws SLTranslationException
SLTranslationException
private void transformMethodlevelCommentsHelper(ProgramElement pe, java.lang.String fileName) throws SLTranslationException
SLTranslationException
private void transformMethodlevelComments(MethodDeclaration md, java.lang.String fileName) throws SLTranslationException
SLTranslationException
protected void makeExplicit(TypeDeclaration td)
RecoderModelTransformer
makeExplicit
in class RecoderModelTransformer
public ProblemReport analyze()
analyze
in class TwoPassTransformation
public void makeExplicit()
RecoderModelTransformer
makeExplicit
in class RecoderModelTransformer
public static ImmutableSet<PositionedString> getWarningsOfLastInstance()