From 55f5e5b2f6382c40ca5a9cc8440cc5c6b283946f Mon Sep 17 00:00:00 2001
From: Daniel Plagge <plagge@cs.uni-duesseldorf.de>
Date: Tue, 11 Mar 2014 11:28:04 +0100
Subject: [PATCH] Bugfix in translation: In case of quantified expressions or
predicates, a superfluous bound variable name was put on the stack, resulting
in wrong resolving of bound variables.
---
.../prob/eventb/translator/internal/TranslationVisitor.java | 6 ++----
1 file changed, 2 insertions(+), 4 deletions(-)
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java b/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java
index 87d6fb7f..36eb4f7f 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java
@@ -616,10 +616,8 @@ public class TranslationVisitor implements ISimpleVisitor {
// I've encountered null types. Maybe that was a bug but just to be
// sure (in most cases, missing type information won't hurt):
if (type != null) {
- // put a translation of the identifier on the stack ...
- decl.accept(this);
- // ... and take it
- final PExpression expr = expressions.pop();
+ final PExpression expr = createIdentifierExpression(decl
+ .getName());
// construct "expr:type"
final PPredicate member = new AMemberPredicate(expr,
translateType(type));
--
GitLab