public final class JmlFacade
extends java.lang.Object
JMLLexer.g4
and JMLParser.g4
.
This class is rather a thin layer upon ANTLR4.
As a normal KeY developer you should rather JmlIO
. JmlIO
provides
a translation from strings into KeY constructs.
JmlIO
Modifier and Type | Method and Description |
---|---|
static JmlLexer |
createLexer(org.antlr.v4.runtime.CharStream stream)
Creates an JML lexer for the give stream.
|
static JmlLexer |
createLexer(PositionedString ps)
Creates a JML lexer for the given string with position.
|
static JmlLexer |
createLexer(java.lang.String content)
Creates a JML lexer for a given string.
|
static JmlParser |
createParser(JmlLexer lexer)
Create a JML parser for a given lexer.
|
static org.antlr.v4.runtime.ParserRuleContext |
parseClause(java.lang.String content)
Parses a given clause, like
ensures or requires and returns a parse tree. |
static org.antlr.v4.runtime.ParserRuleContext |
parseExpr(PositionedString expr)
Parse the given string as an JML expr.
|
static org.antlr.v4.runtime.ParserRuleContext |
parseExpr(java.lang.String expr)
Parse the given string as an JML expr.
|
@Nonnull public static JmlLexer createLexer(@Nonnull org.antlr.v4.runtime.CharStream stream)
@Nonnull public static JmlLexer createLexer(@Nonnull PositionedString ps)
@Nonnull public static JmlLexer createLexer(@Nonnull java.lang.String content)
@Nonnull public static org.antlr.v4.runtime.ParserRuleContext parseExpr(@Nonnull PositionedString expr)
public static org.antlr.v4.runtime.ParserRuleContext parseExpr(java.lang.String expr)
@Nonnull public static JmlParser createParser(@Nonnull JmlLexer lexer)
SyntaxErrorReporter
@Nonnull public static org.antlr.v4.runtime.ParserRuleContext parseClause(@Nonnull java.lang.String content)
ensures
or requires
and returns a parse tree.Copyright © 2003-2019 The KeY-Project.