name clash when declaring a local variable twice

[wadoon]

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

---

• Mantis: MT-1129
• Submitted on: 2011-11-07 by (at)grahl
• Updated: 2011-11-17

Description

Java allows you to declare local variables more than once, e.g. in a for-loop. KeY's parser does not like that and will tell you the following: java.lang.RuntimeException: Name already in namespace: i at de.uka.ilkd.key.logic.Namespace.addSafely(Namespace.java:117) at de.uka.ilkd.key.speclang.translation.SLResolverManager.putIntoTopLocalVariablesNamespace(SLResolverManager.java:245) at de.uka.ilkd.key.speclang.translation.SLResolverManager.putIntoTopLocalVariablesNamespace(SLResolverManager.java:274) at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.(KeYJMLParser.java:110) at de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser.(KeYJMLParser.java:139) at de.uka.ilkd.key.speclang.jml.translation.JMLTranslator.translate(JMLTranslator.java:966) at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.createJMLLoopInvariant(JMLSpecFactory.java:913)

Steps to reproduce

Try to prove this:

 //@ ensures true;
  public void foo(){
    //@ maintaining true;
    for (int i= 0; i < 1; i++);
    //@ maintaining true;
    for (int i= 0; i < 1; i++);
}

Files

Notes

(at)scheben at 2011-11-17

This problem is harder to solve than I thought at a first glance. The bug is in the method which constructs an invariant out of an jml-loop-invariant statement. The method collects all variables which are locally declared in the method-body and tries to put them into the namespace without taking care of scopes. As a bug-fix one would have to extract and to add only those variables which are visible in the block where the loop is declared. Since this is no mayor bug but would cost some time to fix, I decided not to fix it in the near future (by myself).

History

• (at)grahl -- (NEW_BUG) 2011-11-07

• (at)scheben -- (NORMAL_TYPE) 2011-11-07

• (at)scheben -- (NORMAL_TYPE) 2011-11-07

• (at)scheben -- (BUGNOTE_ADDED) 2011-11-17

• (at)scheben -- (NORMAL_TYPE) 2011-11-17

• (at)grahl -- (NORMAL_TYPE) 2011-11-17

• (at)grahl -- (NORMAL_TYPE) 2011-11-17

• (at)grahl -- (NORMAL_TYPE) 2011-11-17

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

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

Attributes

• Category: Parser
• Status: NEW
• Severity: MINOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: LOW
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build:
• Tags []
• Labels: ~KeY Parser ~Bug ~LOW

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:59:12.212Z
• updated_at: 2021-12-11T15:27:02.924Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0