diff options
| author |  wuestholz <unknown> | 2013-07-11 10:31:41 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-11 10:31:41 -0700 |
| commit | 37505e4e1c58753012f5694cc27e337934fb9451 (patch) | |
| tree | d0d47f98a0efa3fd4a92aa5f39ebfb43cb2dfd74 /Source/VCExpr/Boogie2VCExpr.cs | |
| parent | 035abd7ec2a774c8a721f7c39d58224fdcd123e2 (diff) | |
Worked on the parallelization.
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 75 |
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);
+ }
}
}
}
|