Method parameter ending with _0 can not be parsed

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

• Mantis: MT-1358

• Submitted on: 2013-08-14 by (at)greiner

• Updated: 2015-01-16

• Assigned to: (at)kamburjan

Description

If a parameter name ends with _0 and the parameter is used in some form in the method contract, the parameter is claimed to be unknown by KeY.

If the parameter with name "para_0" is referred to as "para" in the JML specification , the problem loads without a problem.

The Problem already existed on the official KeY 2.0.1 Version

Steps to reproduce

Load the attached java file.

Additional Information

Stack trace:

(class de.uka.ilkd.key.proof.io.ProblemLoaderException)
de.uka.ilkd.key.proof.io.ProblemLoaderException: Expression para_0 cannot be resolved.
	at de.uka.ilkd.key.proof.io.DefaultProblemLoader.load(DefaultProblemLoader.java:166)
	at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:90)
	at de.uka.ilkd.key.proof.io.ProblemLoader.access$000(ProblemLoader.java:39)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.construct(ProblemLoader.java:64)
	at de.uka.ilkd.key.gui.SwingWorker$2.run(SwingWorker.java:122)
	at java.lang.Thread.run(Thread.java:722)
Caused by: Expression para_0 cannot be resolved.
	at de.uka.ilkd.key.speclang.translation.SLTranslationExceptionManager.createException(SLTranslationExceptionManager.java:110)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.raiseError(KeYJMLParser.java:150)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.postfixexpr(KeYJMLParser.java:2954)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.unaryexprnotplusminus(KeYJMLParser.java:3366)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.unaryexpr(KeYJMLParser.java:3229)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.multexpr(KeYJMLParser.java:3088)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.additiveexpr(KeYJMLParser.java:3042)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.shiftexpr(KeYJMLParser.java:2860)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.relationalexpr(KeYJMLParser.java:2648)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.equalityexpr(KeYJMLParser.java:2581)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.andexpr(KeYJMLParser.java:2511)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.exclusiveorexpr(KeYJMLParser.java:2449)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.inclusiveorexpr(KeYJMLParser.java:2390)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.logicalandexpr(KeYJMLParser.java:2336)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.logicalorexpr(KeYJMLParser.java:2232)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.impliesexpr(KeYJMLParser.java:2156)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.equivalenceexpr(KeYJMLParser.java:2108)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.conditionalexpr(KeYJMLParser.java:2057)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.assignmentexpr(KeYJMLParser.java:2046)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.expression(KeYJMLParser.java:1559)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.predicate(KeYJMLParser.java:1543)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.predornot(KeYJMLParser.java:1642)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.requiresclause(KeYJMLParser.java:1167)
	at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.top(KeYJMLParser.java:406)
	at de.uka.ilkd.key.speclang.jml.translation.JMLTranslator.translate(JMLTranslator.java:1570)
	at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.translateAndClauses(JMLSpecFactory.java:373)
	at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.translateJMLClauses(JMLSpecFactory.java:265)
	at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.createJMLOperationContracts(JMLSpecFactory.java:1072)
	at de.uka.ilkd.key.speclang.jml.JMLSpecExtractor.extractMethodSpecs(JMLSpecExtractor.java:485)
	at de.uka.ilkd.key.speclang.SLEnvInput.createSpecs(SLEnvInput.java:343)
	at de.uka.ilkd.key.speclang.SLEnvInput.read(SLEnvInput.java:376)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:350)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:532)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:481)
	at de.uka.ilkd.key.proof.io.DefaultProblemLoader.createInitConfig(DefaultProblemLoader.java:233)
	at de.uka.ilkd.key.proof.io.DefaultProblemLoader.load(DefaultProblemLoader.java:139)

Files

History

• (at)greiner -- (NEW_BUG) 2013-08-14

• (at)rbubel -- (NORMAL_TYPE) 2013-10-17

• (at)rbubel -- (NORMAL_TYPE) 2013-10-17

• (at)grahl -- (NORMAL_TYPE) 2013-11-25

• (at)grahl -- (NORMAL_TYPE) 2014-01-03

• (at)grahl -- (NORMAL_TYPE) 2014-01-03

• (at)grahl -- (NORMAL_TYPE) 2014-10-06

• (at)grahl -- (NORMAL_TYPE) 2015-01-16

Attributes

• Category: Parser
• Status: ASSIGNED
• Severity: MINOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: e787c364f9ce97b7b2dc26dc4d706af7aaae70bf
• Build:
• Tags []
• Labels: ~KeY Parser ~Bug ~NORMAL
• Version: 2.0.2

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:35:05.780Z
• updated_at: 2017-05-29T02:35:06.016Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0