summaryrefslogtreecommitdiff
path: root/Source/VCExpr
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-07-11 10:31:41 -0700
committerGravatar wuestholz <unknown>2013-07-11 10:31:41 -0700
commit37505e4e1c58753012f5694cc27e337934fb9451 (patch)
treed0d47f98a0efa3fd4a92aa5f39ebfb43cb2dfd74 /Source/VCExpr
parent035abd7ec2a774c8a721f7c39d58224fdcd123e2 (diff)
Worked on the parallelization.
Diffstat (limited to 'Source/VCExpr')
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs75
1 files changed, 41 insertions, 34 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);
+ }
}
}
}