diff options
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 75 | ||||
| -rw-r--r-- | Source/VCExpr/NameClashResolver.cs | 18 |
2 files changed, 54 insertions, 39 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 2ff93c54..cac6d95b 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1125,43 +1125,50 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Assert(app.Func != null); // resolution must have happened
- if (app.Func.doingExpansion) {
- System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
- return null;
- }
+ lock (app.Func)
+ {
+ if (app.Func.doingExpansion)
+ {
+ System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
+ return null;
+ }
- var exp = app.Func.Body;
- if (exp == null)
- return null;
+ var exp = app.Func.Body;
+ if (exp == null)
+ return null;
- VCExpr/*!*/ translatedBody;
- VCExprSubstitution/*!*/ subst = new VCExprSubstitution();
- try {
- BaseTranslator.PushFormalsScope();
- BaseTranslator.PushBoundVariableScope();
- app.Func.doingExpansion = true;
-
- // first bind the formals to VCExpr variables, which are later
- // substituted with the actual parameters
- var inParams = app.Func.InParams;
- for (int i = 0; i < inParams.Length; ++i)
- subst[BaseTranslator.BindVariable(inParams[i])] = args[i];
-
- // recursively translate the body of the expansion
- translatedBody = BaseTranslator.Translate(exp);
- } finally {
- BaseTranslator.PopFormalsScope();
- BaseTranslator.PopBoundVariableScope();
- app.Func.doingExpansion = false;
- }
+ VCExpr/*!*/ translatedBody;
+ VCExprSubstitution/*!*/ subst = new VCExprSubstitution();
+ try
+ {
+ BaseTranslator.PushFormalsScope();
+ BaseTranslator.PushBoundVariableScope();
+ app.Func.doingExpansion = true;
+
+ // first bind the formals to VCExpr variables, which are later
+ // substituted with the actual parameters
+ var inParams = app.Func.InParams;
+ for (int i = 0; i < inParams.Length; ++i)
+ subst[BaseTranslator.BindVariable(inParams[i])] = args[i];
+
+ // recursively translate the body of the expansion
+ translatedBody = BaseTranslator.Translate(exp);
+ }
+ finally
+ {
+ BaseTranslator.PopFormalsScope();
+ BaseTranslator.PopBoundVariableScope();
+ app.Func.doingExpansion = false;
+ }
- // substitute the formals with the actual parameters in the body
- var tparms = app.Func.TypeParameters;
- Contract.Assert(typeArgs.Count == tparms.Length);
- for (int i = 0; i < typeArgs.Count; ++i)
- subst[tparms[i]] = typeArgs[i];
- SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
- return substituter.Mutate(translatedBody, subst);
+ // substitute the formals with the actual parameters in the body
+ var tparms = app.Func.TypeParameters;
+ Contract.Assert(typeArgs.Count == tparms.Length);
+ for (int i = 0; i < typeArgs.Count; ++i)
+ subst[tparms[i]] = typeArgs[i];
+ SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
+ return substituter.Mutate(translatedBody, subst);
+ }
}
}
}
diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs index a78a6103..a46105f8 100644 --- a/Source/VCExpr/NameClashResolver.cs +++ b/Source/VCExpr/NameClashResolver.cs @@ -33,15 +33,13 @@ namespace Microsoft.Boogie.VCExprAST { private UniqueNamer(UniqueNamer namer) {
Contract.Requires(namer != null);
+
Spacer = namer.Spacer;
GlobalNames = new Dictionary<Object, string>(namer.GlobalNames);
-
- List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ localNames =
- new List<IDictionary<Object, string>>();
- LocalNames = localNames;
+ LocalNames = new List<IDictionary<Object, string>>();
foreach (IDictionary<Object/*!*/, string/*!*/>/*!*/ d in namer.LocalNames)
- localNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));
+ LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));
UsedNames = new HashSet<string>(namer.UsedNames);
CurrentCounters = new Dictionary<string, int>(namer.CurrentCounters);
@@ -53,6 +51,16 @@ namespace Microsoft.Boogie.VCExprAST { return new UniqueNamer(this);
}
+ public void Reset()
+ {
+ GlobalNames.Clear();
+ LocalNames.Clear();
+ LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>());
+ UsedNames.Clear();
+ CurrentCounters.Clear();
+ GlobalPlusLocalNames.Clear();
+ }
+
////////////////////////////////////////////////////////////////////////////
private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalNames;
|