diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 61 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 52 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 6 |
3 files changed, 65 insertions, 54 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 6897a982..a0454229 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -4,6 +4,7 @@ //
//-----------------------------------------------------------------------------
using System;
+using System.Linq;
using System.Collections;
using System.Collections.Generic;
using System.Threading;
@@ -159,54 +160,38 @@ namespace Microsoft.Boogie { private static void Setup(Program prog, ProverContext ctx)
{
- // set up the context
- foreach (Declaration decl in prog.TopLevelDeclarations)
+ // set up the context
+ foreach (Declaration decl in prog.TopLevelDeclarations.ToList())
+ {
+ Contract.Assert(decl != null);
+ var typeDecl = decl as TypeCtorDecl;
+ var constDecl = decl as Constant;
+ var funDecl = decl as Function;
+ var axiomDecl = decl as Axiom;
+ var glVarDecl = decl as GlobalVariable;
+ if (typeDecl != null)
{
- Contract.Assert(decl != null);
- TypeCtorDecl t = decl as TypeCtorDecl;
- if (t != null)
- {
- ctx.DeclareType(t, null);
- }
+ ctx.DeclareType(typeDecl, null);
}
- foreach (Declaration decl in prog.TopLevelDeclarations)
+ else if (constDecl != null)
{
- Contract.Assert(decl != null);
- Constant c = decl as Constant;
- if (c != null)
- {
- ctx.DeclareConstant(c, c.Unique, null);
- }
- else
- {
- Function f = decl as Function;
- if (f != null)
- {
- ctx.DeclareFunction(f, null);
- }
- }
+ ctx.DeclareConstant(constDecl, constDecl.Unique, null);
}
- foreach (Declaration decl in prog.TopLevelDeclarations)
+ else if (funDecl != null)
{
- Contract.Assert(decl != null);
- Axiom ax = decl as Axiom;
- if (ax != null)
- {
- ctx.AddAxiom(ax, null);
- }
+ ctx.DeclareFunction(funDecl, null);
}
- foreach (Declaration decl in prog.TopLevelDeclarations)
+ else if (axiomDecl != null)
{
- Contract.Assert(decl != null);
- GlobalVariable v = decl as GlobalVariable;
- if (v != null)
- {
- ctx.DeclareGlobalVariable(v, null);
- }
+ ctx.AddAxiom(axiomDecl, null);
}
+ else if (glVarDecl != null)
+ {
+ ctx.DeclareGlobalVariable(glVarDecl, null);
+ }
+ }
}
-
/// <summary>
/// Clean-up.
/// </summary>
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 3ae97bdd..bcafb9cb 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -4,6 +4,7 @@ //
//-----------------------------------------------------------------------------
using System;
+using System.Linq;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
@@ -147,14 +148,14 @@ namespace Microsoft.Boogie { return naryExpr.Fun.FunctionName;
}
- public void Print(int indent, Action<Block> blockAction = null) {
+ public void Print(int indent, TextWriter tw, Action<Block> blockAction = null) {
int numBlock = -1;
string ind = new string(' ', indent);
foreach (Block b in Trace) {
Contract.Assert(b != null);
numBlock++;
if (b.tok == null) {
- Console.WriteLine("{0}<intermediate block>", ind);
+ tw.WriteLine("{0}<intermediate block>", ind);
} else {
// for ErrorTrace == 1 restrict the output;
// do not print tokens with -17:-4 as their location because they have been
@@ -165,7 +166,7 @@ namespace Microsoft.Boogie { blockAction(b);
}
- Console.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);
+ tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);
for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)
{
@@ -178,13 +179,13 @@ namespace Microsoft.Boogie { {
Contract.Assert(calleeCounterexamples[loc].args.Count == 1);
var arg = calleeCounterexamples[loc].args[0];
- Console.WriteLine("{0}value = {1}", ind, arg.ToString());
+ tw.WriteLine("{0}value = {1}", ind, arg.ToString());
}
else
{
- Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);
- calleeCounterexamples[loc].counterexample.Print(indent + 4);
- Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);
+ tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);
+ calleeCounterexamples[loc].counterexample.Print(indent + 4, tw);
+ tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);
}
}
}
@@ -197,7 +198,7 @@ namespace Microsoft.Boogie { public bool ModelHasStatesAlready = false;
- public void PrintModel()
+ public void PrintModel(TextWriter tw)
{
var filename = CommandLineOptions.Clo.ModelViewFile;
if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;
@@ -205,8 +206,8 @@ namespace Microsoft.Boogie { var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();
if (filename == "-") {
- m.Write(Console.Out);
- Console.Out.Flush();
+ m.Write(tw);
+ tw.Flush();
} else {
using (var wr = new StreamWriter(filename, !firstModelFile)) {
firstModelFile = false;
@@ -532,7 +533,7 @@ namespace VC { }
[ContractClass(typeof(ConditionGenerationContracts))]
- public abstract class ConditionGeneration {
+ public abstract class ConditionGeneration : IDisposable {
protected internal object CheckerCommonState;
public enum Outcome {
@@ -570,6 +571,9 @@ namespace VC { public int CumulativeAssertionCount; // for statistics
protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();
+
+ private bool _disposed;
+
protected VariableSeq CurrentLocalVariables = null;
// shared across each implementation; created anew for each implementation
@@ -1626,6 +1630,24 @@ namespace VC { #endregion
}
+
+ public void Dispose()
+ {
+ Dispose(true);
+ GC.SuppressFinalize(this);
+ }
+
+ protected virtual void Dispose(bool disposing)
+ {
+ if (!_disposed)
+ {
+ if (disposing)
+ {
+ Close();
+ }
+ _disposed = true;
+ }
+ }
}
public class ModelViewInfo
@@ -1643,10 +1665,10 @@ namespace VC { Contract.Requires(impl != null);
// global variables
- foreach (Declaration d in program.TopLevelDeclarations) {
- if (d is Constant) continue;
- if (d is Variable) {
- AllVariables.Add((Variable)d);
+ foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>()) {
+ if (!(v is Constant))
+ {
+ AllVariables.Add(v);
}
}
// implementation parameters
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 6a0891b8..bea79f13 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1410,7 +1410,11 @@ namespace VC { }
ModelViewInfo mvInfo;
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;
+ lock (program)
+ {
+ gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
+ }
double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;
int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits,
|