T
- The return type of the visit operation. Use Void
for
operations with no return type.public interface KeYParserVisitor<T>
extends org.antlr.v4.runtime.tree.ParseTreeVisitor<T>
KeYParser
.T visitFile(KeYParser.FileContext ctx)
KeYParser.file()
.ctx
- the parse treeT visitDecls(KeYParser.DeclsContext ctx)
KeYParser.decls()
.ctx
- the parse treeT visitProblem(KeYParser.ProblemContext ctx)
KeYParser.problem()
.ctx
- the parse treeT visitOne_include_statement(KeYParser.One_include_statementContext ctx)
KeYParser.one_include_statement()
.ctx
- the parse treeT visitOne_include(KeYParser.One_includeContext ctx)
KeYParser.one_include()
.ctx
- the parse treeT visitOptions_choice(KeYParser.Options_choiceContext ctx)
KeYParser.options_choice()
.ctx
- the parse treeT visitActivated_choice(KeYParser.Activated_choiceContext ctx)
KeYParser.activated_choice()
.ctx
- the parse treeT visitOption_decls(KeYParser.Option_declsContext ctx)
KeYParser.option_decls()
.ctx
- the parse treeT visitChoice(KeYParser.ChoiceContext ctx)
KeYParser.choice()
.ctx
- the parse treeT visitOptionDecl(KeYParser.OptionDeclContext ctx)
KeYParser.optionDecl()
.ctx
- the parse treeT visitSort_decls(KeYParser.Sort_declsContext ctx)
KeYParser.sort_decls()
.ctx
- the parse treeT visitOne_sort_decl(KeYParser.One_sort_declContext ctx)
KeYParser.one_sort_decl()
.ctx
- the parse treeT visitSimple_ident_dots(KeYParser.Simple_ident_dotsContext ctx)
KeYParser.simple_ident_dots()
.ctx
- the parse treeT visitSimple_ident_dots_comma_list(KeYParser.Simple_ident_dots_comma_listContext ctx)
KeYParser.simple_ident_dots_comma_list()
.ctx
- the parse treeT visitExtends_sorts(KeYParser.Extends_sortsContext ctx)
KeYParser.extends_sorts()
.ctx
- the parse treeT visitOneof_sorts(KeYParser.Oneof_sortsContext ctx)
KeYParser.oneof_sorts()
.ctx
- the parse treeT visitKeyjavatype(KeYParser.KeyjavatypeContext ctx)
KeYParser.keyjavatype()
.ctx
- the parse treeT visitProg_var_decls(KeYParser.Prog_var_declsContext ctx)
KeYParser.prog_var_decls()
.ctx
- the parse treeT visitString_literal(KeYParser.String_literalContext ctx)
KeYParser.string_literal()
.ctx
- the parse treeT visitString_value(KeYParser.String_valueContext ctx)
KeYParser.string_value()
.ctx
- the parse treeT visitSimple_ident(KeYParser.Simple_identContext ctx)
KeYParser.simple_ident()
.ctx
- the parse treeT visitSimple_ident_comma_list(KeYParser.Simple_ident_comma_listContext ctx)
KeYParser.simple_ident_comma_list()
.ctx
- the parse treeT visitSchema_var_decls(KeYParser.Schema_var_declsContext ctx)
KeYParser.schema_var_decls()
.ctx
- the parse treeT visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx)
KeYParser.one_schema_var_decl()
.ctx
- the parse treeT visitSchema_modifiers(KeYParser.Schema_modifiersContext ctx)
KeYParser.schema_modifiers()
.ctx
- the parse treeT visitOne_schema_modal_op_decl(KeYParser.One_schema_modal_op_declContext ctx)
KeYParser.one_schema_modal_op_decl()
.ctx
- the parse treeT visitPred_decl(KeYParser.Pred_declContext ctx)
KeYParser.pred_decl()
.ctx
- the parse treeT visitPred_decls(KeYParser.Pred_declsContext ctx)
KeYParser.pred_decls()
.ctx
- the parse treeT visitFunc_decl(KeYParser.Func_declContext ctx)
KeYParser.func_decl()
.ctx
- the parse treeT visitFunc_decls(KeYParser.Func_declsContext ctx)
KeYParser.func_decls()
.ctx
- the parse treeT visitArg_sorts_or_formula(KeYParser.Arg_sorts_or_formulaContext ctx)
KeYParser.arg_sorts_or_formula()
.ctx
- the parse treeT visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_helperContext ctx)
KeYParser.arg_sorts_or_formula_helper()
.ctx
- the parse treeT visitTransform_decl(KeYParser.Transform_declContext ctx)
KeYParser.transform_decl()
.ctx
- the parse treeT visitTransform_decls(KeYParser.Transform_declsContext ctx)
KeYParser.transform_decls()
.ctx
- the parse treeT visitArrayopid(KeYParser.ArrayopidContext ctx)
KeYParser.arrayopid()
.ctx
- the parse treeT visitArg_sorts(KeYParser.Arg_sortsContext ctx)
KeYParser.arg_sorts()
.ctx
- the parse treeT visitWhere_to_bind(KeYParser.Where_to_bindContext ctx)
KeYParser.where_to_bind()
.ctx
- the parse treeT visitRuleset_decls(KeYParser.Ruleset_declsContext ctx)
KeYParser.ruleset_decls()
.ctx
- the parse treeT visitSortId(KeYParser.SortIdContext ctx)
KeYParser.sortId()
.ctx
- the parse treeT visitId_declaration(KeYParser.Id_declarationContext ctx)
KeYParser.id_declaration()
.ctx
- the parse treeT visitFuncpred_name(KeYParser.Funcpred_nameContext ctx)
KeYParser.funcpred_name()
.ctx
- the parse treeT visitTermEOF(KeYParser.TermEOFContext ctx)
KeYParser.termEOF()
.ctx
- the parse treeT visitBoolean_literal(KeYParser.Boolean_literalContext ctx)
KeYParser.boolean_literal()
.ctx
- the parse treeT visitLiterals(KeYParser.LiteralsContext ctx)
KeYParser.literals()
.ctx
- the parse treeT visitTerm(KeYParser.TermContext ctx)
KeYParser.term()
.ctx
- the parse treeT visitParallel_term(KeYParser.Parallel_termContext ctx)
KeYParser.parallel_term()
.ctx
- the parse treeT visitElementary_update_term(KeYParser.Elementary_update_termContext ctx)
KeYParser.elementary_update_term()
.ctx
- the parse treeT visitEquivalence_term(KeYParser.Equivalence_termContext ctx)
KeYParser.equivalence_term()
.ctx
- the parse treeT visitImplication_term(KeYParser.Implication_termContext ctx)
KeYParser.implication_term()
.ctx
- the parse treeT visitDisjunction_term(KeYParser.Disjunction_termContext ctx)
KeYParser.disjunction_term()
.ctx
- the parse treeT visitConjunction_term(KeYParser.Conjunction_termContext ctx)
KeYParser.conjunction_term()
.ctx
- the parse treeT visitTerm60(KeYParser.Term60Context ctx)
KeYParser.term60()
.ctx
- the parse treeT visitNegation_term(KeYParser.Negation_termContext ctx)
negation_term
labeled alternative in KeYParser.unary_formula()
.ctx
- the parse treeT visitQuantifierterm(KeYParser.QuantifiertermContext ctx)
quantifierterm
labeled alternative in KeYParser.unary_formula()
.ctx
- the parse treeT visitModality_term(KeYParser.Modality_termContext ctx)
modality_term
labeled alternative in KeYParser.unary_formula()
.ctx
- the parse treeT visitEquality_term(KeYParser.Equality_termContext ctx)
KeYParser.equality_term()
.ctx
- the parse treeT visitComparison_term(KeYParser.Comparison_termContext ctx)
KeYParser.comparison_term()
.ctx
- the parse treeT visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx)
KeYParser.weak_arith_term()
.ctx
- the parse treeT visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx)
KeYParser.strong_arith_term_1()
.ctx
- the parse treeT visitStrong_arith_term_2(KeYParser.Strong_arith_term_2Context ctx)
KeYParser.strong_arith_term_2()
.ctx
- the parse treeT visitUpdate_term(KeYParser.Update_termContext ctx)
KeYParser.update_term()
.ctx
- the parse treeT visitSubstitution_term(KeYParser.Substitution_termContext ctx)
KeYParser.substitution_term()
.ctx
- the parse treeT visitCast_term(KeYParser.Cast_termContext ctx)
KeYParser.cast_term()
.ctx
- the parse treeT visitUnary_minus_term(KeYParser.Unary_minus_termContext ctx)
KeYParser.unary_minus_term()
.ctx
- the parse treeT visitAtom_prefix(KeYParser.Atom_prefixContext ctx)
KeYParser.atom_prefix()
.ctx
- the parse treeT visitBracket_term(KeYParser.Bracket_termContext ctx)
KeYParser.bracket_term()
.ctx
- the parse treeT visitBracket_suffix_heap(KeYParser.Bracket_suffix_heapContext ctx)
KeYParser.bracket_suffix_heap()
.ctx
- the parse treeT visitBracket_access_heap_update(KeYParser.Bracket_access_heap_updateContext ctx)
bracket_access_heap_update
labeled alternative in KeYParser.brace_suffix()
.ctx
- the parse treeT visitBracket_access_heap_term(KeYParser.Bracket_access_heap_termContext ctx)
bracket_access_heap_term
labeled alternative in KeYParser.brace_suffix()
.ctx
- the parse treeT visitBracket_access_star(KeYParser.Bracket_access_starContext ctx)
bracket_access_star
labeled alternative in KeYParser.brace_suffix()
.ctx
- the parse treeT visitBracket_access_indexrange(KeYParser.Bracket_access_indexrangeContext ctx)
bracket_access_indexrange
labeled alternative in KeYParser.brace_suffix()
.ctx
- the parse treeT visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContext ctx)
KeYParser.primitive_labeled_term()
.ctx
- the parse treeT visitTermParen(KeYParser.TermParenContext ctx)
KeYParser.termParen()
.ctx
- the parse treeT visitAbbreviation(KeYParser.AbbreviationContext ctx)
KeYParser.abbreviation()
.ctx
- the parse treeT visitPrimitive_term(KeYParser.Primitive_termContext ctx)
KeYParser.primitive_term()
.ctx
- the parse treeT visitAccessterm(KeYParser.AccesstermContext ctx)
KeYParser.accessterm()
.ctx
- the parse treeT visitAttribute_star(KeYParser.Attribute_starContext ctx)
attribute_star
labeled alternative in KeYParser.attribute()
.ctx
- the parse treeT visitAttribute_simple(KeYParser.Attribute_simpleContext ctx)
attribute_simple
labeled alternative in KeYParser.attribute()
.ctx
- the parse treeT visitAttribute_complex(KeYParser.Attribute_complexContext ctx)
attribute_complex
labeled alternative in KeYParser.attribute()
.ctx
- the parse treeT visitCall(KeYParser.CallContext ctx)
KeYParser.call()
.ctx
- the parse treeT visitLabel(KeYParser.LabelContext ctx)
KeYParser.label()
.ctx
- the parse treeT visitSingle_label(KeYParser.Single_labelContext ctx)
KeYParser.single_label()
.ctx
- the parse treeT visitLocation_term(KeYParser.Location_termContext ctx)
KeYParser.location_term()
.ctx
- the parse treeT visitIfThenElseTerm(KeYParser.IfThenElseTermContext ctx)
KeYParser.ifThenElseTerm()
.ctx
- the parse treeT visitIfExThenElseTerm(KeYParser.IfExThenElseTermContext ctx)
KeYParser.ifExThenElseTerm()
.ctx
- the parse treeT visitLocset_term(KeYParser.Locset_termContext ctx)
KeYParser.locset_term()
.ctx
- the parse treeT visitBound_variables(KeYParser.Bound_variablesContext ctx)
KeYParser.bound_variables()
.ctx
- the parse treeT visitOne_bound_variable(KeYParser.One_bound_variableContext ctx)
KeYParser.one_bound_variable()
.ctx
- the parse treeT visitArgument_list(KeYParser.Argument_listContext ctx)
KeYParser.argument_list()
.ctx
- the parse treeT visitNumber(KeYParser.NumberContext ctx)
KeYParser.number()
.ctx
- the parse treeT visitChar_literal(KeYParser.Char_literalContext ctx)
KeYParser.char_literal()
.ctx
- the parse treeT visitVarId(KeYParser.VarIdContext ctx)
KeYParser.varId()
.ctx
- the parse treeT visitVarIds(KeYParser.VarIdsContext ctx)
KeYParser.varIds()
.ctx
- the parse treeT visitTriggers(KeYParser.TriggersContext ctx)
KeYParser.triggers()
.ctx
- the parse treeT visitTaclet(KeYParser.TacletContext ctx)
KeYParser.taclet()
.ctx
- the parse treeT visitModifiers(KeYParser.ModifiersContext ctx)
KeYParser.modifiers()
.ctx
- the parse treeT visitSeq(KeYParser.SeqContext ctx)
KeYParser.seq()
.ctx
- the parse treeT visitSeqEOF(KeYParser.SeqEOFContext ctx)
KeYParser.seqEOF()
.ctx
- the parse treeT visitTermorseq(KeYParser.TermorseqContext ctx)
KeYParser.termorseq()
.ctx
- the parse treeT visitSemisequent(KeYParser.SemisequentContext ctx)
KeYParser.semisequent()
.ctx
- the parse treeT visitVarexplist(KeYParser.VarexplistContext ctx)
KeYParser.varexplist()
.ctx
- the parse treeT visitVarexp(KeYParser.VarexpContext ctx)
KeYParser.varexp()
.ctx
- the parse treeT visitVarexpId(KeYParser.VarexpIdContext ctx)
KeYParser.varexpId()
.ctx
- the parse treeT visitVarexp_argument(KeYParser.Varexp_argumentContext ctx)
KeYParser.varexp_argument()
.ctx
- the parse treeT visitGoalspecs(KeYParser.GoalspecsContext ctx)
KeYParser.goalspecs()
.ctx
- the parse treeT visitGoalspecwithoption(KeYParser.GoalspecwithoptionContext ctx)
KeYParser.goalspecwithoption()
.ctx
- the parse treeT visitOption(KeYParser.OptionContext ctx)
KeYParser.option()
.ctx
- the parse treeT visitOption_list(KeYParser.Option_listContext ctx)
KeYParser.option_list()
.ctx
- the parse treeT visitGoalspec(KeYParser.GoalspecContext ctx)
KeYParser.goalspec()
.ctx
- the parse treeT visitReplacewith(KeYParser.ReplacewithContext ctx)
KeYParser.replacewith()
.ctx
- the parse treeT visitAdd(KeYParser.AddContext ctx)
KeYParser.add()
.ctx
- the parse treeT visitAddrules(KeYParser.AddrulesContext ctx)
KeYParser.addrules()
.ctx
- the parse treeT visitAddprogvar(KeYParser.AddprogvarContext ctx)
KeYParser.addprogvar()
.ctx
- the parse treeT visitTacletlist(KeYParser.TacletlistContext ctx)
KeYParser.tacletlist()
.ctx
- the parse treeT visitPvset(KeYParser.PvsetContext ctx)
KeYParser.pvset()
.ctx
- the parse treeT visitRulesets(KeYParser.RulesetsContext ctx)
KeYParser.rulesets()
.ctx
- the parse treeT visitRuleset(KeYParser.RulesetContext ctx)
KeYParser.ruleset()
.ctx
- the parse treeT visitMetaId(KeYParser.MetaIdContext ctx)
KeYParser.metaId()
.ctx
- the parse treeT visitMetaTerm(KeYParser.MetaTermContext ctx)
KeYParser.metaTerm()
.ctx
- the parse treeT visitContracts(KeYParser.ContractsContext ctx)
KeYParser.contracts()
.ctx
- the parse treeT visitInvariants(KeYParser.InvariantsContext ctx)
KeYParser.invariants()
.ctx
- the parse treeT visitOne_contract(KeYParser.One_contractContext ctx)
KeYParser.one_contract()
.ctx
- the parse treeT visitOne_invariant(KeYParser.One_invariantContext ctx)
KeYParser.one_invariant()
.ctx
- the parse treeT visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx)
KeYParser.rulesOrAxioms()
.ctx
- the parse treeT visitBootClassPath(KeYParser.BootClassPathContext ctx)
KeYParser.bootClassPath()
.ctx
- the parse treeT visitClassPaths(KeYParser.ClassPathsContext ctx)
KeYParser.classPaths()
.ctx
- the parse treeT visitJavaSource(KeYParser.JavaSourceContext ctx)
KeYParser.javaSource()
.ctx
- the parse treeT visitOneJavaSource(KeYParser.OneJavaSourceContext ctx)
KeYParser.oneJavaSource()
.ctx
- the parse treeT visitProfile(KeYParser.ProfileContext ctx)
KeYParser.profile()
.ctx
- the parse treeT visitPreferences(KeYParser.PreferencesContext ctx)
KeYParser.preferences()
.ctx
- the parse treeT visitProofScript(KeYParser.ProofScriptContext ctx)
KeYParser.proofScript()
.ctx
- the parse treeT visitProof(KeYParser.ProofContext ctx)
KeYParser.proof()
.ctx
- the parse treeCopyright © 2003-2019 The KeY-Project.