diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index a8594d8bbf..92f9f6b7d7 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -66,14 +66,14 @@ PUBLIC: 'public'; PURE: 'pure'; RETURN_BEHAVIOR: 'return_' BEHAVIOR; FINAL: 'final'; -MODEL: 'model'/* -> pushMode(expr)*/; +MODEL: 'model'/* */; fragment Pred: '_redundantly'?; //suffix fragment Pfree: '_free'?; //suffix -ACCESSIBLE: 'accessible' Pred -> pushMode(expr); -ASSERT: 'assert' Pred -> pushMode(expr); -ASSUME: 'assume' Pred -> pushMode(expr); +ACCESSIBLE: 'accessible' Pred; +ASSERT: 'assert' Pred; +ASSUME: 'assume' Pred; /** * The name 'assignable' is kept here for legacy reasons. * Note that KeY does only verify what can be modified (i.e., what is 'modifiable'). @@ -81,7 +81,7 @@ ASSUME: 'assume' Pred -> pushMode(expr); ASSIGNABLE : ('assignable' | 'assigns' | 'assigning' | 'modifiable' | 'modifies' | 'modifying' | - 'writable' | 'writes' | 'writing') (Pfree|Pred) -> pushMode(expr); + 'writable' | 'writes' | 'writing') (Pfree|Pred); /** * The name 'assignable' is kept here for legacy reasons. * Note that KeY does only verify what can be modified (i.e., what is 'modifiable'). @@ -89,82 +89,59 @@ ASSIGNABLE LOOP_ASSIGNABLE : ('loop_assignable' | 'loop_assigns' | 'loop_assigning' | 'loop_modifiable' | 'loop_modifies' | 'loop_modifying' | - 'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred) -> pushMode(expr); -AXIOM: 'axiom' -> pushMode(expr); -BREAKS: 'breaks' -> pushMode(expr); -CAPTURES: 'captures' Pred -> pushMode(expr); + 'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred); +AXIOM: 'axiom'; +BREAKS: 'breaks'; +CAPTURES: 'captures' Pred; CODE: 'code'; //? -CONSTRAINT: 'constraint' Pred -> pushMode(expr); -CONTINUES: 'continues' -> pushMode(expr); +CONSTRAINT: 'constraint' Pred; +CONTINUES: 'continues'; DEBUG: 'debug'; //? -DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr); -DETERMINES: 'determines' -> pushMode(expr); -DIVERGES: 'diverges' Pred -> pushMode(expr); -//DURATION: 'duration' Pred -> pushMode(expr); -ENSURES: ('ensures' | 'post') (Pfree|Pred) -> pushMode(expr); -FOR_EXAMPLE: 'for_example' -> pushMode(expr); -//FORALL: 'forall' -> pushMode(expr); //? +DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred; +DETERMINES: 'determines'; +DIVERGES: 'diverges' Pred; +//DURATION: 'duration' Pred; +ENSURES: ('ensures' | 'post') (Pfree|Pred); +FOR_EXAMPLE: 'for_example'; +//FORALL: 'forall'; //? HELPER: 'helper'; -IMPLIES_THAT: 'implies_that' -> pushMode(expr); -IN: 'in' Pred -> pushMode(expr); -INITIALLY: 'initially' -> pushMode(expr); +IMPLIES_THAT: 'implies_that'; +IN: 'in' Pred; +INITIALLY: 'initially'; INSTANCE: 'instance'; -INVARIANT: 'invariant' (Pfree|Pred) -> pushMode(expr); +INVARIANT: 'invariant' (Pfree|Pred); LOOP_CONTRACT: 'loop_contract'; -LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred) -> pushMode(expr); +LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred); LOOP_DETERMINES: 'loop_determines'; // internal translation for 'determines' in loop invariants LOOP_SEPARATES: 'loop_separates'; //KeY extension, deprecated -MAPS: 'maps' Pred -> pushMode(expr); -MEASURED_BY: 'measured_by' Pred -> pushMode(expr); +MAPS: 'maps' Pred; +MEASURED_BY: 'measured_by' Pred; MERGE_POINT: 'merge_point'; MERGE_PROC: 'merge_proc'; -MERGE_PARAMS: 'merge_params' -> pushMode(expr); -MONITORED: 'monitored' -> pushMode(expr); -MONITORS_FOR: 'monitors_for' -> pushMode(expr); -//OLD: 'old' -> pushMode(expr); -//POST: 'post'Pred -> pushMode(expr); -//PRE: 'pre' Pred -> pushMode(expr); +MERGE_PARAMS: 'merge_params'; +MONITORED: 'monitored'; +MONITORS_FOR: 'monitors_for'; READABLE: 'readable'; -REPRESENTS: 'represents' Pred -> pushMode(expr); -REQUIRES: ('requires'| 'pre') (Pfree|Pred) -> pushMode(expr); -RETURN: 'return' -> pushMode(expr); -RETURNS: 'returns' -> pushMode(expr); -RESPECTS: 'respects' -> pushMode(expr); -SEPARATES: 'separates' -> pushMode(expr); -SET: 'set' -> pushMode(expr); -SIGNALS: ('signals' Pred | 'exsures' Pred) -> pushMode(expr); -SIGNALS_ONLY: 'signals_only' Pred -> pushMode(expr); -WHEN: 'when' Pred -> pushMode(expr); -WORKING_SPACE: 'working_space' Pred -> pushMode(expr); -WRITABLE: 'writable' -> pushMode(expr); - +REPRESENTS: 'represents' Pred; +REQUIRES: ('requires'| 'pre') (Pfree|Pred); +RETURN: 'return'; +RETURNS: 'returns'; +RESPECTS: 'respects'; +SEPARATES: 'separates'; +SET: 'set'; +SIGNALS: ('signals' Pred | 'exsures' Pred); +SIGNALS_ONLY: 'signals_only' Pred; +WHEN: 'when' Pred; +WORKING_SPACE: 'working_space' Pred; +WRITABLE: 'writable'; JML_ML_END: '*/' -> channel(HIDDEN); WS: (' ' | '\t' | '\n' | '\r' | '@')+ -> channel(HIDDEN); NEST_START: '{|' ; NEST_END: '|}' ; -C_RBRACKET: ']' -> type(RBRACKET); -C_LBRACKET: '[' -> type(LBRACKET); -SEMICOLON : ';' -> type(SEMI_TOPLEVEL); -C_LBRACE: '{' -> type(LBRACE); -C_RBRACE: '}' -> type(RBRACE); -C_EQUAL: '=' -> type(EQUAL_SINGLE), pushMode(expr); -C_LPAREN: '(' -> type(LPAREN); -C_RPAREN: ')' -> type(RPAREN); C_STRING_LITERAL: '"' -> pushMode(string), more; -C_IDENT: '\\'? LETTER (LETTERORDIGIT)* -> type(IDENT); -C_COLON: ':' -> type(COLON); -C_DOT: '.' -> type(DOT); -C_COMMA: ',' -> type(COMMA); - -SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> channel(HIDDEN); -ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment); - -JML_SL_START: {!jmlMarkerDecision.isComment("//")}? '//' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN); -JML_ML_START: {!jmlMarkerDecision.isComment("/*")}?'/*' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN); - -ERROR_CHAR: .; - -mode expr; +COLON: ':'; +DOT: '.'; +COMMA: ','; /* Java keywords */ BOOLEAN: 'boolean'; @@ -181,33 +158,8 @@ THIS: 'this'; TRUE: 'true'; VOID: 'void'; -E_NULLABLE: 'nullable'->type(NULLABLE); -E_NONNULL: 'non_null' -> type(NON_NULL); - - DEPENDS: 'depends'; // internal translation for 'accessible' on model fields -/* JML and JML* keywords */ -/*ACCESSIBLE: 'accessible'; -MODIFIABLE: 'modifiable'; -BREAKS: 'breaks'; -CONTINUES: 'continues'; -DECREASES: 'decreases'; // internal translation for 'measured_by' -DETERMINES: 'determines'; //KeY extension, not official JML -ENSURES: 'ensures'; -ENSURES_FREE: 'ensures_free'; -MODEL_METHOD_AXIOM: 'model_method_axiom'; //KeY extension, not official JML -MERGE_PARAMS: 'merge_params'; //KeY extension, not official JML -NON_NULL: 'non_null'; -NULLABLE: 'nullable'; -REPRESENTS: 'represents'; -REQUIRES: 'requires'; -REQUIRES_FREE: 'requires_free'; -RETURNS: 'returns'; //KeY extension, not official JML -SEPARATES: 'separates'; //KeY extension, not official JML -SIGNALS: 'signals'; -SIGNALS_ONLY: 'signals_only';*/ - /* JML keywords prefixed with a backslash */ ALLFIELDS: '\\all_fields'; //KeY extension, not official JML ALLOBJECTS: '\\all_objects'; //KeY extension, not official JML @@ -320,22 +272,24 @@ WORKINGSPACE: '\\working_space'; // ONLY_CALLED: '\\only_called'; // ONLY_CAPTURED: '\\only_captured'; +SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> channel(HIDDEN); +ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment); + +JML_SL_START: {!jmlMarkerDecision.isComment("//")}? '//' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN); +JML_ML_START: {!jmlMarkerDecision.isComment("/*")}?'/*' ([+-] [a-zA-Z_0-9]*)* '@' -> channel(HIDDEN); + E_JML_SL_START: '//@' -> type(JML_SL_START), channel(HIDDEN); E_JML_ML_START: '/*@' -> type(JML_ML_START), channel(HIDDEN); -E_JML_ML_END: '*/' -> channel(HIDDEN); E_SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> type(COMMENT), channel(HIDDEN); E_ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment); AND: '&'; BITWISENOT: '~'; -COLON: ':'; -COMMA: ','; DIV: '/'; -DOT: '.'; DOTDOT: '..'; -EQUAL_SINGLE: '='; EQV_ANTIV: '<==>' | '<=!=>'; EQ_NEQ: '==' | '!='; +EQUAL_SINGLE: '='; GEQ: '>='; IMPLIES: '==>'; IMPLIESBACKWARD: '<=='; @@ -368,8 +322,7 @@ LBRACE: '{' {incrBrace();}; RBRACE: '}' {decrBrace();}; LBRACKET: '[' {incrBracket();}; RBRACKET: ']' {decrBracket();}; -SEMI_TOPLEVEL: { semicolonOnToplevel()}? ';' -> popMode; //jump back to contract mode -SEMI: { ! semicolonOnToplevel()}? ';'; +SEMI: ';'; fragment LETTER: 'a'..'z' | 'A'..'Z' | '_' | '$'; @@ -486,7 +439,7 @@ INFORMAL_DESCRIPTION: '(*' ( '*' ~')' | ~'*' )* '*)'; DOC_COMMENT: '/**' -> pushMode(mlComment); fragment PRAGMA: '\\nowarn'; -E_ERROR_CHAR: . -> type(ERROR_CHAR); +ERROR_CHAR: .; mode mlComment; ML_COMMENT_END: ('*/'|EOF) -> type(COMMENT), channel(HIDDEN), popMode; diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index 40f27ec6ac..725c3a233c 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -16,17 +16,17 @@ classlevel_comments: classlevel_comment* EOF; classlevel_comment: classlevel_element | modifiers | set_statement; classlevel_element0: modifiers? (classlevel_element modifiers?); classlevel_element - : class_invariant /*| depends_clause*/ | method_specification - | method_declaration | field_declaration | represents_clause - | history_constraint | initially_clause | class_axiom - | monitors_for_clause | readable_if_clause | writable_if_clause - | datagroup_clause | set_statement | nowarn_pragma - | accessible_clause | assert_statement | assume_statement + : class_invariant | set_statement | field_declaration + | method_specification | method_declaration | represents_clause + | history_constraint | initially_clause | class_axiom + | monitors_for_clause | readable_if_clause | writable_if_clause + | datagroup_clause | nowarn_pragma | accessible_clause + | assert_statement | assume_statement ; methodlevel_comment: (modifiers? methodlevel_element modifiers?)* EOF; methodlevel_element - : field_declaration | set_statement | merge_point_statement + : set_statement | field_declaration | merge_point_statement | loop_specification | assert_statement | assume_statement | nowarn_pragma | debug_statement | block_specification | block_loop_specification | assert_statement | assume_statement @@ -43,9 +43,9 @@ modifier -class_axiom: AXIOM expression SEMI_TOPLEVEL; -initially_clause: INITIALLY expression SEMI_TOPLEVEL; -class_invariant: INVARIANT expression SEMI_TOPLEVEL; +class_axiom: AXIOM expression SEMI; +initially_clause: INITIALLY expression SEMI; +class_invariant: INVARIANT expression SEMI; //axiom_name: AXIOM_NAME_BEGIN IDENT AXIOM_NAME_END; method_specification: (also_keyword)* spec_case ((also_keyword)+ spec_case)*; also_keyword: (ALSO | FOR_EXAMPLE | IMPLIES_THAT); @@ -73,32 +73,32 @@ clause // clauses targetHeap : SPECIAL_IDENT+; -ensures_clause: ENSURES targetHeap? predornot SEMI_TOPLEVEL; -requires_clause: REQUIRES targetHeap? predornot SEMI_TOPLEVEL; -measured_by_clause: MEASURED_BY predornot (COMMA predornot)* SEMI_TOPLEVEL; -captures_clause: CAPTURES predornot SEMI_TOPLEVEL; -diverges_clause: DIVERGES predornot SEMI_TOPLEVEL; -working_space_clause: WORKING_SPACE predornot SEMI_TOPLEVEL; -duration_clause: DURATION predornot SEMI_TOPLEVEL; -when_clause: WHEN predornot SEMI_TOPLEVEL; +ensures_clause: ENSURES targetHeap? predornot SEMI; +requires_clause: REQUIRES targetHeap? predornot SEMI; +measured_by_clause: MEASURED_BY predornot (COMMA predornot)* SEMI; +captures_clause: CAPTURES predornot SEMI; +diverges_clause: DIVERGES predornot SEMI; +working_space_clause: WORKING_SPACE predornot SEMI; +duration_clause: DURATION predornot SEMI; +when_clause: WHEN predornot SEMI; accessible_clause : ACCESSIBLE targetHeap? (lhs=expression COLON)? rhs=storeRefUnion (MEASURED_BY mby=expression)? - SEMI_TOPLEVEL; + SEMI; /** * The name 'assignable' is kept here for legacy reasons. * Note that KeY does only verify what can be modified (i.e., what is 'modifiable'). */ -assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI; //depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ; //decreases_clause: DECREASES termexpression (COMMA termexpression)*; represents_clause : REPRESENTS lhs=expression (((LARROW|EQUAL_SINGLE) (rhs=expression|t=storeRefUnion)) | (SUCH_THAT predicate)) - SEMI_TOPLEVEL + SEMI ; separates_clause @@ -108,14 +108,14 @@ separates_clause | ERASES erase+=infflowspeclist | NEW_OBJECTS newobj+=infflowspeclist )* - SEMI_TOPLEVEL + SEMI ; loop_separates_clause : LOOP_SEPARATES sep=infflowspeclist (NEW_OBJECTS newobj+=infflowspeclist)* - SEMI_TOPLEVEL + SEMI ; infflowspeclist @@ -131,7 +131,7 @@ determines_clause | ERASES erases+=infflowspeclist | NEW_OBJECTS newObs+=infflowspeclist )* - SEMI_TOPLEVEL + SEMI ; loop_determines_clause @@ -139,21 +139,21 @@ loop_determines_clause det=infflowspeclist BY ITSELF (NEW_OBJECTS newObs+=infflowspeclist)* - SEMI_TOPLEVEL + SEMI ; -signals_clause: SIGNALS LPAREN referencetype (IDENT)? RPAREN (predornot)? SEMI_TOPLEVEL; -signals_only_clause: SIGNALS_ONLY (NOTHING |referencetype (COMMA referencetype)*) SEMI_TOPLEVEL; -breaks_clause: BREAKS LPAREN (lbl=IDENT)? RPAREN (predornot)? SEMI_TOPLEVEL; -continues_clause: CONTINUES LPAREN (lbl=IDENT)? RPAREN (predornot)? SEMI_TOPLEVEL; -returns_clause: RETURNS predornot? SEMI_TOPLEVEL; +signals_clause: SIGNALS LPAREN referencetype (IDENT)? RPAREN (predornot)? SEMI; +signals_only_clause: SIGNALS_ONLY (NOTHING |referencetype (COMMA referencetype)*) SEMI; +breaks_clause: BREAKS LPAREN (lbl=IDENT)? RPAREN (predornot)? SEMI; +continues_clause: CONTINUES LPAREN (lbl=IDENT)? RPAREN (predornot)? SEMI; +returns_clause: RETURNS predornot? SEMI; -name_clause: SPEC_NAME STRING_LITERAL SEMICOLON ; +name_clause: SPEC_NAME STRING_LITERAL SEMI ; //old_clause: OLD modifiers type IDENT INITIALISER ; -field_declaration: typespec IDENT (LBRACKET RBRACKET)* initialiser? SEMI_TOPLEVEL; -method_declaration: typespec IDENT param_list (method_body|SEMI_TOPLEVEL); -method_body: LBRACE RETURN expression SEMI_TOPLEVEL RBRACE; +field_declaration: typespec IDENT (LBRACKET RBRACKET)* initialiser? SEMI; +method_declaration: typespec IDENT param_list (method_body|SEMI); +method_body: LBRACE RETURN expression SEMI RBRACE; param_list: LPAREN (param_decl (COMMA param_decl)*)? RPAREN; param_decl: ((NON_NULL | NULLABLE))? typespec p=IDENT (LBRACKET RBRACKET)*; history_constraint: CONSTRAINT expression; @@ -165,12 +165,12 @@ in_group_clause: IN expression; maps_into_clause: MAPS expression; nowarn_pragma: NOWARN expression; debug_statement: DEBUG expression; -set_statement: SET (assignee=expression) EQUAL_SINGLE (value=expression) SEMI_TOPLEVEL; +set_statement: SET (assignee=expression) EQUAL_SINGLE (value=expression) SEMI; merge_point_statement: MERGE_POINT (MERGE_PROC (proc=STRING_LITERAL))? (mergeparamsspec)? - SEMI_TOPLEVEL + SEMI ; loop_specification : loop_invariant @@ -181,22 +181,22 @@ loop_specification | loop_assignable_clause | variant_function)*; -loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL; +loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI; /** * The name 'assignable' is kept here for legacy reasons. * Note that KeY does only verify what can be modified (i.e., what is 'modifiable'). */ -loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; -variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL; +loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI; +variant_function: DECREASING expression (COMMA expression)* SEMI; //loop_separates_clause: SEPARATES expression; //loop_determines_clause: DETERMINES expression; -assume_statement: ASSUME expression SEMI_TOPLEVEL; +assume_statement: ASSUME expression SEMI; initialiser: EQUAL_SINGLE expression; block_specification: method_specification; block_loop_specification: loop_contract_keyword spec_case ((also_keyword)+ loop_contract_keyword spec_case)*; loop_contract_keyword: LOOP_CONTRACT; -assert_statement: (ASSERT expression | UNREACHABLE) SEMI_TOPLEVEL; +assert_statement: (ASSERT expression | UNREACHABLE) SEMI; //breaks_clause: BREAKS expression; //continues_clause: CONTINUES expression; //returns_clause: RETURNS expression; @@ -279,7 +279,93 @@ primaryexpr | array_initializer ; this_: THIS; -ident: IDENT | JML_IDENT | SPECIAL_IDENT | THIS | SUPER; + +ident: + IDENT + | ACCESSIBLE + | ALSO + | ASSERT + | ASSIGNABLE + | ASSUME + | BEHAVIOR + | BREAK_BEHAVIOR + | BREAKS + | CAPTURES + | CODE + | CODE_BIGINT_MATH + | CODE_JAVA_MATH + | CODE_SAFE_MATH + | CONST + | CONSTRAINT + | CONTINUE_BEHAVIOR + | CONTINUES + | DEBUG + | DEPENDS + | DETERMINES + | DIVERGES + | ENSURES + | EXCEPTIONAL_BEHAVIOUR + | FOR_EXAMPLE + | GHOST + | HELPER + | IMPLIES_THAT + | IN + | INITIALLY + | INSTANCE + | INVARIANT + | JML_IDENT + | LOOP_ASSIGNABLE + | LOOP_CONTRACT + | LOOP_DETERMINES + | LOOP_INVARIANT + | LOOP_SEPARATES + | MAPS + | MEASURED_BY + | MERGE_PARAMS + | MERGE_POINT + | MERGE_PROC + | MODEL + | MONITORED + | MONITORS_FOR + | NO_STATE + | NON_NULL + | NORMAL_BEHAVIOR + | NOWARN + | NULLABLE + | NULLABLE_BY_DEFAULT + | PURE + | READABLE + | REPRESENTS + | REQUIRES + | RESPECTS + | RETURN_BEHAVIOR + | RETURNS + | SEPARATES + | SET + | SIGNALS + | SIGNALS_ONLY + | SPEC_BIGINT_MATH + | SPEC_JAVA_MATH + | SPEC_NAME + | SPEC_PROTECTED + | SPEC_PUBLIC + | SPEC_SAFE_MATH + | SPECIAL_IDENT + | STRICTFP + | STRICTLY_PURE + | SUPER + | THIS + | TWO_STATE + | UNINITIALIZED + | UNREACHABLE + | WHEN + | WORKING_SPACE + | WRITABLE + | AXIOM + | DECREASING + | MODEL_BEHAVIOUR + ; + inv:INV; inv_free:INV_FREE; true_:TRUE; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java index 80b93be0ce..0e9923e3c5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java @@ -78,7 +78,6 @@ public static ParserRuleContext parseExpr(String expr) { } private static ParserRuleContext getExpressionContext(JmlLexer lexer) { - lexer._mode = JmlLexer.expr; JmlParser parser = createParser(lexer); JmlParser.ExpressionEOFContext ctx = parser.expressionEOF(); ParserRuleContext c; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java index 6664f1069e..f6fa3355a9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java @@ -453,7 +453,9 @@ public Object visitClass_axiom(JmlParser.Class_axiomContext ctx) { @Override public Object visitField_declaration(JmlParser.Field_declarationContext ctx) { - assert !mods.isEmpty(); + if (mods.isEmpty()) { + raiseError(ctx, "Modifiers are empty."); + } TextualJMLFieldDecl inv = new TextualJMLFieldDecl(mods, ctx); constructs = constructs.append(inv); return null; diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java index 39259c2444..ac521773ec 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java @@ -57,25 +57,25 @@ public void testLexer1() { @Test public void testLexer2() { lex("ensures //-key@ this should be ignored\n" + "true;", ENSURES, WS, COMMENT, WS, TRUE, - SEMI_TOPLEVEL, EOF); + SEMI, EOF); } @Test public void testLexer3() { lex("ensures /*-key@ this should be ignored */ true;", ENSURES, WS, COMMENT, WS, TRUE, - SEMI_TOPLEVEL, EOF); + SEMI, EOF); } @Test public void testLexer4() { - lex("/*-openjml@ ensures true; */", JML_ML_START, WS, ENSURES, WS, TRUE, SEMI_TOPLEVEL, WS, + lex("/*-openjml@ ensures true; */", JML_ML_START, WS, ENSURES, WS, TRUE, SEMI, WS, JML_ML_END, EOF); } @Test public void testLexer5() { lex("/*@ pure */ /*@ ensures true;", JML_ML_START, WS, PURE, WS, JML_ML_END, WS, - JML_ML_START, WS, ENSURES, WS, TRUE, SEMI_TOPLEVEL, EOF); + JML_ML_START, WS, ENSURES, WS, TRUE, SEMI, EOF); } @Test @@ -143,7 +143,7 @@ public void testSimpleSpec() { Assertions.assertNotNull(constructs); Assertions.assertEquals(1, constructs.size()); - assertTrue(constructs.head() instanceof TextualJMLSpecCase); + assertInstanceOf(TextualJMLSpecCase.class, constructs.head()); TextualJMLSpecCase specCase = (TextualJMLSpecCase) constructs.head(); Assertions.assertSame(Behavior.NORMAL_BEHAVIOR, specCase.getBehavior()); @@ -172,7 +172,7 @@ public void testComplexSpec() { Assertions.assertNotNull(constructs); Assertions.assertEquals(1, constructs.size()); - assertTrue(constructs.head() instanceof TextualJMLSpecCase); + assertInstanceOf(TextualJMLSpecCase.class, constructs.head()); TextualJMLSpecCase specCase = (TextualJMLSpecCase) constructs.head(); Assertions.assertSame(Behavior.BEHAVIOR, specCase.getBehavior()); @@ -212,8 +212,8 @@ public void testMultipleSpecs() { Assertions.assertNotNull(constructs); Assertions.assertEquals(2, constructs.size()); - assertTrue(constructs.head() instanceof TextualJMLSpecCase); - assertTrue(constructs.tail().head() instanceof TextualJMLSpecCase); + assertInstanceOf(TextualJMLSpecCase.class, constructs.head()); + assertInstanceOf(TextualJMLSpecCase.class, constructs.tail().head()); TextualJMLSpecCase specCase1 = (TextualJMLSpecCase) constructs.head(); TextualJMLSpecCase specCase2 = (TextualJMLSpecCase) constructs.tail().head(); diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java index 1b403026ae..c9d77e3099 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java @@ -50,7 +50,6 @@ public void parseAndInterpret(String expr) { LocationVariable result = new LocationVariable(new ProgramElementName("result"), kjt); LocationVariable exc = new LocationVariable(new ProgramElementName("exc"), kjt); JmlLexer lexer = JmlFacade.createLexer(expr); - lexer._mode = JmlLexer.expr; JmlParser parser = new JmlParser(new CommonTokenStream(lexer)); JmlParser.ExpressionContext ctx = parser.expressionEOF().expression(); Assertions.assertEquals(0, parser.getNumberOfSyntaxErrors());