Commit 77fe1031 authored by Mattias Ulbrich's avatar Mattias Ulbrich
Browse files

Merge branch 'weigl/fix1566' into 'master'

Fix #1566

Closes #1566

See merge request key/key!367
parents bee2f7f5 728a5202
......@@ -380,7 +380,7 @@ atom_prefix:
| bracket_term
;
bracket_term: primitive_labeled_term (bracket_suffix_heap)* attribute*;
bracket_suffix_heap: brace_suffix (AT heap=term)?;
bracket_suffix_heap: brace_suffix (AT heap=bracket_term)?;
brace_suffix:
LBRACKET target=term ASSIGN val=term RBRACKET #bracket_access_heap_update
| LBRACKET id=simple_ident args=argument_list RBRACKET #bracket_access_heap_term
......@@ -465,9 +465,9 @@ accessterm
attribute:
DOT STAR #attribute_star
| DOT id=simple_ident call? (AT heap=term)? #attribute_simple
| DOT id=simple_ident call? (AT heap=bracket_term)? #attribute_simple
| DOT LPAREN sort=sortId DOUBLECOLON id=simple_ident RPAREN
call? (AT heap=term)? #attribute_complex
call? (AT heap=bracket_term)? #attribute_complex
;
call:
......
......@@ -15,6 +15,7 @@ import de.uka.ilkd.key.nparser.KeYParser;
import de.uka.ilkd.key.parser.NotDeclException;
import de.uka.ilkd.key.pp.AbbrevMap;
import de.uka.ilkd.key.util.Debug;
import org.antlr.v4.runtime.Parser;
import org.antlr.v4.runtime.ParserRuleContext;
import org.antlr.v4.runtime.Token;
import javax.annotation.Nullable;
......@@ -332,7 +333,7 @@ public class ExpressionBuilder extends DefaultBuilder {
Term t = accept(ctx.primitive_labeled_term());
for (int i = 0; i < ctx.bracket_suffix_heap().size(); i++) {
KeYParser.Brace_suffixContext brace_suffix = ctx.bracket_suffix_heap(i).brace_suffix();
KeYParser.TermContext heap = ctx.bracket_suffix_heap(i).heap;
ParserRuleContext heap = ctx.bracket_suffix_heap(i).heap;
t = accept(brace_suffix, t);
if (heap != null) {
t = replaceHeap(t, accept(heap), heap);
......@@ -1262,7 +1263,7 @@ public class ExpressionBuilder extends DefaultBuilder {
if (attrib instanceof KeYParser.Attribute_simpleContext) {
KeYParser.Attribute_simpleContext simpleContext = (KeYParser.Attribute_simpleContext) attrib;
boolean isCall = simpleContext.call() != null;
KeYParser.TermContext heap = simpleContext.heap; //TODO?
ParserRuleContext heap = simpleContext.heap; //TODO?
String attributeName = accept(simpleContext.id);
ProgramVariable maybeAttr = getJavaInfo().getAttribute(attributeName, kjt);
if (maybeAttr != null) {
......
......@@ -13,13 +13,18 @@
package de.uka.ilkd.key.parser;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.nparser.KeyAst;
import de.uka.ilkd.key.nparser.KeyIO;
import de.uka.ilkd.key.nparser.ParsingFacade;
import de.uka.ilkd.key.proof.init.Includes;
import de.uka.ilkd.key.proof.init.ProblemInitializer;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.proof.io.RuleSourceFactory;
import de.uka.ilkd.key.rule.TacletForTests;
import de.uka.ilkd.key.util.HelperClassForTests;
import org.antlr.runtime.RecognitionException;
import org.antlr.v4.runtime.CharStreams;
import org.junit.Assert;
......@@ -73,4 +78,11 @@ public class TestParser {
loader.parseFile().loadComplete();
loader.loadProblem();
}
@Test
public void testIssue1566() throws ProblemLoaderException {
File file = new File(HelperClassForTests.TESTCASE_DIRECTORY, "issues/1566/a.key");
KeYEnvironment<DefaultUserInterfaceControl> env = KeYEnvironment.load(file);
}
}
\ No newline at end of file
https://git.key-project.org/key/key/-/issues/1566
## Description
Amongst others, the term `o.f@heap + 1` is parsed incorrectly
## Reproducible
always
### Steps to reproduce
Create A.java:
````
class A { int f; }
````
Create a.key (in same directory):
````
\javaSource ".";
\programVariables { A that; }
\problem { that.f@heap + 1 = 1 + that.f@heap }
````
Load it. KeY fails.
This file can be loaded into %"v2.8.0" however.
### Additional information
Another problem is that the error message is pretty broken and does not allow to browse the guilty source code:
`Could not build term on: heap+1/tmp/k/a.key:6:18`
---
* Commit: bee2f7f582f39c914b5f11725aa1eb115233fde8, master at the time
\ No newline at end of file
\javaSource ".";
\programVariables { A that; }
\problem { that.f@heap + 1 = 1 + that.f@heap }
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment