public class KeYJMLPreParser extends Parser
Modifier and Type | Class and Description |
---|---|
protected class |
KeYJMLPreParser.DFA1 |
protected class |
KeYJMLPreParser.DFA15 |
protected class |
KeYJMLPreParser.DFA18 |
protected class |
KeYJMLPreParser.DFA2 |
protected class |
KeYJMLPreParser.DFA23 |
protected class |
KeYJMLPreParser.DFA3 |
protected class |
KeYJMLPreParser.DFA36 |
protected class |
KeYJMLPreParser.DFA5 |
protected class |
KeYJMLPreParser.DFA9 |
DEFAULT_TOKEN_CHANNEL, HIDDEN, INITIAL_FOLLOW_STACK_SIZE, MEMO_RULE_FAILED, MEMO_RULE_UNKNOWN, NEXT_TOKEN_RULE_NAME, state
Modifier | Constructor and Description |
---|---|
private |
KeYJMLPreParser(KeYJMLPreLexer lexer,
String fileName,
Position offsetPos) |
|
KeYJMLPreParser(String comment,
String fileName,
Position offsetPos) |
|
KeYJMLPreParser(TokenStream input) |
|
KeYJMLPreParser(TokenStream input,
RecognizerSharedState state) |
getCurrentInputSymbol, getMissingSymbol, getSourceName, getTokenStream, reset, setTokenStream, traceIn, traceOut
alreadyParsedRule, beginResync, combineFollows, computeContextSensitiveRuleFOLLOW, computeErrorRecoverySet, consumeUntil, consumeUntil, displayRecognitionError, emitErrorMessage, endResync, failed, getBacktrackingLevel, getErrorHeader, getErrorMessage, getNumberOfSyntaxErrors, getRuleInvocationStack, getRuleInvocationStack, getRuleMemoization, getRuleMemoizationCacheSize, getTokenErrorDisplay, match, matchAny, memoize, mismatchIsMissingToken, mismatchIsUnwantedToken, pushFollow, recover, reportError, setBacktrackingLevel, toStrings, traceIn, traceOut
public static final String[] tokenNames
public static final int EOF
public static final int ABSTRACT
public static final int ACCESSIBLE
public static final int ACCESSIBLE_REDUNDANTLY
public static final int ALSO
public static final int ASSERT
public static final int ASSERT_REDUNDANTLY
public static final int ASSIGNABLE
public static final int ASSIGNABLE_RED
public static final int ASSUME
public static final int ASSUME_REDUNDANTLY
public static final int AXIOM
public static final int AXIOM_NAME_BEGIN
public static final int AXIOM_NAME_END
public static final int BEHAVIOR
public static final int BEHAVIOUR
public static final int BODY
public static final int BRACE_DISPATCH
public static final int BREAKS
public static final int BREAK_BEHAVIOR
public static final int BREAK_BEHAVIOUR
public static final int CAPTURES
public static final int CAPTURES_RED
public static final int CODE
public static final int CODE_BIGINT_MATH
public static final int CODE_JAVA_MATH
public static final int CODE_SAFE_MATH
public static final int COMMA
public static final int CONST
public static final int CONSTRAINT
public static final int CONSTRAINT_RED
public static final int CONTINUES
public static final int CONTINUE_BEHAVIOR
public static final int CONTINUE_BEHAVIOUR
public static final int DEBUG
public static final int DECIMALINTEGERLITERAL
public static final int DECREASES
public static final int DECREASES_REDUNDANTLY
public static final int DECREASING
public static final int DECREASING_REDUNDANTLY
public static final int DETERMINES
public static final int DIGIT
public static final int DIGITS
public static final int DIVERGES
public static final int DIVERGES_RED
public static final int DOT
public static final int DURATION
public static final int DURATION_RED
public static final int EMPTYBRACKETS
public static final int ENSURES
public static final int ENSURES_FREE
public static final int ENSURES_RED
public static final int EQUALITY
public static final int ESC
public static final int EXCEPTIONAL_BEHAVIOR
public static final int EXCEPTIONAL_BEHAVIOUR
public static final int EXSURES
public static final int EXSURES_RED
public static final int FINAL
public static final int FORALL
public static final int FOR_EXAMPLE
public static final int GHOST
public static final int HELPER
public static final int HEXDIGIT
public static final int HEXINTEGERLITERAL
public static final int HEXNUMERAL
public static final int IDENT
public static final int IMPLIES_THAT
public static final int IN
public static final int INITIALLY
public static final int INSTANCE
public static final int INTEGERLITERAL
public static final int INTEGERTYPESUFFIX
public static final int INVARIANT
public static final int INVARIANT_RED
public static final int IN_RED
public static final int JAVAOPERATOR
public static final int JMLSPECIALSYMBOL
public static final int JOIN_PROC
public static final int LETTER
public static final int LOOP_INVARIANT
public static final int LOOP_INVARIANT_RED
public static final int LPAREN
public static final int MAINTAINING
public static final int MAINTAINING_REDUNDANTLY
public static final int MAPS
public static final int MAPS_RED
public static final int MEASURED_BY
public static final int MEASURED_BY_REDUNDANTLY
public static final int ML_COMMENT
public static final int MODEL
public static final int MODEL_BEHAVIOR
public static final int MODEL_BEHAVIOUR
public static final int MODIFIABLE
public static final int MODIFIABLE_RED
public static final int MODIFIES
public static final int MODIFIES_RED
public static final int MONITORED
public static final int MONITORS_FOR
public static final int NATIVE
public static final int NEST_END
public static final int NEST_START
public static final int NONZERODIGIT
public static final int NON_NULL
public static final int NORMAL_BEHAVIOR
public static final int NORMAL_BEHAVIOUR
public static final int NOWARN
public static final int NO_STATE
public static final int NULLABLE
public static final int NULLABLE_BY_DEFAULT
public static final int OCTALDIGIT
public static final int OCTALINTEGERLITERAL
public static final int OCTALNUMERAL
public static final int OLD
public static final int POST
public static final int POST_RED
public static final int PRE
public static final int PRE_RED
public static final int PRIVATE
public static final int PROTECTED
public static final int PUBLIC
public static final int PURE
public static final int READABLE
public static final int REPRESENTS
public static final int REPRESENTS_RED
public static final int REQUIRES
public static final int REQUIRES_FREE
public static final int REQUIRES_RED
public static final int RESPECTS
public static final int RETURNS
public static final int RETURN_BEHAVIOR
public static final int RETURN_BEHAVIOUR
public static final int RPAREN
public static final int SEMICOLON
public static final int SEPARATES
public static final int SET
public static final int SIGNALS
public static final int SIGNALS_ONLY
public static final int SIGNALS_ONLY_RED
public static final int SIGNALS_RED
public static final int SL_COMMENT
public static final int SPEC_BIGINT_MATH
public static final int SPEC_JAVA_MATH
public static final int SPEC_NAME
public static final int SPEC_PROTECTED
public static final int SPEC_PUBLIC
public static final int SPEC_SAFE_MATH
public static final int STATIC
public static final int STRICTFP
public static final int STRICTLY_PURE
public static final int STRING_LITERAL
public static final int SYNCHRONIZED
public static final int TRANSIENT
public static final int TWO_STATE
public static final int UNINITIALIZED
public static final int UNREACHABLE
public static final int VOLATILE
public static final int WHEN
public static final int WHEN_RED
public static final int WORKING_SPACE
public static final int WORKING_SPACE_RED
public static final int WRITABLE
public static final int WS
public static final int AXION_NAME_END
public static final int CODE_SAVE_MATH
public static final int INITIALISER
public static final int LOOP_INVARIANT_REDUNDANTLY
public static final int SPEC_SAVE_MATH
private KeYJMLPreLexer lexer
private SLTranslationExceptionManager excManager
private ImmutableSet<PositionedString> warnings
protected KeYJMLPreParser.DFA1 dfa1
protected KeYJMLPreParser.DFA2 dfa2
protected KeYJMLPreParser.DFA3 dfa3
protected KeYJMLPreParser.DFA5 dfa5
protected KeYJMLPreParser.DFA9 dfa9
protected KeYJMLPreParser.DFA15 dfa15
protected KeYJMLPreParser.DFA18 dfa18
protected KeYJMLPreParser.DFA23 dfa23
protected KeYJMLPreParser.DFA36 dfa36
static final String DFA1_eotS
static final String DFA1_eofS
static final String DFA1_minS
static final String DFA1_maxS
static final String DFA1_acceptS
static final String DFA1_specialS
static final String[] DFA1_transitionS
static final short[] DFA1_eot
static final short[] DFA1_eof
static final char[] DFA1_min
static final char[] DFA1_max
static final short[] DFA1_accept
static final short[] DFA1_special
static final short[][] DFA1_transition
static final String DFA2_eotS
static final String DFA2_eofS
static final String DFA2_minS
static final String DFA2_maxS
static final String DFA2_acceptS
static final String DFA2_specialS
static final String[] DFA2_transitionS
static final short[] DFA2_eot
static final short[] DFA2_eof
static final char[] DFA2_min
static final char[] DFA2_max
static final short[] DFA2_accept
static final short[] DFA2_special
static final short[][] DFA2_transition
static final String DFA3_eotS
static final String DFA3_eofS
static final String DFA3_minS
static final String DFA3_maxS
static final String DFA3_acceptS
static final String DFA3_specialS
static final String[] DFA3_transitionS
static final short[] DFA3_eot
static final short[] DFA3_eof
static final char[] DFA3_min
static final char[] DFA3_max
static final short[] DFA3_accept
static final short[] DFA3_special
static final short[][] DFA3_transition
static final String DFA5_eotS
static final String DFA5_eofS
static final String DFA5_minS
static final String DFA5_maxS
static final String DFA5_acceptS
static final String DFA5_specialS
static final String[] DFA5_transitionS
static final short[] DFA5_eot
static final short[] DFA5_eof
static final char[] DFA5_min
static final char[] DFA5_max
static final short[] DFA5_accept
static final short[] DFA5_special
static final short[][] DFA5_transition
static final String DFA9_eotS
static final String DFA9_eofS
static final String DFA9_minS
static final String DFA9_maxS
static final String DFA9_acceptS
static final String DFA9_specialS
static final String[] DFA9_transitionS
static final short[] DFA9_eot
static final short[] DFA9_eof
static final char[] DFA9_min
static final char[] DFA9_max
static final short[] DFA9_accept
static final short[] DFA9_special
static final short[][] DFA9_transition
static final String DFA15_eotS
static final String DFA15_eofS
static final String DFA15_minS
static final String DFA15_maxS
static final String DFA15_acceptS
static final String DFA15_specialS
static final String[] DFA15_transitionS
static final short[] DFA15_eot
static final short[] DFA15_eof
static final char[] DFA15_min
static final char[] DFA15_max
static final short[] DFA15_accept
static final short[] DFA15_special
static final short[][] DFA15_transition
static final String DFA18_eotS
static final String DFA18_eofS
static final String DFA18_minS
static final String DFA18_maxS
static final String DFA18_acceptS
static final String DFA18_specialS
static final String[] DFA18_transitionS
static final short[] DFA18_eot
static final short[] DFA18_eof
static final char[] DFA18_min
static final char[] DFA18_max
static final short[] DFA18_accept
static final short[] DFA18_special
static final short[][] DFA18_transition
static final String DFA23_eotS
static final String DFA23_eofS
static final String DFA23_minS
static final String DFA23_maxS
static final String DFA23_acceptS
static final String DFA23_specialS
static final String[] DFA23_transitionS
static final short[] DFA23_eot
static final short[] DFA23_eof
static final char[] DFA23_min
static final char[] DFA23_max
static final short[] DFA23_accept
static final short[] DFA23_special
static final short[][] DFA23_transition
static final String DFA36_eotS
static final String DFA36_eofS
static final String DFA36_minS
static final String DFA36_maxS
static final String DFA36_acceptS
static final String DFA36_specialS
static final String[] DFA36_transitionS
static final short[] DFA36_eot
static final short[] DFA36_eof
static final char[] DFA36_min
static final char[] DFA36_max
static final short[] DFA36_accept
static final short[] DFA36_special
static final short[][] DFA36_transition
public static final BitSet FOLLOW_modifiers_in_classlevel_comment115
public static final BitSet FOLLOW_classlevel_element_in_classlevel_comment131
public static final BitSet FOLLOW_modifiers_in_classlevel_comment150
public static final BitSet FOLLOW_EOF_in_classlevel_comment163
public static final BitSet FOLLOW_class_invariant_in_classlevel_element204
public static final BitSet FOLLOW_depends_clause_in_classlevel_element225
public static final BitSet FOLLOW_method_specification_in_classlevel_element238
public static final BitSet FOLLOW_field_or_method_declaration_in_classlevel_element251
public static final BitSet FOLLOW_represents_clause_in_classlevel_element264
public static final BitSet FOLLOW_history_constraint_in_classlevel_element277
public static final BitSet FOLLOW_initially_clause_in_classlevel_element290
public static final BitSet FOLLOW_class_axiom_in_classlevel_element303
public static final BitSet FOLLOW_monitors_for_clause_in_classlevel_element316
public static final BitSet FOLLOW_readable_if_clause_in_classlevel_element329
public static final BitSet FOLLOW_writable_if_clause_in_classlevel_element342
public static final BitSet FOLLOW_datagroup_clause_in_classlevel_element355
public static final BitSet FOLLOW_set_statement_in_classlevel_element368
public static final BitSet FOLLOW_assert_statement_in_classlevel_element385
public static final BitSet FOLLOW_assume_statement_in_classlevel_element399
public static final BitSet FOLLOW_nowarn_pragma_in_classlevel_element413
public static final BitSet FOLLOW_modifiers_in_methodlevel_comment448
public static final BitSet FOLLOW_methodlevel_element_in_methodlevel_comment453
public static final BitSet FOLLOW_EOF_in_methodlevel_comment466
public static final BitSet FOLLOW_field_or_method_declaration_in_methodlevel_element507
public static final BitSet FOLLOW_set_statement_in_methodlevel_element520
public static final BitSet FOLLOW_loop_specification_in_methodlevel_element533
public static final BitSet FOLLOW_assert_statement_in_methodlevel_element546
public static final BitSet FOLLOW_assume_statement_in_methodlevel_element559
public static final BitSet FOLLOW_nowarn_pragma_in_methodlevel_element572
public static final BitSet FOLLOW_debug_statement_in_methodlevel_element585
public static final BitSet FOLLOW_block_specification_in_methodlevel_element598
public static final BitSet FOLLOW_modifier_in_modifiers648
public static final BitSet FOLLOW_ABSTRACT_in_modifier681
public static final BitSet FOLLOW_FINAL_in_modifier706
public static final BitSet FOLLOW_GHOST_in_modifier734
public static final BitSet FOLLOW_HELPER_in_modifier762
public static final BitSet FOLLOW_INSTANCE_in_modifier789
public static final BitSet FOLLOW_MODEL_in_modifier814
public static final BitSet FOLLOW_NON_NULL_in_modifier842
public static final BitSet FOLLOW_NULLABLE_in_modifier867
public static final BitSet FOLLOW_NULLABLE_BY_DEFAULT_in_modifier892
public static final BitSet FOLLOW_PRIVATE_in_modifier906
public static final BitSet FOLLOW_PROTECTED_in_modifier932
public static final BitSet FOLLOW_PUBLIC_in_modifier956
public static final BitSet FOLLOW_PURE_in_modifier983
public static final BitSet FOLLOW_STRICTLY_PURE_in_modifier1012
public static final BitSet FOLLOW_SPEC_PROTECTED_in_modifier1032
public static final BitSet FOLLOW_SPEC_PUBLIC_in_modifier1051
public static final BitSet FOLLOW_STATIC_in_modifier1073
public static final BitSet FOLLOW_TWO_STATE_in_modifier1100
public static final BitSet FOLLOW_NO_STATE_in_modifier1124
public static final BitSet FOLLOW_SPEC_JAVA_MATH_in_modifier1149
public static final BitSet FOLLOW_SPEC_SAVE_MATH_in_modifier1168
public static final BitSet FOLLOW_SPEC_BIGINT_MATH_in_modifier1187
public static final BitSet FOLLOW_CODE_JAVA_MATH_in_modifier1204
public static final BitSet FOLLOW_CODE_SAVE_MATH_in_modifier1223
public static final BitSet FOLLOW_CODE_BIGINT_MATH_in_modifier1242
public static final BitSet FOLLOW_invariant_keyword_in_class_invariant1282
public static final BitSet FOLLOW_expression_in_class_invariant1291
public static final BitSet FOLLOW_AXIOM_NAME_BEGIN_in_axiom_name1320
public static final BitSet FOLLOW_IDENT_in_axiom_name1324
public static final BitSet FOLLOW_AXIOM_NAME_END_in_axiom_name1326
public static final BitSet FOLLOW_AXIOM_in_class_axiom1416
public static final BitSet FOLLOW_expression_in_class_axiom1420
public static final BitSet FOLLOW_INITIALLY_in_initially_clause1485
public static final BitSet FOLLOW_expression_in_initially_clause1489
public static final BitSet FOLLOW_also_keyword_in_method_specification1534
public static final BitSet FOLLOW_spec_case_in_method_specification1544
public static final BitSet FOLLOW_also_keyword_in_method_specification1570
public static final BitSet FOLLOW_spec_case_in_method_specification1576
public static final BitSet FOLLOW_lightweight_spec_case_in_spec_case1650
public static final BitSet FOLLOW_heavyweight_spec_case_in_spec_case1662
public static final BitSet FOLLOW_generic_spec_case_in_lightweight_spec_case1705
public static final BitSet FOLLOW_modifier_in_heavyweight_spec_case1749
public static final BitSet FOLLOW_behavior_spec_case_in_heavyweight_spec_case1769
public static final BitSet FOLLOW_break_behavior_spec_case_in_heavyweight_spec_case1783
public static final BitSet FOLLOW_continue_behavior_spec_case_in_heavyweight_spec_case1797
public static final BitSet FOLLOW_exceptional_behavior_spec_case_in_heavyweight_spec_case1811
public static final BitSet FOLLOW_normal_behavior_spec_case_in_heavyweight_spec_case1821
public static final BitSet FOLLOW_model_behavior_spec_case_in_heavyweight_spec_case1831
public static final BitSet FOLLOW_return_behavior_spec_case_in_heavyweight_spec_case1841
public static final BitSet FOLLOW_behavior_keyword_in_behavior_spec_case1883
public static final BitSet FOLLOW_generic_spec_case_in_behavior_spec_case1891
public static final BitSet FOLLOW_normal_behavior_keyword_in_normal_behavior_spec_case1947
public static final BitSet FOLLOW_generic_spec_case_in_normal_behavior_spec_case1955
public static final BitSet FOLLOW_model_behavior_keyword_in_model_behavior_spec_case2010
public static final BitSet FOLLOW_generic_spec_case_in_model_behavior_spec_case2018
public static final BitSet FOLLOW_exceptional_behavior_keyword_in_exceptional_behavior_spec_case2077
public static final BitSet FOLLOW_generic_spec_case_in_exceptional_behavior_spec_case2085
public static final BitSet FOLLOW_spec_var_decls_in_generic_spec_case2148
public static final BitSet FOLLOW_spec_header_in_generic_spec_case2160
public static final BitSet FOLLOW_free_spec_header_in_generic_spec_case2171
public static final BitSet FOLLOW_generic_spec_body_in_generic_spec_case2204
public static final BitSet FOLLOW_generic_spec_body_in_generic_spec_case2230
public static final BitSet FOLLOW_old_clause_in_spec_var_decls2276
public static final BitSet FOLLOW_FORALL_in_spec_var_decls2311
public static final BitSet FOLLOW_expression_in_spec_var_decls2315
public static final BitSet FOLLOW_requires_clause_in_spec_header2372
public static final BitSet FOLLOW_requires_free_clause_in_free_spec_header2426
public static final BitSet FOLLOW_requires_keyword_in_requires_clause2470
public static final BitSet FOLLOW_expression_in_requires_clause2474
public static final BitSet FOLLOW_REQUIRES_FREE_in_requires_free_clause2541
public static final BitSet FOLLOW_expression_in_requires_free_clause2545
public static final BitSet FOLLOW_simple_spec_body_in_generic_spec_body2584
public static final BitSet FOLLOW_NEST_START_in_generic_spec_body2605
public static final BitSet FOLLOW_generic_spec_case_seq_in_generic_spec_body2614
public static final BitSet FOLLOW_NEST_END_in_generic_spec_body2622
public static final BitSet FOLLOW_generic_spec_case_in_generic_spec_case_seq2665
public static final BitSet FOLLOW_also_keyword_in_generic_spec_case_seq2683
public static final BitSet FOLLOW_generic_spec_case_in_generic_spec_case_seq2697
public static final BitSet FOLLOW_simple_spec_body_clause_in_simple_spec_body2763
public static final BitSet FOLLOW_assignable_clause_in_simple_spec_body_clause2805
public static final BitSet FOLLOW_accessible_clause_in_simple_spec_body_clause2820
public static final BitSet FOLLOW_ensures_clause_in_simple_spec_body_clause2835
public static final BitSet FOLLOW_ensures_free_clause_in_simple_spec_body_clause2853
public static final BitSet FOLLOW_signals_clause_in_simple_spec_body_clause2866
public static final BitSet FOLLOW_joinproc_clause_in_simple_spec_body_clause2886
public static final BitSet FOLLOW_signals_only_clause_in_simple_spec_body_clause2904
public static final BitSet FOLLOW_diverges_clause_in_simple_spec_body_clause2917
public static final BitSet FOLLOW_measured_by_clause_in_simple_spec_body_clause2934
public static final BitSet FOLLOW_name_clause_in_simple_spec_body_clause2948
public static final BitSet FOLLOW_captures_clause_in_simple_spec_body_clause2967
public static final BitSet FOLLOW_when_clause_in_simple_spec_body_clause2974
public static final BitSet FOLLOW_working_space_clause_in_simple_spec_body_clause2981
public static final BitSet FOLLOW_duration_clause_in_simple_spec_body_clause2988
public static final BitSet FOLLOW_breaks_clause_in_simple_spec_body_clause2997
public static final BitSet FOLLOW_continues_clause_in_simple_spec_body_clause3016
public static final BitSet FOLLOW_returns_clause_in_simple_spec_body_clause3032
public static final BitSet FOLLOW_separates_clause_in_simple_spec_body_clause3057
public static final BitSet FOLLOW_determines_clause_in_simple_spec_body_clause3080
public static final BitSet FOLLOW_separates_keyword_in_separates_clause3140
public static final BitSet FOLLOW_expression_in_separates_clause3144
public static final BitSet FOLLOW_determines_keyword_in_determines_clause3208
public static final BitSet FOLLOW_expression_in_determines_clause3212
public static final BitSet FOLLOW_DETERMINES_in_determines_keyword3232
public static final BitSet FOLLOW_assignable_keyword_in_assignable_clause3266
public static final BitSet FOLLOW_expression_in_assignable_clause3270
public static final BitSet FOLLOW_accessible_keyword_in_accessible_clause3367
public static final BitSet FOLLOW_expression_in_accessible_clause3371
public static final BitSet FOLLOW_measured_by_keyword_in_measured_by_clause3436
public static final BitSet FOLLOW_expression_in_measured_by_clause3440
public static final BitSet FOLLOW_ensures_keyword_in_ensures_clause3504
public static final BitSet FOLLOW_expression_in_ensures_clause3508
public static final BitSet FOLLOW_ENSURES_FREE_in_ensures_free_clause3567
public static final BitSet FOLLOW_expression_in_ensures_free_clause3571
public static final BitSet FOLLOW_signals_keyword_in_signals_clause3607
public static final BitSet FOLLOW_expression_in_signals_clause3611
public static final BitSet FOLLOW_signals_only_keyword_in_signals_only_clause3688
public static final BitSet FOLLOW_expression_in_signals_only_clause3692
public static final BitSet FOLLOW_diverges_keyword_in_diverges_clause3749
public static final BitSet FOLLOW_expression_in_diverges_clause3753
public static final BitSet FOLLOW_captures_keyword_in_captures_clause3792
public static final BitSet FOLLOW_expression_in_captures_clause3796
public static final BitSet FOLLOW_SPEC_NAME_in_name_clause3849
public static final BitSet FOLLOW_STRING_LITERAL_in_name_clause3853
public static final BitSet FOLLOW_SEMICOLON_in_name_clause3855
public static final BitSet FOLLOW_when_keyword_in_when_clause3879
public static final BitSet FOLLOW_expression_in_when_clause3883
public static final BitSet FOLLOW_working_space_keyword_in_working_space_clause3928
public static final BitSet FOLLOW_expression_in_working_space_clause3932
public static final BitSet FOLLOW_duration_keyword_in_duration_clause3977
public static final BitSet FOLLOW_expression_in_duration_clause3981
public static final BitSet FOLLOW_OLD_in_old_clause4028
public static final BitSet FOLLOW_modifiers_in_old_clause4032
public static final BitSet FOLLOW_type_in_old_clause4037
public static final BitSet FOLLOW_IDENT_in_old_clause4042
public static final BitSet FOLLOW_INITIALISER_in_old_clause4047
public static final BitSet FOLLOW_IDENT_in_type4079
public static final BitSet FOLLOW_EMPTYBRACKETS_in_type4090
public static final BitSet FOLLOW_type_in_field_or_method_declaration4115
public static final BitSet FOLLOW_IDENT_in_field_or_method_declaration4120
public static final BitSet FOLLOW_method_declaration_in_field_or_method_declaration4139
public static final BitSet FOLLOW_field_declaration_in_field_or_method_declaration4162
public static final BitSet FOLLOW_EMPTYBRACKETS_in_field_declaration4204
public static final BitSet FOLLOW_initialiser_in_field_declaration4223
public static final BitSet FOLLOW_SEMICOLON_in_field_declaration4235
public static final BitSet FOLLOW_param_list_in_method_declaration4284
public static final BitSet FOLLOW_BODY_in_method_declaration4303
public static final BitSet FOLLOW_SEMICOLON_in_method_declaration4320
public static final BitSet FOLLOW_LPAREN_in_param_list4369
public static final BitSet FOLLOW_param_decl_in_param_list4397
public static final BitSet FOLLOW_COMMA_in_param_list4433
public static final BitSet FOLLOW_param_decl_in_param_list4453
public static final BitSet FOLLOW_RPAREN_in_param_list4509
public static final BitSet FOLLOW_set_in_param_decl4567
public static final BitSet FOLLOW_IDENT_in_param_decl4611
public static final BitSet FOLLOW_AXIOM_NAME_BEGIN_in_param_decl4645
public static final BitSet FOLLOW_AXION_NAME_END_in_param_decl4660
public static final BitSet FOLLOW_EMPTYBRACKETS_in_param_decl4675
public static final BitSet FOLLOW_IDENT_in_param_decl4718
public static final BitSet FOLLOW_represents_keyword_in_represents_clause4762
public static final BitSet FOLLOW_expression_in_represents_clause4766
public static final BitSet FOLLOW_accessible_keyword_in_depends_clause4830
public static final BitSet FOLLOW_expression_in_depends_clause4834
public static final BitSet FOLLOW_constraint_keyword_in_history_constraint4870
public static final BitSet FOLLOW_expression_in_history_constraint4874
public static final BitSet FOLLOW_MONITORS_FOR_in_monitors_for_clause4934
public static final BitSet FOLLOW_expression_in_monitors_for_clause4938
public static final BitSet FOLLOW_READABLE_in_readable_if_clause4969
public static final BitSet FOLLOW_expression_in_readable_if_clause4973
public static final BitSet FOLLOW_WRITABLE_in_writable_if_clause5004
public static final BitSet FOLLOW_expression_in_writable_if_clause5008
public static final BitSet FOLLOW_in_group_clause_in_datagroup_clause5039
public static final BitSet FOLLOW_maps_into_clause_in_datagroup_clause5043
public static final BitSet FOLLOW_in_keyword_in_in_group_clause5062
public static final BitSet FOLLOW_expression_in_in_group_clause5066
public static final BitSet FOLLOW_maps_keyword_in_maps_into_clause5110
public static final BitSet FOLLOW_expression_in_maps_into_clause5114
public static final BitSet FOLLOW_NOWARN_in_nowarn_pragma5165
public static final BitSet FOLLOW_expression_in_nowarn_pragma5169
public static final BitSet FOLLOW_DEBUG_in_debug_statement5202
public static final BitSet FOLLOW_expression_in_debug_statement5206
public static final BitSet FOLLOW_SET_in_set_statement5236
public static final BitSet FOLLOW_expression_in_set_statement5240
public static final BitSet FOLLOW_loop_invariant_in_loop_specification5283
public static final BitSet FOLLOW_loop_invariant_in_loop_specification5328
public static final BitSet FOLLOW_loop_separates_clause_in_loop_specification5352
public static final BitSet FOLLOW_loop_determines_clause_in_loop_specification5375
public static final BitSet FOLLOW_assignable_clause_in_loop_specification5398
public static final BitSet FOLLOW_variant_function_in_loop_specification5419
public static final BitSet FOLLOW_maintaining_keyword_in_loop_invariant5460
public static final BitSet FOLLOW_expression_in_loop_invariant5464
public static final BitSet FOLLOW_decreasing_keyword_in_variant_function5541
public static final BitSet FOLLOW_expression_in_variant_function5545
public static final BitSet FOLLOW_separates_keyword_in_loop_separates_clause5630
public static final BitSet FOLLOW_expression_in_loop_separates_clause5634
public static final BitSet FOLLOW_determines_keyword_in_loop_determines_clause5670
public static final BitSet FOLLOW_expression_in_loop_determines_clause5674
public static final BitSet FOLLOW_assume_keyword_in_assume_statement5707
public static final BitSet FOLLOW_expression_in_assume_statement5711
public static final BitSet FOLLOW_LPAREN_in_expression5791
public static final BitSet FOLLOW_RPAREN_in_expression5809
public static final BitSet FOLLOW_SEMICOLON_in_expression5829
public static final BitSet FOLLOW_set_in_expression5845
public static final BitSet FOLLOW_SEMICOLON_in_expression5893
public static final BitSet FOLLOW_EQUALITY_in_initialiser5926
public static final BitSet FOLLOW_expression_in_initialiser5930
public static final BitSet FOLLOW_method_specification_in_block_specification5978
public static final BitSet FOLLOW_assert_keyword_in_assert_statement6004
public static final BitSet FOLLOW_expression_in_assert_statement6008
public static final BitSet FOLLOW_UNREACHABLE_in_assert_statement6026
public static final BitSet FOLLOW_SEMICOLON_in_assert_statement6028
public static final BitSet FOLLOW_breaks_keyword_in_breaks_clause6083
public static final BitSet FOLLOW_expression_in_breaks_clause6087
public static final BitSet FOLLOW_BREAKS_in_breaks_keyword6100
public static final BitSet FOLLOW_continues_keyword_in_continues_clause6131
public static final BitSet FOLLOW_expression_in_continues_clause6135
public static final BitSet FOLLOW_CONTINUES_in_continues_keyword6148
public static final BitSet FOLLOW_returns_keyword_in_returns_clause6179
public static final BitSet FOLLOW_expression_in_returns_clause6183
public static final BitSet FOLLOW_RETURNS_in_returns_keyword6196
public static final BitSet FOLLOW_joinproc_keyword_in_joinproc_clause6232
public static final BitSet FOLLOW_expression_in_joinproc_clause6236
public static final BitSet FOLLOW_JOIN_PROC_in_joinproc_keyword6251
public static final BitSet FOLLOW_break_behavior_keyword_in_break_behavior_spec_case6286
public static final BitSet FOLLOW_generic_spec_case_in_break_behavior_spec_case6294
public static final BitSet FOLLOW_continue_behavior_keyword_in_continue_behavior_spec_case6349
public static final BitSet FOLLOW_generic_spec_case_in_continue_behavior_spec_case6357
public static final BitSet FOLLOW_return_behavior_keyword_in_return_behavior_spec_case6412
public static final BitSet FOLLOW_generic_spec_case_in_return_behavior_spec_case6420
public static final BitSet FOLLOW_accessible_keyword_in_synpred1_KeYJMLPreParser216
public static final BitSet FOLLOW_expression_in_synpred1_KeYJMLPreParser218
public static final BitSet FOLLOW_LPAREN_in_synpred2_KeYJMLPreParser4130
public KeYJMLPreParser(TokenStream input)
public KeYJMLPreParser(TokenStream input, RecognizerSharedState state)
private KeYJMLPreParser(KeYJMLPreLexer lexer, String fileName, Position offsetPos)
public Parser[] getDelegates()
public String[] getTokenNames()
getTokenNames
in class BaseRecognizer
public String getGrammarFileName()
getGrammarFileName
in class BaseRecognizer
private PositionedString createPositionedString(String text, Token t)
private PositionedString createPositionedString(String text, Position pos)
private void raiseError(String msg) throws SLTranslationException
SLTranslationException
private void raiseNotSupported(String feature) throws SLTranslationException
SLTranslationException
public ImmutableList<TextualJMLConstruct> parseClasslevelComment() throws SLTranslationException
SLTranslationException
public ImmutableList<TextualJMLConstruct> parseMethodlevelComment() throws SLTranslationException
SLTranslationException
public ImmutableSet<PositionedString> getWarnings()
private PositionedString flipHeaps(String declString, PositionedString result)
private PositionedString flipHeaps(String declString, PositionedString result, boolean allowPreHeaps)
protected Object recoverFromMismatchedToken(IntStream input, int ttype, BitSet follow) throws RecognitionException
recoverFromMismatchedToken
in class BaseRecognizer
RecognitionException
public Object recoverFromMismatchedSet(IntStream input, RecognitionException e, BitSet follow) throws RecognitionException
recoverFromMismatchedSet
in class BaseRecognizer
RecognitionException
public final ImmutableList<TextualJMLConstruct> classlevel_comment() throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> classlevel_element(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> methodlevel_comment() throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> methodlevel_element(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<String> modifiers() throws SLTranslationException, RecognitionException
public final String modifier() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> class_invariant(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final String axiom_name() throws SLTranslationException, RecognitionException
public final void invariant_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> class_axiom(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> initially_clause(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> method_specification(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void also_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> lightweight_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> heavyweight_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> behavior_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void behavior_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> normal_behavior_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void normal_behavior_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> model_behavior_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void model_behavior_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> exceptional_behavior_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void exceptional_behavior_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> generic_spec_case(ImmutableList<String> mods, Behavior b) throws SLTranslationException, RecognitionException
public final ImmutableList<PositionedString[]> spec_var_decls() throws SLTranslationException, RecognitionException
public final ImmutableList<PositionedString> spec_header() throws SLTranslationException, RecognitionException
public final ImmutableList<PositionedString> free_spec_header() throws SLTranslationException, RecognitionException
public final PositionedString requires_clause() throws SLTranslationException, RecognitionException
public final void requires_keyword() throws RecognitionException
RecognitionException
public final PositionedString requires_free_clause() throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> generic_spec_body(ImmutableList<String> mods, Behavior b, ImmutableList<TextualJMLConstruct> specs) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> generic_spec_case_seq(ImmutableList<String> mods, Behavior b, ImmutableList<TextualJMLConstruct> specs) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> simple_spec_body(ImmutableList<String> mods, Behavior b) throws SLTranslationException, RecognitionException
public final void simple_spec_body_clause(TextualJMLSpecCase sc, Behavior b) throws SLTranslationException, RecognitionException
public final PositionedString separates_clause() throws SLTranslationException, RecognitionException
public final void separates_keyword() throws RecognitionException
RecognitionException
public final PositionedString determines_clause() throws SLTranslationException, RecognitionException
public final void determines_keyword() throws RecognitionException
RecognitionException
public final PositionedString assignable_clause() throws SLTranslationException, RecognitionException
public final void assignable_keyword() throws RecognitionException
RecognitionException
public final PositionedString accessible_clause() throws SLTranslationException, RecognitionException
public final void accessible_keyword() throws RecognitionException
RecognitionException
public final PositionedString measured_by_clause() throws SLTranslationException, RecognitionException
public final void measured_by_keyword() throws RecognitionException
RecognitionException
public final PositionedString ensures_clause() throws SLTranslationException, RecognitionException
public final void ensures_keyword() throws RecognitionException
RecognitionException
public final PositionedString ensures_free_clause() throws SLTranslationException, RecognitionException
public final PositionedString signals_clause() throws SLTranslationException, RecognitionException
public final void signals_keyword() throws RecognitionException
RecognitionException
public final PositionedString signals_only_clause() throws SLTranslationException, RecognitionException
public final void signals_only_keyword() throws RecognitionException
RecognitionException
public final PositionedString diverges_clause() throws SLTranslationException, RecognitionException
public final void diverges_keyword() throws RecognitionException
RecognitionException
public final void captures_clause() throws SLTranslationException, RecognitionException
public final void captures_keyword() throws RecognitionException
RecognitionException
public final PositionedString name_clause() throws SLTranslationException, RecognitionException
public final void when_clause() throws SLTranslationException, RecognitionException
public final void when_keyword() throws RecognitionException
RecognitionException
public final void working_space_clause() throws SLTranslationException, RecognitionException
public final void working_space_keyword() throws RecognitionException
RecognitionException
public final void duration_clause() throws SLTranslationException, RecognitionException
public final void duration_keyword() throws RecognitionException
RecognitionException
public final PositionedString[] old_clause() throws SLTranslationException, RecognitionException
public final PositionedString type() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> field_or_method_declaration(ImmutableList<String> mods) throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> field_declaration(ImmutableList<String> mods, PositionedString type, Token name) throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> method_declaration(ImmutableList<String> mods, PositionedString type, Token name) throws RecognitionException
RecognitionException
public final String param_list() throws RecognitionException
RecognitionException
public final String param_decl() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> represents_clause(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void represents_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> depends_clause(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> history_constraint(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void constraint_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> monitors_for_clause(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> readable_if_clause(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> writable_if_clause(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> datagroup_clause(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void in_group_clause() throws SLTranslationException, RecognitionException
public final void in_keyword() throws RecognitionException
RecognitionException
public final void maps_into_clause() throws SLTranslationException, RecognitionException
public final void maps_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> nowarn_pragma(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> debug_statement(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> set_statement(ImmutableList<String> mods) throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> loop_specification(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final PositionedString loop_invariant() throws RecognitionException
RecognitionException
public final void maintaining_keyword() throws RecognitionException
RecognitionException
public final PositionedString variant_function() throws RecognitionException
RecognitionException
public final void decreasing_keyword() throws RecognitionException
RecognitionException
public final PositionedString loop_separates_clause() throws SLTranslationException, RecognitionException
public final PositionedString loop_determines_clause() throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> assume_statement(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void assume_keyword() throws RecognitionException
RecognitionException
public final PositionedString expression() throws RecognitionException
RecognitionException
public final String initialiser() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> block_specification(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final ImmutableList<TextualJMLConstruct> assert_statement(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void assert_keyword() throws RecognitionException
RecognitionException
public final PositionedString breaks_clause() throws SLTranslationException, RecognitionException
public final void breaks_keyword() throws RecognitionException
RecognitionException
public final PositionedString continues_clause() throws SLTranslationException, RecognitionException
public final void continues_keyword() throws RecognitionException
RecognitionException
public final PositionedString returns_clause() throws SLTranslationException, RecognitionException
public final void returns_keyword() throws RecognitionException
RecognitionException
public final PositionedString joinproc_clause() throws SLTranslationException, RecognitionException
public final void joinproc_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> break_behavior_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void break_behavior_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> continue_behavior_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void continue_behavior_keyword() throws RecognitionException
RecognitionException
public final ImmutableList<TextualJMLConstruct> return_behavior_spec_case(ImmutableList<String> mods) throws SLTranslationException, RecognitionException
public final void return_behavior_keyword() throws RecognitionException
RecognitionException
public final void synpred1_KeYJMLPreParser_fragment() throws RecognitionException
RecognitionException
public final void synpred2_KeYJMLPreParser_fragment() throws RecognitionException
RecognitionException
public final boolean synpred2_KeYJMLPreParser()
public final boolean synpred1_KeYJMLPreParser()