public final class JMLTransformer extends RecoderModelTransformer
RecoderModelTransformer.FinalOuterVarsCollector, RecoderModelTransformer.TransformerCache
Modifier and Type | Field and Description |
---|---|
static ImmutableList<java.lang.String> |
javaMods |
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() |
static java.lang.String |
getFullText(org.antlr.v4.runtime.ParserRuleContext context) |
static ImmutableList<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.
|
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
public static final ImmutableList<java.lang.String> javaMods
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.public static java.lang.String getFullText(org.antlr.v4.runtime.ParserRuleContext context)
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 ImmutableList<PositionedString> getWarningsOfLastInstance()
Copyright © 2003-2019 The KeY-Project.