Skip to content

Commit

Permalink
Fix some tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@jwiesler
jwiesler committed Mar 11, 2023
1 parent 693e6e5 commit 17d3786
Show file tree
Hide file tree
Showing 7 changed files with 28 additions and 42 deletions.
31 changes: 16 additions & 15 deletions key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -188,6 +188,10 @@ private IdDeclaration parseIdDeclaration(String s) throws ParserException {
return new IdDeclaration(ctx.id.getText(), sort);
}

private static Position createPosition(int irow) {
return new Position(irow + 1, 1);
}

/**
* throws an exception iff no input in indicated row, and no metavariable instantiation is
* possible
Expand All @@ -200,8 +204,7 @@ private void checkNeededInputAvailable(int irow) throws MissingInstantiationExce

if ((getValueAt(irow, icol) == null || ((String) getValueAt(irow, icol)).length() == 0)
&& !originalApp.complete()) {
throw new MissingInstantiationException("" + getValueAt(irow, 0), new Position(irow, 1),
false);
throw new MissingInstantiationException("" + getValueAt(irow, 0), createPosition(irow), false);
}
}

Expand All @@ -227,7 +230,7 @@ private Term parseRow(int irow, Namespace<QuantifiableVariable> varNS,
String instantiation = (String) getValueAt(irow, 1);

if (instantiation == null || "".equals(instantiation)) {
throw new MissingInstantiationException("", new Position(irow, 1), false);
throw new MissingInstantiationException("", createPosition(irow), false);
}

try {
Expand Down Expand Up @@ -257,7 +260,7 @@ private IdDeclaration parseIdDeclaration(int irow)
String instantiation = (String) getValueAt(irow, 1);

if (instantiation == null || "".equals(instantiation)) {
throw new MissingInstantiationException("", new Position(irow, 1), false);
throw new MissingInstantiationException("", createPosition(irow), false);
}

try {
Expand All @@ -268,7 +271,7 @@ private IdDeclaration parseIdDeclaration(int irow)
throw new SVInstantiationParserException(instantiation,
loc.getPosition().offsetLine(irow), pe.getMessage(), false).initCause(pe);
} else {
throw new SVInstantiationParserException(instantiation, new Position(irow, 1),
throw new SVInstantiationParserException(instantiation, createPosition(irow),
pe.getMessage(), false).initCause(pe);
}
}
Expand Down Expand Up @@ -308,13 +311,13 @@ private ProgramElement parseRow(int irow) throws SVInstantiationParserException

if (!varNamer.isUniqueNameForSchemaVariable(instantiation, sv,
originalApp.posInOccurrence(), prefix)) {
throw new SVInstantiationParserException(instantiation, new Position(irow, 1),
throw new SVInstantiationParserException(instantiation, createPosition(irow),
"Name is already in use.", false);
}

ProgramElement pe = originalApp.getProgramElement(instantiation, sv, services);
if (pe == null) {
throw new SVInstantiationParserException(instantiation, new Position(irow, 1),
throw new SVInstantiationParserException(instantiation, createPosition(irow),
"Unexpected sort: " + sv.sort() + "." + "Label SV or a program variable SV expected"
+ " declared as new.",
false);
Expand Down Expand Up @@ -347,7 +350,7 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException {
try {
sort = result.getRealSort(sv, services);
} catch (SortException e) {
throw new MissingSortException("" + sv, new Position(irow, 1));
throw new MissingSortException("" + sv, createPosition(irow));
}
}

Expand All @@ -363,7 +366,7 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException {
services);
} else {
throw new SVInstantiationParserException(idd.getName(),
new Position(irow, 1),
createPosition(irow),
"Name already in use.", false);
}
}
Expand All @@ -375,9 +378,7 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException {
SchemaVariable problemVarSV = result.varSVNameConflict();

if (problemVarSV != null) {
throw new SVInstantiationParserException("",
new Position(getSVRow(problemVarSV), 1),
"Ambiguous instantiation of schema variable " + problemVarSV, false);
throw new SVInstantiationParserException("", createPosition(getSVRow(problemVarSV)), "Ambiguous instantiation of schema variable " + problemVarSV, false);
}

for (irow = noEditRow + 1; irow < entries.size(); irow++) {
Expand Down Expand Up @@ -413,16 +414,16 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException {
result = result.addCheckedInstantiation(sv, addOrigin(instance),
services, true);
} catch (RigidnessException e) {
throw new SVRigidnessException("" + sv, new Position(irow, 1));
throw new SVRigidnessException("" + sv, createPosition(irow));
} catch (IllegalInstantiationException iae) {
throw new SVInstantiationParserException((String) getValueAt(irow, 1),
new Position(irow, 1), iae.getMessage(), false);
createPosition(irow), iae.getMessage(), false);
}
}
}
}
} catch (SortException e) {
throw new SortMismatchException("" + sv, sort, new Position(irow, 1));
throw new SortMismatchException("" + sv, sort, createPosition(irow));
}

return result;
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/java/Position.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ public static Position fromPosition(SourceElement.Position pos) {
if (pos == SourceElement.Position.UNDEFINED) {
return UNDEFINED;
} else {
return new Position(pos.getLine(), pos.getColumn() + 1);
return new Position(pos.getLine() + 1, pos.getColumn() + 1);
}
}

Expand Down
24 changes: 6 additions & 18 deletions key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,40 +8,28 @@
import de.uka.ilkd.key.java.abstraction.PrimitiveType;
import de.uka.ilkd.key.java.abstraction.Type;
import de.uka.ilkd.key.java.expression.Literal;
import de.uka.ilkd.key.java.expression.literal.CharLiteral;
import de.uka.ilkd.key.java.expression.literal.DoubleLiteral;
import de.uka.ilkd.key.java.expression.literal.FloatLiteral;
import de.uka.ilkd.key.java.expression.literal.IntLiteral;
import de.uka.ilkd.key.java.expression.literal.LongLiteral;
import de.uka.ilkd.key.java.expression.literal.StringLiteral;
import de.uka.ilkd.key.java.expression.literal.*;
import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
import de.uka.ilkd.key.ldt.*;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.*;
import de.uka.ilkd.key.logic.sort.ArraySort;
import de.uka.ilkd.key.logic.sort.Sort;
import de.uka.ilkd.key.nparser.KeyIO;
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.parser.ParserException;
import de.uka.ilkd.key.proof.OpReplacer;
import de.uka.ilkd.key.speclang.ClassAxiom;
import de.uka.ilkd.key.speclang.HeapContext;
import de.uka.ilkd.key.speclang.PositionedString;
import de.uka.ilkd.key.speclang.jml.translation.JMLResolverManager;
import de.uka.ilkd.key.speclang.njml.JmlParser.PrimaryFloatingPointContext;
import de.uka.ilkd.key.speclang.njml.OverloadedOperatorHandler.JMLOperator;
import de.uka.ilkd.key.speclang.translation.*;
import de.uka.ilkd.key.speclang.translation.SLExceptionFactory;
import de.uka.ilkd.key.speclang.translation.SLExpression;
import de.uka.ilkd.key.speclang.translation.SLParameters;
import de.uka.ilkd.key.speclang.translation.SLTranslationException;
import de.uka.ilkd.key.util.InfFlowSpec;
import de.uka.ilkd.key.util.Pair;
import de.uka.ilkd.key.util.mergerule.MergeParamsSpec;
import de.uka.ilkd.key.util.parsing.BuildingException;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.ParserRuleContext;
import org.antlr.v4.runtime.Token;
import org.antlr.v4.runtime.tree.TerminalNode;
Expand Down Expand Up @@ -105,7 +93,7 @@ class Translator extends JmlParserBaseVisitor<Object> {
this.heapLDT = services.getTypeConverter().getHeapLDT();
this.locSetLDT = services.getTypeConverter().getLocSetLDT();
this.booleanLDT = services.getTypeConverter().getBooleanLDT();
this.exc = new SLExceptionFactory("", 0, 0);
this.exc = new SLExceptionFactory("", 1, 0);

this.selfVar = self;
this.paramVars = paramVars;
Expand Down
6 changes: 1 addition & 5 deletions key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLExceptionFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,11 @@

import de.uka.ilkd.key.java.Position;
import de.uka.ilkd.key.speclang.PositionedString;
import de.uka.ilkd.key.util.Debug;
import org.antlr.runtime.*;
import org.antlr.v4.runtime.ParserRuleContext;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
import recoder.service.KeYCrossReferenceSourceInfo;

import javax.annotation.Nonnull;

import java.util.LinkedList;
import java.util.List;

Expand Down Expand Up @@ -71,7 +67,7 @@ public SLExceptionFactory updatePosition(org.antlr.v4.runtime.Token start) {
// -------------------------------------------------------------------------
private Position createAbsolutePosition(int relativeLine, int relativeColumn) {
int absoluteLine = offsetLine + relativeLine - 1;
int absoluteColumn = (relativeLine == 1 ? offsetColumn : 1) + relativeColumn - 1;
int absoluteColumn = (relativeLine == 1 ? offsetColumn : 1) + relativeColumn;
return Position.newOneZeroBased(absoluteLine, absoluteColumn);
}

Expand Down
3 changes: 2 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,8 @@ public BuildingException(@Nullable Token t, String message, Throwable e) {

private static String getPosition(Token t) {
if (t != null) {
return t.getTokenSource().getSourceName() + ":" + Position.fromToken(t);
var p = Position.fromToken(t);
return t.getTokenSource().getSourceName() + ":" + p.getLine() + ":" + p.getColumn();
} else
return "";
}
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/test/java/de/uka/ilkd/key/rule/tacletbuilder/TestTacletBuild.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ public void testSchemavariablesInAddrulesRespectPrefix() {
helper.parseThrowException(
new File(testRules + File.separator + "schemaVarInAddruleRespectPrefix.key"));
} catch (BuildingException e) {
assertTrue(e.toString().contains("schemaVarInAddruleRespectPrefix.key:9:2"),
assertTrue(e.toString().contains("schemaVarInAddruleRespectPrefix.key:9:3"),
"Position of error message is wrong.");
assertTrue(e.getCause().getMessage().contains(
"Schema variable b (formula)occurs at different places in taclet all_left_hide with different prefixes."),
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/test/java/de/uka/ilkd/key/speclang/njml/NJmlTranslatorTests.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ public void testWarnRequires() {
PositionedString message = warnings.head();
assertEquals(
"Diverging Semantics form JML Reference: Requires does not initiate a new contract. "
+ "See https://www.key-project.org/docs/user/JMLGrammar/#TODO (Test.java, 5/37)",
+ "See https://www.key-project.org/docs/user/JMLGrammar/#TODO (Test.java, 5/38)",
message.toString());
}

Expand Down

0 comments on commit 17d3786

Please sign in to comment.