public class JmlIO
extends java.lang.Object
This facade stores a the parsing context of JML constructs, e.g., the return or self variable, the parameters.
You can set these values via the builder methods. The translate*
methods translate
a given ParserRuleContext
into a KeY-entity.
It also maintains the list of translation warnings, see getWarnings()
.
Internally, this is a type-safe wrapper around the visitor Translator
.
Translator
Constructor and Description |
---|
JmlIO()
Generate an empty jml i/o instance.
|
JmlIO(Services services,
KeYJavaType specInClass,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores)
Full constructor of this class.
|
Modifier and Type | Method and Description |
---|---|
JmlIO |
atBefore(java.util.Map<LocationVariable,Term> atBefores) |
JmlIO |
atPres(java.util.Map<LocationVariable,Term> atPres) |
JmlIO |
classType(KeYJavaType classType)
Sets the sort/type of the class containing the interpreted JML.
|
JmlIO |
clear()
Clears the internal fields.
|
void |
clearWarnings() |
JmlIO |
exceptionVariable(ProgramVariable excVar)
Sets the variable that is used to store exceptions.
|
ImmutableList<PositionedString> |
getWarnings()
returns the gathered interpretation warnings, e.g., deprecated constructs.
|
static boolean |
isKnownFunction(java.lang.String functionName)
Checks whether the given
functionName is a known JML function for KeY. |
JmlIO |
parameters(ImmutableList<ProgramVariable> params)
Sets the current list of known parameter.
|
ImmutableList<TextualJMLConstruct> |
parseClassLevel(JmlLexer lexer)
Parses a JML constructs on class level, e.g., invariants and methods contracts, and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
parseClassLevel(java.lang.String content)
Parses a JML constructs on class level, e.g., invariants and methods contracts, and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
parseClassLevel(java.lang.String concatenatedComment,
java.lang.String fileName,
Position pos)
Parse and interpret class level comments.
|
Term |
parseExpression(PositionedString p)
Parse and interpret the given string as an JML expression in the current context.
|
Term |
parseExpression(java.lang.String input)
Parses and interpret the given input as an JML expression in the current context.
|
ImmutableList<TextualJMLConstruct> |
parseMethodLevel(PositionedString positionedString)
Parses a JML constructs which occurs inside methods (mostly JML statements) and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
parseMethodLevel(java.lang.String concatenatedComment,
java.lang.String fileName,
Position position)
Parse and interpret the given string as a method level construct.
|
JmlIO |
resultVariable(ProgramVariable resultVar)
Sets the variable representing
\result . |
JmlIO |
selfVar(ProgramVariable selfVar)
Sets the variable representing the
this reference. |
JmlIO |
services(Services services)
Sets the current services
|
Triple<IObserverFunction,Term,Term> |
translateDependencyContract(LabeledParserRuleContext ctx)
Translates a dependency contract.
|
Triple<IObserverFunction,Term,Term> |
translateDependencyContract(org.antlr.v4.runtime.ParserRuleContext ctx)
Translates the given context into a dependency contract, aka, accessible-clause or depends-clause.
|
InfFlowSpec |
translateInfFlow(LabeledParserRuleContext expr)
Translate the given context into an information flow specification.
|
InfFlowSpec |
translateInfFlow(org.antlr.v4.runtime.ParserRuleContext expr)
Translate the given context into an information flow specification.
|
Pair<Label,Term> |
translateLabeledClause(LabeledParserRuleContext parserRuleContext,
OriginTermLabel.SpecType type)
Interpret a labeled term (breaks clauses, continue clauses).
|
MergeParamsSpec |
translateMergeParams(JmlParser.MergeparamsspecContext ctx)
Interpret a merge params.
|
Pair<IObserverFunction,Term> |
translateRepresents(LabeledParserRuleContext clause)
Interpret a given represents clause.
|
Pair<IObserverFunction,Term> |
translateRepresents(org.antlr.v4.runtime.ParserRuleContext clause)
Interpret the given parse tree as a represents clause
|
Term |
translateTerm(LabeledParserRuleContext expr)
Interpret the given parse tree as an JML expression in the current context.
|
Term |
translateTerm(LabeledParserRuleContext expr,
OriginTermLabel.SpecType type)
Interpret the given parse tree as an JML expression in the current context.
|
Term |
translateTerm(org.antlr.v4.runtime.ParserRuleContext expr)
Interpret the given parse tree as an JML expression in the current context.
|
Term |
translateTerm(org.antlr.v4.runtime.ParserRuleContext expr,
OriginTermLabel.SpecType type)
Interpret the given parse tree as an JML expression in the current context.
|
public JmlIO()
services(Services)
is provided.public JmlIO(@Nonnull Services services, @Nullable KeYJavaType specInClass, @Nullable ProgramVariable selfVar, @Nullable ImmutableList<ProgramVariable> paramVars, @Nullable ProgramVariable resultVar, @Nullable ProgramVariable excVar, @Nullable java.util.Map<LocationVariable,Term> atPres, @Nullable java.util.Map<LocationVariable,Term> atBefores)
services
- a service object used for constructing the termsspecInClass
- the class in which the expression and contracts should be evaluatedselfVar
- the self variable considered for this
-referencesparamVars
- a list of parameter variablesresultVar
- the \return
-variableexcVar
- the variable to store exceptionatPres
- i do not knowatBefores
- i do not knowpublic Pair<IObserverFunction,Term> translateRepresents(org.antlr.v4.runtime.ParserRuleContext clause)
java.lang.ClassCastException
- if unsuitable parser rule context is given@Nonnull public Pair<IObserverFunction,Term> translateRepresents(@Nonnull LabeledParserRuleContext clause)
Note weigl: This method does not add the given term label to the returned objects. I am not if this is currently wanted/needed.
java.lang.ClassCastException
- if unsuitable parser rule context is given@param clausepublic static boolean isKnownFunction(java.lang.String functionName)
functionName
is a known JML function for KeY.functionName
- a stringJmlTermFactory.jml2jdl
public Pair<Label,Term> translateLabeledClause(LabeledParserRuleContext parserRuleContext, OriginTermLabel.SpecType type)
public MergeParamsSpec translateMergeParams(JmlParser.MergeparamsspecContext ctx)
public ImmutableList<TextualJMLConstruct> parseClassLevel(java.lang.String concatenatedComment, java.lang.String fileName, Position pos)
public ImmutableList<PositionedString> getWarnings()
public ImmutableList<TextualJMLConstruct> parseMethodLevel(java.lang.String concatenatedComment, java.lang.String fileName, Position position)
public Term parseExpression(PositionedString p)
@Nonnull public Term translateTerm(@Nonnull org.antlr.v4.runtime.ParserRuleContext expr)
public Term translateTerm(LabeledParserRuleContext expr)
public Term translateTerm(LabeledParserRuleContext expr, OriginTermLabel.SpecType type)
type
and in labeled parse tree.public Term translateTerm(org.antlr.v4.runtime.ParserRuleContext expr, OriginTermLabel.SpecType type)
public Term parseExpression(java.lang.String input)
@Nonnull public InfFlowSpec translateInfFlow(@Nonnull org.antlr.v4.runtime.ParserRuleContext expr)
expr
- should be a JmlParser.Separates_clauseContext
or JmlParser.Determines_clauseContext
,
or JmlParser.Loop_separates_clauseContext
or JmlParser.Loop_determines_clauseContext
.java.lang.ClassCastException
- if the expr
is not suitablepublic InfFlowSpec translateInfFlow(LabeledParserRuleContext expr)
translateInfFlow(ParserRuleContext)
but this method can also handles the given label.public Triple<IObserverFunction,Term,Term> translateDependencyContract(org.antlr.v4.runtime.ParserRuleContext ctx)
ctx
- should a JmlParser.Accessible_clauseContext
java.lang.ClassCastException
- if the ctx
is not suitablepublic Triple<IObserverFunction,Term,Term> translateDependencyContract(LabeledParserRuleContext ctx)
Note (weigl): No label is currently attached.
java.lang.ClassCastException
- if the ctx
is not suitablepublic JmlIO selfVar(ProgramVariable selfVar)
this
reference.public JmlIO parameters(ImmutableList<ProgramVariable> params)
public JmlIO exceptionVariable(ProgramVariable excVar)
public JmlIO atPres(java.util.Map<LocationVariable,Term> atPres)
public JmlIO resultVariable(ProgramVariable resultVar)
\result
.public JmlIO classType(KeYJavaType classType)
public JmlIO atBefore(java.util.Map<LocationVariable,Term> atBefores)
public JmlIO clear()
public void clearWarnings()
public ImmutableList<TextualJMLConstruct> parseClassLevel(JmlLexer lexer)
public ImmutableList<TextualJMLConstruct> parseClassLevel(java.lang.String content)
public ImmutableList<TextualJMLConstruct> parseMethodLevel(PositionedString positionedString)
Copyright © 2003-2019 The KeY-Project.