Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLineOptions to separate the options that belong to these 3 tools.

5 files changed, 179 insertions, 50 deletions

diff --git a/Dafny/DafnyMain.cs b/Dafny/DafnyMain.cs
index 3f0b6e97..1d075415 100644
--- a/Dafny/DafnyMain.cs
+++ b/Dafny/DafnyMain.cs
@@ -49,8 +49,8 @@ namespace Microsoft.Dafny {
 

       program = new Program(programName, modules, builtIns);

 

-      if (Bpl.CommandLineOptions.Clo.DafnyPrintFile != null) {

-        string filename = Bpl.CommandLineOptions.Clo.DafnyPrintFile;

+      if (DafnyOptions.O.DafnyPrintFile != null) {

+        string filename = DafnyOptions.O.DafnyPrintFile;

         if (filename == "-") {

           Printer pr = new Printer(System.Console.Out);

           pr.PrintProgram(program);

diff --git a/Dafny/DafnyOptions.cs b/Dafny/DafnyOptions.cs
new file mode 100644
index 00000000..8c604b8a
--- /dev/null
+++ b/Dafny/DafnyOptions.cs
@@ -0,0 +1,132 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics.Contracts;

+using Bpl = Microsoft.Boogie;

+

+namespace Microsoft.Dafny

+{

+  public class DafnyOptions : Bpl.CommandLineOptions

+  {

+    public DafnyOptions()

+      : base("Dafny", "Dafny program verifier") {

+    }

+

+    private static DafnyOptions clo;

+    public static DafnyOptions O {

+      get { return clo; }

+    }

+

+    public static void Install(DafnyOptions options) {

+      Contract.Requires(options != null);

+      clo = options;

+      Bpl.CommandLineOptions.Install(options);

+    }

+

+    public bool DisallowSoundnessCheating = false;

+    public int Induction = 3;

+    public int InductionHeuristic = 6;

+    public string DafnyPrelude = null;

+    public string DafnyPrintFile = null;

+    public bool Compile = true;

+    public bool ForceCompile = false;

+

+    protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

+      Contract.Requires(name != null);

+      Contract.Requires(ps != null);

+      var args = ps.args;  // convenient synonym

+

+      switch (name) {

+        case "dprelude":

+          if (ps.ConfirmArgumentCount(1)) {

+            DafnyPrelude = args[ps.i];

+          }

+          return true;

+

+        case "dprint":

+          if (ps.ConfirmArgumentCount(1)) {

+            DafnyPrintFile = args[ps.i];

+          }

+          return true;

+

+        case "compile": {

+            int compile = 0;

+            if (ps.GetNumericArgument(ref compile, 3)) {

+              Compile = compile == 1 || compile == 2;

+              ForceCompile = compile == 2;

+            }

+            return true;

+          }

+

+        case "noCheating": {

+            int cheat = 0; // 0 is default, allows cheating

+            if (ps.GetNumericArgument(ref cheat, 2)) {

+              DisallowSoundnessCheating = cheat == 1;

+            }

+            return true;

+          }

+

+        case "induction":

+          ps.GetNumericArgument(ref Induction, 4);

+          return true;

+

+        case "inductionHeuristic":

+          ps.GetNumericArgument(ref InductionHeuristic, 7);

+          return true;

+

+        default:

+          break;

+      }

+      // not a Dafny-specific option, so defer to superclass

+      return base.ParseOption(name, ps);

+    }

+

+    protected override void ApplyDefaultOptions() {

+      base.ApplyDefaultOptions();

+

+      // expand macros in filenames, now that LogPrefix is fully determined

+      ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp);

+      ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp);

+    }

+

+    public override void AttributeUsage() {

+      // TODO: provide attribute help here

+    }

+

+    public override void Usage() {

+      Console.WriteLine(@"  ---- Dafny options ---------------------------------------------------------

+

+  Multiple .dfy files supplied on the command line are concatenated into one

+  Dafny program.

+

+  /dprelude:<file>

+                choose Dafny prelude file

+  /dprint:<file>

+                print Dafny program after parsing it

+                (use - as <file> to print to console)

+  /compile:<n>  0 - do not compile Dafny program

+                1 (default) - upon successful verification of the Dafny

+                    program, compile Dafny program to C# program out.cs

+                2 - always attempt to compile Dafny program to C# program

+                    out.cs, regardless of verification outcome

+  /noCheating:<n>

+                0 (default) - allow assume statements and free invariants

+                1 - treat all assumptions as asserts, and drop free.

+  /induction:<n>

+                0 - never do induction, not even when attributes request it

+                1 - only apply induction when attributes request it

+                2 - apply induction as requested (by attributes) and also

+                    for heuristically chosen quantifiers

+                3 (default) - apply induction as requested, and for

+                    heuristically chosen quantifiers and ghost methods

+  /inductionHeuristic:<n>

+                0 - least discriminating induction heuristic (that is, lean

+                    toward applying induction more often)

+                1,2,3,4,5 - levels in between, ordered as follows as far as

+                    how discriminating they are:  0 < 1 < 2 < (3,4) < 5 < 6

+                6 (default) - most discriminating

+");

+    }

+  }

+}

diff --git a/Dafny/DafnyPipeline.csproj b/Dafny/DafnyPipeline.csproj
index 40a8cacc..dfa9e503 100644
--- a/Dafny/DafnyPipeline.csproj
+++ b/Dafny/DafnyPipeline.csproj
@@ -154,6 +154,7 @@
     <Compile Include="Compiler.cs" />

     <Compile Include="DafnyAst.cs" />

     <Compile Include="DafnyMain.cs" />

+    <Compile Include="DafnyOptions.cs" />

     <Compile Include="Printer.cs" />

     <Compile Include="Resolver.cs" />

     <Compile Include="SccGraph.cs" />

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index f3373736..88f95f30 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -259,7 +259,7 @@ namespace Microsoft.Dafny {
     }

 

     static Bpl.Program ReadPrelude() {

-      string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude;

+      string preludePath = DafnyOptions.O.DafnyPrelude;

       if (preludePath == null)

       {

           //using (System.IO.Stream stream = cce.NonNull( System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource

@@ -1054,7 +1054,7 @@ namespace Microsoft.Dafny {
 

       Bpl.StmtList stmts;

       if (!wellformednessProc) {

-        if (3 <= CommandLineOptions.Clo.DafnyInduction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) {

+        if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) {

           var posts = new List<Expression>();

           m.Ens.ForEach(mfe => posts.Add(mfe.E));

           var allIns = new List<Formal>();

@@ -1805,7 +1805,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr gTotal = IsTotal(e.Guard, etran);

         Bpl.Expr g = etran.TrExpr(e.Guard);

         Bpl.Expr bTotal = IsTotal(e.Body, etran);

-        if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) {

+        if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {

           return BplAnd(gTotal, BplAnd(g, bTotal));

         } else {

           return BplAnd(gTotal, Bpl.Expr.Imp(g, bTotal));

@@ -1958,7 +1958,7 @@ namespace Microsoft.Dafny {
         var e = (PredicateExpr)expr;

         Bpl.Expr gCanCall = CanCallAssumption(e.Guard, etran);

         Bpl.Expr bCanCall = CanCallAssumption(e.Body, etran);

-        if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) {

+        if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {

           return BplAnd(gCanCall, bCanCall);

         } else {

           Bpl.Expr g = etran.TrExpr(e.Guard);

@@ -2369,7 +2369,7 @@ namespace Microsoft.Dafny {
       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         CheckWellformed(e.Guard, options, locals, builder, etran);

-        if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) {

+        if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {

           bool splitHappened;

           var ss = TrSplitExpr(e.Guard, etran, out splitHappened);

           if (!splitHappened) {

@@ -2843,7 +2843,7 @@ namespace Microsoft.Dafny {
       if (!wellformednessProc) {

         string comment = "user-defined preconditions";

         foreach (MaybeFreeExpression p in m.Req) {

-          if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {

+          if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));

           } else {

             bool splitHappened;  // we actually don't care

@@ -2856,7 +2856,7 @@ namespace Microsoft.Dafny {
         }

         comment = "user-defined postconditions";

         if (!skipEnsures) foreach (MaybeFreeExpression p in m.Ens) {

-          if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {

+          if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));

           } else {

             bool splitHappened;  // we actually don't care

@@ -3330,7 +3330,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(currentMethod != null && predef != null);

       if (stmt is PredicateStmt) {

-        if (stmt is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {

+        if (stmt is AssertStmt || DafnyOptions.O.DisallowSoundnessCheating) {

           AddComment(builder, stmt, "assert statement");

           PredicateStmt s = (PredicateStmt)stmt;

           TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

@@ -3958,7 +3958,7 @@ namespace Microsoft.Dafny {
         invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));

 

         invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));

-        if (loopInv.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {

+        if (loopInv.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

           invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));

         } else {

           bool splitHappened;

@@ -6578,7 +6578,7 @@ namespace Microsoft.Dafny {
       } else if ((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) {

         var e = (QuantifierExpr)expr;

         var inductionVariables = ApplyInduction(e);

-        if (2 <= CommandLineOptions.Clo.DafnyInduction && inductionVariables.Count != 0) {

+        if (2 <= DafnyOptions.O.Induction && inductionVariables.Count != 0) {

           // From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation

           //   (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))

           // For an existential (exists n :: P(n)), it is

@@ -6689,7 +6689,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tracePrinter != null);

       Contract.Ensures(Contract.Result<List<VarType>>() != null);

 

-      if (CommandLineOptions.Clo.DafnyInduction == 0) {

+      if (DafnyOptions.O.Induction == 0) {

         return new List<VarType>();  // don't apply induction

       }

 

@@ -6774,7 +6774,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      if (CommandLineOptions.Clo.DafnyInduction < 2) {

+      if (DafnyOptions.O.Induction < 2) {

         return new List<VarType>();  // don't apply induction

       }

 

@@ -6809,7 +6809,7 @@ namespace Microsoft.Dafny {
     /// Parameter 'n' is allowed to be a ThisSurrogate.

     /// </summary>

     bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {

-      switch (CommandLineOptions.Clo.DafnyInductionHeuristic) {

+      switch (DafnyOptions.O.InductionHeuristic) {

         case 0: return true;

         case 1: return ContainsFreeVariable(expr, false, n);

         default: return VarOccursInArgumentToRecursiveFunction(expr, n, false);

@@ -6827,7 +6827,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(n != null);

 

       // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.

-      var subExprIsProminent = CommandLineOptions.Clo.DafnyInductionHeuristic == 2 || CommandLineOptions.Clo.DafnyInductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;

+      var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;

 

       if (expr is ThisExpr) {

         return exprIsProminent && n is ThisSurrogate;

@@ -6836,13 +6836,13 @@ namespace Microsoft.Dafny {
         return exprIsProminent && e.Var == n;

       } else if (expr is SeqSelectExpr) {

         var e = (SeqSelectExpr)expr;

-        var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent;

+        var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;

         return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) ||  // this subexpression does not acquire "prominent" status

           (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) ||  // this one does (unless arrays/sequences are excluded)

           (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q));    // ditto

       } else if (expr is MultiSelectExpr) {

         var e = (MultiSelectExpr)expr;

-        var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent;

+        var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;

         return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) ||

           e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));

       } else if (expr is FunctionCallExpr) {

@@ -6853,7 +6853,7 @@ namespace Microsoft.Dafny {
         bool inferredDecreases;  // we don't actually care

         var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases);

         bool variantArgument;

-        if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) {

+        if (DafnyOptions.O.InductionHeuristic < 6) {

           variantArgument = rec;

         } else {

           // The receiver is considered to be "variant" if the function is recursive and the receiver participates

@@ -6868,7 +6868,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < e.Function.Formals.Count; i++) {

           var f = e.Function.Formals[i];

           var exp = e.Args[i];

-          if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) {

+          if (DafnyOptions.O.InductionHeuristic < 6) {

             variantArgument = rec;

           } else {

             // The argument position is considered to be "variant" if the function is recursive and the argument participates

diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs
index 1c6c1e77..eed5cf59 100644
--- a/DafnyDriver/DafnyDriver.cs
+++ b/DafnyDriver/DafnyDriver.cs
@@ -4,11 +4,11 @@
 //

 //-----------------------------------------------------------------------------

 //---------------------------------------------------------------------------------------------

-// OnlyDafny OnlyDafny.ssc

+// DafnyDriver

 //       - main program for taking a Dafny program and verifying it

 //---------------------------------------------------------------------------------------------

 

-namespace Microsoft.Boogie

+namespace Microsoft.Dafny

 {

   using System;

   using System.IO;

@@ -17,30 +17,27 @@ namespace Microsoft.Boogie
   using System.Diagnostics.Contracts;

   using PureCollections;

   using Microsoft.Boogie;

+  using Bpl = Microsoft.Boogie;

   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics;

   using VC;

   using AI = Microsoft.AbstractInterpretationFramework;

 

-/*

-  The following assemblies are referenced because they are needed at runtime, not at compile time:

-    BaseTypes

-    Provers.Z3

-    System.Compiler.Framework

-*/

-

-  public class OnlyDafny

+  public class DafnyDriver

   {

     // ------------------------------------------------------------------------

     // Main

 

-    public static int Main (string[] args)

-    {Contract.Requires(cce.NonNullElements(args));

+    public static int Main(string[] args)

+    {

+      Contract.Requires(cce.NonNullElements(args));

+

+      DafnyOptions.Install(new DafnyOptions());

+

       //assert forall{int i in (0:args.Length); args[i] != null};

       ExitValue exitValue = ExitValue.VERIFIED;

       CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;

-      if (CommandLineOptions.Clo.Parse(args) != 1)

-      {

+      if (!CommandLineOptions.Clo.Parse(args)) {

         exitValue = ExitValue.PREPROCESSING_ERROR;

         goto END;

       }

@@ -84,7 +81,6 @@ namespace Microsoft.Boogie
             goto END;

         }

       }

-      CommandLineOptions.Clo.RunningBoogieOnSsc = false;

       exitValue = ProcessFiles(CommandLineOptions.Clo.Files);

 

       END:

@@ -155,7 +151,7 @@ namespace Microsoft.Boogie
           ErrorWriteLine(err);

         } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {

           Dafny.Translator translator = new Dafny.Translator();

-          Program boogieProgram = translator.Translate(dafnyProgram);

+          Bpl.Program boogieProgram = translator.Translate(dafnyProgram);

           if (CommandLineOptions.Clo.PrintFile != null)

           {

             PrintBplFile(CommandLineOptions.Clo.PrintFile, boogieProgram, false);

@@ -176,12 +172,12 @@ namespace Microsoft.Boogie
           switch (oc) {

             case PipelineOutcome.VerificationCompleted:

               WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

-              if ((CommandLineOptions.Clo.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || CommandLineOptions.Clo.ForceCompile)

+              if ((DafnyOptions.O.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || DafnyOptions.O.ForceCompile)

                 CompileDafnyProgram(dafnyProgram);

               break;

             case PipelineOutcome.Done:

               WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

-              if (CommandLineOptions.Clo.ForceCompile)

+              if (DafnyOptions.O.ForceCompile)

                 CompileDafnyProgram(dafnyProgram);

               break;

             default:

@@ -209,7 +205,7 @@ namespace Microsoft.Boogie
       }

     }

 

-    static void PrintBplFile (string filename, Program program, bool allowPrintDesugaring)

+    static void PrintBplFile (string filename, Bpl.Program program, bool allowPrintDesugaring)

     {

       Contract.Requires(filename != null);

       Contract.Requires(program != null);

@@ -230,7 +226,7 @@ namespace Microsoft.Boogie
     }

 

 

-    static bool ProgramHasDebugInfo (Program program)

+    static bool ProgramHasDebugInfo (Bpl.Program program)

     {

       Contract.Requires(program != null);

         // We inspect the last declaration because the first comes from the prelude and therefore always has source context.

@@ -251,7 +247,7 @@ namespace Microsoft.Boogie
     static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories){

       Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);

       Console.WriteLine();

-      Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

+      Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

       if (inconclusives != 0) {

         Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");

       }

@@ -291,11 +287,11 @@ namespace Microsoft.Boogie
     /// Parse the given files into one Boogie program.  If an I/O or parse error occurs, an error will be printed

     /// and null will be returned.  On success, a non-null program is returned.

     /// </summary>

-    static Program ParseBoogieProgram(List<string/*!*/>/*!*/ fileNames, bool suppressTraceOutput)

+    static Bpl.Program ParseBoogieProgram(List<string/*!*/>/*!*/ fileNames, bool suppressTraceOutput)

     {

       Contract.Requires(cce.NonNullElements(fileNames));

       //BoogiePL.Errors.count = 0;

-      Program program = null;

+      Bpl.Program program = null;

       bool okay = true;

       foreach (string bplFileName in fileNames) {

         if (!suppressTraceOutput) {

@@ -307,7 +303,7 @@ namespace Microsoft.Boogie
           }

         }

 

-        Program programSnippet;

+        Bpl.Program programSnippet;

         int errorCount;

         try {

           errorCount = Microsoft.Boogie.Parser.Parse(bplFileName, null, out programSnippet);

@@ -330,7 +326,7 @@ namespace Microsoft.Boogie
       if (!okay) {

         return null;

       } else if (program == null) {

-        return new Program();

+        return new Bpl.Program();

       } else {

         return program;

       }

@@ -344,7 +340,7 @@ namespace Microsoft.Boogie
     /// The method prints errors for resolution and type checking errors, but still returns

     /// their error code.

     /// </summary>

-    static PipelineOutcome BoogiePipelineWithRerun (Program/*!*/ program, string/*!*/ bplFileName,

+    static PipelineOutcome BoogiePipelineWithRerun (Bpl.Program/*!*/ program, string/*!*/ bplFileName,

         out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

     Contract.Requires(bplFileName != null);

@@ -367,7 +363,7 @@ namespace Microsoft.Boogie
 

             List<string/*!*/>/*!*/ fileNames = new List<string/*!*/>();

             fileNames.Add(bplFileName);

-            Program reparsedProgram = ParseBoogieProgram(fileNames, true);

+            Bpl.Program reparsedProgram = ParseBoogieProgram(fileNames, true);

             if (reparsedProgram != null) {

               ResolveAndTypecheck(reparsedProgram, bplFileName);

             }

@@ -394,7 +390,7 @@ namespace Microsoft.Boogie
     ///  - TypeCheckingError if a type checking error occurred

     ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded

     /// </summary>

-    static PipelineOutcome ResolveAndTypecheck (Program program, string bplFileName)

+    static PipelineOutcome ResolveAndTypecheck (Bpl.Program program, string bplFileName)

     {

       Contract.Requires(program != null);

       Contract.Requires(bplFileName != null);

@@ -435,7 +431,7 @@ namespace Microsoft.Boogie
     ///  - VerificationCompleted if inference and verification completed, in which the out

     ///    parameters contain meaningful values

     /// </summary>

-    static PipelineOutcome InferAndVerify (Program program,

+    static PipelineOutcome InferAndVerify (Bpl.Program program,

                                            out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

@@ -491,7 +487,7 @@ namespace Microsoft.Boogie
       }

 

       var decls = program.TopLevelDeclarations.ToArray();

-      foreach ( Declaration decl in decls )

+      foreach (var decl in decls )

       {Contract.Assert(decl != null);

         Implementation impl = decl as Implementation;

         if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)