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<String> |
javaMods |
private static String |
JML
JML markers left and right.
|
private static String |
JMR |
private HashMap<TypeDeclaration,List<? extends Constructor>> |
typeDeclaration2Constructores |
private HashMap<TypeDeclaration,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 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 String |
getJMLModString(ImmutableList<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<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,
String fileName) |
private void |
transformFieldDecl(TextualJMLFieldDecl decl,
Comment[] originalComments) |
private void |
transformMethodDecl(TextualJMLMethodDecl decl,
Comment[] originalComments) |
private void |
transformMethodlevelComments(MethodDeclaration md,
String fileName) |
private void |
transformMethodlevelCommentsHelper(ProgramElement pe,
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 String JML
private static final String JMR
private static final ImmutableList<String> javaMods
private static ImmutableSet<PositionedString> warnings
private final HashMap<TypeDeclaration,List<Method>> typeDeclaration2Methods
private final HashMap<TypeDeclaration,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 String concatenate(Comment[] comments)
private PositionedString prependJavaMods(ImmutableList<String> mods, PositionedString ps)
private String getJMLModString(ImmutableList<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 transformClasslevelComments(TypeDeclaration td, String fileName) throws SLTranslationException
SLTranslationException
private void transformMethodlevelCommentsHelper(ProgramElement pe, String fileName) throws SLTranslationException
SLTranslationException
private void transformMethodlevelComments(MethodDeclaration md, 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()