diff options
| author |  MichalMoskal <unknown> | 2010-12-17 00:33:08 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-12-17 00:33:08 +0000 |
| commit | 12c28b0c769090a4d444cd31d7e871f707dd06a1 (patch) | |
| tree | 32c0dc67cde7c0a88cecacb53bc8dc5a7b3d3d69 | |
| parent | 063f42fc32048568db11fc24cbbe5a81f03f429f (diff) | |
Add functions generated in lambda-expansion of function body to top-level program declarations.
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 4 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
3 files changed, 7 insertions, 4 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) {
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index fcf556f0..a68e5699 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -484,8 +484,9 @@ namespace Microsoft.Boogie ErrorWriteLine("Fatal Error: ProverException: {0}", e);
return PipelineOutcome.FatalError;
}
-
- foreach ( Declaration decl in program.TopLevelDeclarations )
+
+ 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)
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index d4481bd5..18d4791f 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2270,7 +2270,7 @@ namespace VC { List<Expr> axioms;
List<Function> functions;
LambdaHelper.Desugar(impl, out axioms, out functions);
- // TODO: do something with functions (Z3 currently doesn't need them)
+ program.TopLevelDeclarations.AddRange(functions);
if (axioms.Count > 0) {
CmdSeq cmds = new CmdSeq();
|