public class ExpressionBuilder extends DefaultBuilder
KeyAst.Term
.
You should use the facade KeyIO.parseExpression(String)
for term parsing.Modifier and Type | Field and Description |
---|---|
protected boolean |
javaSchemaModeAllowed |
static java.lang.String |
NO_HEAP_EXPRESSION_BEFORE_AT_EXCEPTION_MESSAGE |
LIMIT_SUFFIX, nss, services
Constructor and Description |
---|
ExpressionBuilder(Services services,
NamespaceSet nss) |
ExpressionBuilder(Services services,
NamespaceSet nss,
Namespace<SchemaVariable> schemaNamespace) |
Modifier and Type | Method and Description |
---|---|
<T> T |
accept(org.antlr.v4.runtime.RuleContext ctx)
Helper function for avoiding cast.
|
protected <T> T |
accept(org.antlr.v4.runtime.RuleContext ctx,
java.lang.Object... args) |
protected <T> T |
acceptFirst(java.util.Collection<? extends org.antlr.v4.runtime.RuleContext> seq) |
protected BuildingIssue |
addWarning(org.antlr.v4.runtime.ParserRuleContext node,
java.lang.String description) |
protected BuildingIssue |
addWarning(java.lang.String description) |
protected T |
aggregateResult(T aggregate,
T nextResult) |
protected Term |
capsulateTf(org.antlr.v4.runtime.ParserRuleContext ctx,
java.util.function.Supplier<Term> termSupplier) |
Term |
createAttributeTerm(Term prefix,
Operator attribute,
org.antlr.v4.runtime.ParserRuleContext ctx) |
<T> T |
defaultOnException(T defaultValue,
java.util.function.Supplier<T> supplier) |
protected void |
disableJavaSchemaMode() |
protected void |
each(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument) |
protected void |
each(org.antlr.v4.runtime.RuleContext... ctx) |
protected void |
enableJavaSchemaMode() |
AbbrevMap |
getAbbrevMap() |
java.util.List<BuildingIssue> |
getBuildingIssues() |
TermFactory |
getTermFactory() |
protected Term |
heapSelectionSuffix(Term term,
Term heap,
org.antlr.v4.runtime.ParserRuleContext ctx)
Replace standard heap by another heap in an observer function.
|
boolean |
isClass(java.lang.String p) |
protected boolean |
isHeapTerm(Term term) |
protected <T2> java.util.List<T2> |
mapMapOf(java.util.List<? extends org.antlr.v4.runtime.RuleContext>... ctxss) |
protected <T> java.util.List<T> |
mapOf(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument) |
protected <T> T |
oneOf(org.antlr.v4.runtime.ParserRuleContext... ctxs) |
static java.lang.String |
operatorOfJavaBlock(java.lang.String raw)
Given a raw modality string, this method determines the operator name.
|
protected ImmutableSet<Modality> |
opSVHelper(java.lang.String opName,
ImmutableSet<Modality> modalities) |
protected <T> T |
peek() |
protected <T> T |
pop() |
protected void |
push(java.lang.Object... obj) |
protected void |
semanticError(org.antlr.v4.runtime.ParserRuleContext ctx,
java.lang.String format,
java.lang.Object... args)
Throws a semanticError for the given ast node and message.
|
void |
setAbbrevMap(AbbrevMap abbrevMap) |
protected void |
throwEx(java.lang.Throwable e)
Wraps an exception into a
BuildingException |
static java.lang.String |
trimJavaBlock(java.lang.String raw)
Given a raw modality string, this function trims the modality information.
|
static Term |
updateOrigin(Term t,
org.antlr.v4.runtime.ParserRuleContext ctx) |
java.lang.Object |
visitAbbreviation(KeYParser.AbbreviationContext ctx)
Visit a parse tree produced by
KeYParser.abbreviation() . |
Term |
visitAccessterm(KeYParser.AccesstermContext ctx)
Visit a parse tree produced by
KeYParser.accessterm() . |
java.util.List<Term> |
visitArgument_list(KeYParser.Argument_listContext ctx)
Visit a parse tree produced by
KeYParser.argument_list() . |
java.lang.Object |
visitBoolean_literal(KeYParser.Boolean_literalContext ctx)
Visit a parse tree produced by
KeYParser.boolean_literal() . |
java.util.List<QuantifiableVariable> |
visitBound_variables(KeYParser.Bound_variablesContext ctx)
Visit a parse tree produced by
KeYParser.bound_variables() . |
java.lang.Object |
visitBracket_access_heap_term(KeYParser.Bracket_access_heap_termContext ctx)
Visit a parse tree produced by the
bracket_access_heap_term
labeled alternative in KeYParser.brace_suffix() . |
java.lang.Object |
visitBracket_access_heap_update(KeYParser.Bracket_access_heap_updateContext ctx)
Visit a parse tree produced by the
bracket_access_heap_update
labeled alternative in KeYParser.brace_suffix() . |
java.lang.Object |
visitBracket_access_indexrange(KeYParser.Bracket_access_indexrangeContext ctx)
Visit a parse tree produced by the
bracket_access_indexrange
labeled alternative in KeYParser.brace_suffix() . |
java.lang.Object |
visitBracket_access_star(KeYParser.Bracket_access_starContext ctx)
Visit a parse tree produced by the
bracket_access_star
labeled alternative in KeYParser.brace_suffix() . |
java.lang.Object |
visitBracket_term(KeYParser.Bracket_termContext ctx)
Visit a parse tree produced by
KeYParser.bracket_term() . |
java.lang.Object |
visitCast_term(KeYParser.Cast_termContext ctx)
Visit a parse tree produced by
KeYParser.cast_term() . |
java.lang.Object |
visitChar_literal(KeYParser.Char_literalContext ctx)
Visit a parse tree produced by
KeYParser.char_literal() . |
java.lang.Object |
visitComparison_term(KeYParser.Comparison_termContext ctx)
Visit a parse tree produced by
KeYParser.comparison_term() . |
Term |
visitConjunction_term(KeYParser.Conjunction_termContext ctx)
Visit a parse tree produced by
KeYParser.conjunction_term() . |
Term |
visitDisjunction_term(KeYParser.Disjunction_termContext ctx)
Visit a parse tree produced by
KeYParser.disjunction_term() . |
Term |
visitElementary_update_term(KeYParser.Elementary_update_termContext ctx)
Visit a parse tree produced by
KeYParser.elementary_update_term() . |
Term |
visitEquality_term(KeYParser.Equality_termContext ctx)
Visit a parse tree produced by
KeYParser.equality_term() . |
Term |
visitEquivalence_term(KeYParser.Equivalence_termContext ctx)
Visit a parse tree produced by
KeYParser.equivalence_term() . |
java.lang.Object |
visitFuncpred_name(KeYParser.Funcpred_nameContext ctx)
Handles "[sort]::a.name.or.something.else"
|
java.lang.Object |
visitIfExThenElseTerm(KeYParser.IfExThenElseTermContext ctx)
Visit a parse tree produced by
KeYParser.ifExThenElseTerm() . |
Term |
visitIfThenElseTerm(KeYParser.IfThenElseTermContext ctx)
Visit a parse tree produced by
KeYParser.ifThenElseTerm() . |
Term |
visitImplication_term(KeYParser.Implication_termContext ctx)
Visit a parse tree produced by
KeYParser.implication_term() . |
ImmutableArray<TermLabel> |
visitLabel(KeYParser.LabelContext ctx)
Visit a parse tree produced by
KeYParser.label() . |
java.lang.Object |
visitLocation_term(KeYParser.Location_termContext ctx)
Visit a parse tree produced by
KeYParser.location_term() . |
Term |
visitLocset_term(KeYParser.Locset_termContext ctx)
Visit a parse tree produced by
KeYParser.locset_term() . |
java.lang.Object |
visitMetaId(KeYParser.MetaIdContext ctx)
Visit a parse tree produced by
KeYParser.metaId() . |
Term |
visitMetaTerm(KeYParser.MetaTermContext ctx)
Visit a parse tree produced by
KeYParser.metaTerm() . |
java.lang.Object |
visitModality_term(KeYParser.Modality_termContext ctx)
Visit a parse tree produced by the
modality_term
labeled alternative in KeYParser.unary_formula() . |
Term |
visitNegation_term(KeYParser.Negation_termContext ctx)
Visit a parse tree produced by the
negation_term
labeled alternative in KeYParser.unary_formula() . |
java.lang.Object |
visitNumber(KeYParser.NumberContext ctx)
Visit a parse tree produced by
KeYParser.number() . |
QuantifiableVariable |
visitOne_bound_variable(KeYParser.One_bound_variableContext ctx)
Visit a parse tree produced by
KeYParser.one_bound_variable() . |
Term |
visitParallel_term(KeYParser.Parallel_termContext ctx)
Visit a parse tree produced by
KeYParser.parallel_term() . |
java.lang.Object |
visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContext ctx)
Visit a parse tree produced by
KeYParser.primitive_labeled_term() . |
Term |
visitQuantifierterm(KeYParser.QuantifiertermContext ctx)
Visit a parse tree produced by the
quantifierterm
labeled alternative in KeYParser.unary_formula() . |
Semisequent |
visitSemisequent(KeYParser.SemisequentContext ctx)
Visit a parse tree produced by
KeYParser.semisequent() . |
Sequent |
visitSeq(KeYParser.SeqContext ctx)
Visit a parse tree produced by
KeYParser.seq() . |
Sequent |
visitSeqEOF(KeYParser.SeqEOFContext ctx)
Visit a parse tree produced by
KeYParser.seqEOF() . |
TermLabel |
visitSingle_label(KeYParser.Single_labelContext ctx)
Visit a parse tree produced by
KeYParser.single_label() . |
Term |
visitString_literal(KeYParser.String_literalContext ctx)
Visit a parse tree produced by
KeYParser.string_literal() . |
java.lang.Object |
visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx)
Visit a parse tree produced by
KeYParser.strong_arith_term_1() . |
java.lang.Object |
visitStrong_arith_term_2(KeYParser.Strong_arith_term_2Context ctx)
Visit a parse tree produced by
KeYParser.strong_arith_term_2() . |
java.lang.Object |
visitSubstitution_term(KeYParser.Substitution_termContext ctx)
Visit a parse tree produced by
KeYParser.substitution_term() . |
Term |
visitTermEOF(KeYParser.TermEOFContext ctx)
Visit a parse tree produced by
KeYParser.termEOF() . |
java.lang.Object |
visitTermorseq(KeYParser.TermorseqContext ctx)
Visit a parse tree produced by
KeYParser.termorseq() . |
java.lang.Object |
visitTermParen(KeYParser.TermParenContext ctx)
Visit a parse tree produced by
KeYParser.termParen() . |
java.lang.Object |
visitUnary_minus_term(KeYParser.Unary_minus_termContext ctx)
Visit a parse tree produced by
KeYParser.unary_minus_term() . |
java.lang.Object |
visitUpdate_term(KeYParser.Update_termContext ctx)
Visit a parse tree produced by
KeYParser.update_term() . |
java.lang.Object |
visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx)
Visit a parse tree produced by
KeYParser.weak_arith_term() . |
choices, doLookup, functions, getJavaInfo, getServices, lookup, lookupSort, lookupVarfuncId, namespaces, programVariables, ruleSets, schemaVariables, semanticErrorMsg, setSchemaVariables, sorts, toArraySort, unbindVars, variables, visitArg_sorts_or_formula_helper, visitArg_sorts_or_formula, visitArg_sorts, visitKeyjavatype, visitPvset, visitRuleset, visitRulesets, visitSimple_ident_comma_list, visitSimple_ident_dots_comma_list, visitSimple_ident_dots, visitSimple_ident, visitSortId, visitString_value, visitVarIds, visitWhere_to_bind
visitActivated_choice, visitAdd, visitAddprogvar, visitAddrules, visitArrayopid, visitAtom_prefix, visitAttribute_complex, visitAttribute_simple, visitAttribute_star, visitBootClassPath, visitBracket_suffix_heap, visitCall, visitChoice, visitClassPaths, visitContracts, visitDecls, visitExtends_sorts, visitFile, visitFunc_decl, visitFunc_decls, visitGoalspec, visitGoalspecs, visitGoalspecwithoption, visitId_declaration, visitInvariants, visitJavaSource, visitLiterals, visitModifiers, visitOne_contract, visitOne_include_statement, visitOne_include, visitOne_invariant, visitOne_schema_modal_op_decl, visitOne_schema_var_decl, visitOne_sort_decl, visitOneJavaSource, visitOneof_sorts, visitOption_decls, visitOption_list, visitOption, visitOptionDecl, visitOptions_choice, visitPred_decl, visitPred_decls, visitPreferences, visitPrimitive_term, visitProblem, visitProfile, visitProg_var_decls, visitProof, visitProofScript, visitReplacewith, visitRuleset_decls, visitRulesOrAxioms, visitSchema_modifiers, visitSchema_var_decls, visitSort_decls, visitTaclet, visitTacletlist, visitTerm, visitTerm60, visitTransform_decl, visitTransform_decls, visitTriggers, visitVarexp_argument, visitVarexp, visitVarexpId, visitVarexplist, visitVarId
defaultResult, shouldVisitNextChild, visit, visitChildren, visitErrorNode, visitTerminal
public static final java.lang.String NO_HEAP_EXPRESSION_BEFORE_AT_EXCEPTION_MESSAGE
protected boolean javaSchemaModeAllowed
public ExpressionBuilder(Services services, NamespaceSet nss)
public ExpressionBuilder(Services services, NamespaceSet nss, Namespace<SchemaVariable> schemaNamespace)
public static java.lang.String trimJavaBlock(java.lang.String raw)
raw
- non-null stringpublic static java.lang.String operatorOfJavaBlock(java.lang.String raw)
raw
- public Term visitParallel_term(KeYParser.Parallel_termContext ctx)
KeYParserBaseVisitor
KeYParser.parallel_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitParallel_term
in interface KeYParserVisitor<java.lang.Object>
visitParallel_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitTermEOF(KeYParser.TermEOFContext ctx)
KeYParserBaseVisitor
KeYParser.termEOF()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitTermEOF
in interface KeYParserVisitor<java.lang.Object>
visitTermEOF
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitElementary_update_term(KeYParser.Elementary_update_termContext ctx)
KeYParserBaseVisitor
KeYParser.elementary_update_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitElementary_update_term
in interface KeYParserVisitor<java.lang.Object>
visitElementary_update_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitEquivalence_term(KeYParser.Equivalence_termContext ctx)
KeYParserBaseVisitor
KeYParser.equivalence_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitEquivalence_term
in interface KeYParserVisitor<java.lang.Object>
visitEquivalence_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitImplication_term(KeYParser.Implication_termContext ctx)
KeYParserBaseVisitor
KeYParser.implication_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitImplication_term
in interface KeYParserVisitor<java.lang.Object>
visitImplication_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitDisjunction_term(KeYParser.Disjunction_termContext ctx)
KeYParserBaseVisitor
KeYParser.disjunction_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitDisjunction_term
in interface KeYParserVisitor<java.lang.Object>
visitDisjunction_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitConjunction_term(KeYParser.Conjunction_termContext ctx)
KeYParserBaseVisitor
KeYParser.conjunction_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitConjunction_term
in interface KeYParserVisitor<java.lang.Object>
visitConjunction_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitUnary_minus_term(KeYParser.Unary_minus_termContext ctx)
KeYParserBaseVisitor
KeYParser.unary_minus_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitUnary_minus_term
in interface KeYParserVisitor<java.lang.Object>
visitUnary_minus_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitNegation_term(KeYParser.Negation_termContext ctx)
KeYParserBaseVisitor
negation_term
labeled alternative in KeYParser.unary_formula()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitNegation_term
in interface KeYParserVisitor<java.lang.Object>
visitNegation_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitEquality_term(KeYParser.Equality_termContext ctx)
KeYParserBaseVisitor
KeYParser.equality_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitEquality_term
in interface KeYParserVisitor<java.lang.Object>
visitEquality_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitComparison_term(KeYParser.Comparison_termContext ctx)
KeYParserBaseVisitor
KeYParser.comparison_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitComparison_term
in interface KeYParserVisitor<java.lang.Object>
visitComparison_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx)
KeYParserBaseVisitor
KeYParser.weak_arith_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitWeak_arith_term
in interface KeYParserVisitor<java.lang.Object>
visitWeak_arith_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx)
KeYParserBaseVisitor
KeYParser.strong_arith_term_1()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitStrong_arith_term_1
in interface KeYParserVisitor<java.lang.Object>
visitStrong_arith_term_1
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitStrong_arith_term_2(KeYParser.Strong_arith_term_2Context ctx)
KeYParserBaseVisitor
KeYParser.strong_arith_term_2()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitStrong_arith_term_2
in interface KeYParserVisitor<java.lang.Object>
visitStrong_arith_term_2
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treeprotected Term capsulateTf(org.antlr.v4.runtime.ParserRuleContext ctx, java.util.function.Supplier<Term> termSupplier)
public java.lang.Object visitBracket_term(KeYParser.Bracket_termContext ctx)
KeYParserBaseVisitor
KeYParser.bracket_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitBracket_term
in interface KeYParserVisitor<java.lang.Object>
visitBracket_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Sequent visitSeq(KeYParser.SeqContext ctx)
KeYParserBaseVisitor
KeYParser.seq()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSeq
in interface KeYParserVisitor<java.lang.Object>
visitSeq
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Sequent visitSeqEOF(KeYParser.SeqEOFContext ctx)
KeYParserBaseVisitor
KeYParser.seqEOF()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSeqEOF
in interface KeYParserVisitor<java.lang.Object>
visitSeqEOF
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitTermorseq(KeYParser.TermorseqContext ctx)
KeYParserBaseVisitor
KeYParser.termorseq()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitTermorseq
in interface KeYParserVisitor<java.lang.Object>
visitTermorseq
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Semisequent visitSemisequent(KeYParser.SemisequentContext ctx)
KeYParserBaseVisitor
KeYParser.semisequent()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSemisequent
in interface KeYParserVisitor<java.lang.Object>
visitSemisequent
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treeprotected void enableJavaSchemaMode()
protected void disableJavaSchemaMode()
public java.lang.Object visitMetaId(KeYParser.MetaIdContext ctx)
KeYParserBaseVisitor
KeYParser.metaId()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitMetaId
in interface KeYParserVisitor<java.lang.Object>
visitMetaId
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitMetaTerm(KeYParser.MetaTermContext ctx)
KeYParserBaseVisitor
KeYParser.metaTerm()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitMetaTerm
in interface KeYParserVisitor<java.lang.Object>
visitMetaTerm
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term createAttributeTerm(Term prefix, Operator attribute, org.antlr.v4.runtime.ParserRuleContext ctx)
public Term visitString_literal(KeYParser.String_literalContext ctx)
KeYParserBaseVisitor
KeYParser.string_literal()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitString_literal
in interface KeYParserVisitor<java.lang.Object>
visitString_literal
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitCast_term(KeYParser.Cast_termContext ctx)
KeYParserBaseVisitor
KeYParser.cast_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitCast_term
in interface KeYParserVisitor<java.lang.Object>
visitCast_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitBracket_access_heap_update(KeYParser.Bracket_access_heap_updateContext ctx)
KeYParserBaseVisitor
bracket_access_heap_update
labeled alternative in KeYParser.brace_suffix()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitBracket_access_heap_update
in interface KeYParserVisitor<java.lang.Object>
visitBracket_access_heap_update
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitBracket_access_heap_term(KeYParser.Bracket_access_heap_termContext ctx)
KeYParserBaseVisitor
bracket_access_heap_term
labeled alternative in KeYParser.brace_suffix()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitBracket_access_heap_term
in interface KeYParserVisitor<java.lang.Object>
visitBracket_access_heap_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitBracket_access_star(KeYParser.Bracket_access_starContext ctx)
KeYParserBaseVisitor
bracket_access_star
labeled alternative in KeYParser.brace_suffix()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitBracket_access_star
in interface KeYParserVisitor<java.lang.Object>
visitBracket_access_star
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitBracket_access_indexrange(KeYParser.Bracket_access_indexrangeContext ctx)
KeYParserBaseVisitor
bracket_access_indexrange
labeled alternative in KeYParser.brace_suffix()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitBracket_access_indexrange
in interface KeYParserVisitor<java.lang.Object>
visitBracket_access_indexrange
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitBoolean_literal(KeYParser.Boolean_literalContext ctx)
KeYParserBaseVisitor
KeYParser.boolean_literal()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitBoolean_literal
in interface KeYParserVisitor<java.lang.Object>
visitBoolean_literal
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContext ctx)
KeYParserBaseVisitor
KeYParser.primitive_labeled_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitPrimitive_labeled_term
in interface KeYParserVisitor<java.lang.Object>
visitPrimitive_labeled_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic ImmutableArray<TermLabel> visitLabel(KeYParser.LabelContext ctx)
KeYParserBaseVisitor
KeYParser.label()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitLabel
in interface KeYParserVisitor<java.lang.Object>
visitLabel
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic TermLabel visitSingle_label(KeYParser.Single_labelContext ctx)
KeYParserBaseVisitor
KeYParser.single_label()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSingle_label
in interface KeYParserVisitor<java.lang.Object>
visitSingle_label
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitAbbreviation(KeYParser.AbbreviationContext ctx)
KeYParserBaseVisitor
KeYParser.abbreviation()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitAbbreviation
in interface KeYParserVisitor<java.lang.Object>
visitAbbreviation
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitIfThenElseTerm(KeYParser.IfThenElseTermContext ctx)
KeYParserBaseVisitor
KeYParser.ifThenElseTerm()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitIfThenElseTerm
in interface KeYParserVisitor<java.lang.Object>
visitIfThenElseTerm
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitIfExThenElseTerm(KeYParser.IfExThenElseTermContext ctx)
KeYParserBaseVisitor
KeYParser.ifExThenElseTerm()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitIfExThenElseTerm
in interface KeYParserVisitor<java.lang.Object>
visitIfExThenElseTerm
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitQuantifierterm(KeYParser.QuantifiertermContext ctx)
KeYParserBaseVisitor
quantifierterm
labeled alternative in KeYParser.unary_formula()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitQuantifierterm
in interface KeYParserVisitor<java.lang.Object>
visitQuantifierterm
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Term visitLocset_term(KeYParser.Locset_termContext ctx)
KeYParserBaseVisitor
KeYParser.locset_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitLocset_term
in interface KeYParserVisitor<java.lang.Object>
visitLocset_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitLocation_term(KeYParser.Location_termContext ctx)
KeYParserBaseVisitor
KeYParser.location_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitLocation_term
in interface KeYParserVisitor<java.lang.Object>
visitLocation_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitSubstitution_term(KeYParser.Substitution_termContext ctx)
KeYParserBaseVisitor
KeYParser.substitution_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSubstitution_term
in interface KeYParserVisitor<java.lang.Object>
visitSubstitution_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitUpdate_term(KeYParser.Update_termContext ctx)
KeYParserBaseVisitor
KeYParser.update_term()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitUpdate_term
in interface KeYParserVisitor<java.lang.Object>
visitUpdate_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.util.List<QuantifiableVariable> visitBound_variables(KeYParser.Bound_variablesContext ctx)
KeYParserBaseVisitor
KeYParser.bound_variables()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitBound_variables
in interface KeYParserVisitor<java.lang.Object>
visitBound_variables
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic QuantifiableVariable visitOne_bound_variable(KeYParser.One_bound_variableContext ctx)
KeYParserBaseVisitor
KeYParser.one_bound_variable()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitOne_bound_variable
in interface KeYParserVisitor<java.lang.Object>
visitOne_bound_variable
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitModality_term(KeYParser.Modality_termContext ctx)
KeYParserBaseVisitor
modality_term
labeled alternative in KeYParser.unary_formula()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitModality_term
in interface KeYParserVisitor<java.lang.Object>
visitModality_term
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.util.List<Term> visitArgument_list(KeYParser.Argument_listContext ctx)
KeYParserBaseVisitor
KeYParser.argument_list()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitArgument_list
in interface KeYParserVisitor<java.lang.Object>
visitArgument_list
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitChar_literal(KeYParser.Char_literalContext ctx)
KeYParserBaseVisitor
KeYParser.char_literal()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitChar_literal
in interface KeYParserVisitor<java.lang.Object>
visitChar_literal
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic boolean isClass(java.lang.String p)
public java.lang.Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx)
visitFuncpred_name
in interface KeYParserVisitor<java.lang.Object>
visitFuncpred_name
in class DefaultBuilder
ctx
- public java.lang.Object visitTermParen(KeYParser.TermParenContext ctx)
KeYParserBaseVisitor
KeYParser.termParen()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitTermParen
in interface KeYParserVisitor<java.lang.Object>
visitTermParen
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic <T> T defaultOnException(T defaultValue, java.util.function.Supplier<T> supplier)
public Term visitAccessterm(KeYParser.AccesstermContext ctx)
KeYParserBaseVisitor
KeYParser.accessterm()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitAccessterm
in interface KeYParserVisitor<java.lang.Object>
visitAccessterm
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitNumber(KeYParser.NumberContext ctx)
KeYParserBaseVisitor
KeYParser.number()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitNumber
in interface KeYParserVisitor<java.lang.Object>
visitNumber
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic TermFactory getTermFactory()
protected ImmutableSet<Modality> opSVHelper(java.lang.String opName, ImmutableSet<Modality> modalities)
protected boolean isHeapTerm(Term term)
protected Term heapSelectionSuffix(Term term, Term heap, org.antlr.v4.runtime.ParserRuleContext ctx)
public void setAbbrevMap(AbbrevMap abbrevMap)
public AbbrevMap getAbbrevMap()
@Nullable public <T> T accept(@Nullable org.antlr.v4.runtime.RuleContext ctx)
T
- ctx
- protected T aggregateResult(T aggregate, T nextResult)
aggregateResult
in class org.antlr.v4.runtime.tree.AbstractParseTreeVisitor<T>
protected <T> T peek()
T
- protected <T> T acceptFirst(java.util.Collection<? extends org.antlr.v4.runtime.RuleContext> seq)
protected <T> T pop()
protected void push(java.lang.Object... obj)
@Nullable protected <T> T accept(@Nullable org.antlr.v4.runtime.RuleContext ctx, java.lang.Object... args)
protected <T> T oneOf(org.antlr.v4.runtime.ParserRuleContext... ctxs)
protected <T> java.util.List<T> mapOf(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument)
protected void each(org.antlr.v4.runtime.RuleContext... ctx)
protected void each(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument)
protected <T2> java.util.List<T2> mapMapOf(java.util.List<? extends org.antlr.v4.runtime.RuleContext>... ctxss)
@Nonnull public java.util.List<BuildingIssue> getBuildingIssues()
protected BuildingIssue addWarning(org.antlr.v4.runtime.ParserRuleContext node, java.lang.String description)
protected BuildingIssue addWarning(java.lang.String description)
protected void semanticError(org.antlr.v4.runtime.ParserRuleContext ctx, java.lang.String format, java.lang.Object... args)
ctx
- format
- args
- protected void throwEx(java.lang.Throwable e)
BuildingException
e
- Copyright © 2003-2019 The KeY-Project.