summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-12-17 00:33:08 +0000
committerGravatar MichalMoskal <unknown>2010-12-17 00:33:08 +0000
commit12c28b0c769090a4d444cd31d7e871f707dd06a1 (patch)
tree32c0dc67cde7c0a88cecacb53bc8dc5a7b3d3d69 /Source/BoogieDriver
parent063f42fc32048568db11fc24cbbe5a81f03f429f (diff)
Add functions generated in lambda-expansion of function body to top-level program declarations.
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs4
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 98c1b9da..ab930f22 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -489,7 +489,9 @@ namespace Microsoft.Boogie {
return PipelineOutcome.FatalError;
}
- foreach (Declaration decl in program.TopLevelDeclarations) {
+ // operate on a stable copy, in case it gets updated while we're running
+ var decls = program.TopLevelDeclarations.ToArray();
+ foreach (Declaration decl in decls) {
Contract.Assert(decl != null);
Implementation impl = decl as Implementation;
if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {