diff options
author | 2011-11-15 18:48:02 -0800 | |
---|---|---|
committer | 2011-11-15 18:48:02 -0800 | |
commit | 209496c409f76b7dc8282ec7a540e08e1fc70924 (patch) | |
tree | 58cfdfb2c11a7e387f2f0265a6817d598c357cb6 | |
parent | f1974cc472fda89f45a049c24f6df0ad1a41c315 (diff) |
Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLineOptions to separate the options that belong to these 3 tools.
-rw-r--r-- | Dafny/DafnyMain.cs | 4 | ||||
-rw-r--r-- | Dafny/DafnyOptions.cs | 132 | ||||
-rw-r--r-- | Dafny/DafnyPipeline.csproj | 1 | ||||
-rw-r--r-- | Dafny/Translator.cs | 36 | ||||
-rw-r--r-- | DafnyDriver/DafnyDriver.cs | 56 |
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)
|