diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-10-02 22:27:35 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-10-02 22:27:35 +0100 |
| commit | 3297f35c08738cd95bd01c1f4ab1e8baadddf67e (patch) | |
| tree | 58adb68086eb78112a55005892fc53e749ff036d /Source | |
| parent | 2a32d6e6a9b7e193c7a49893acc52397f1824d1d (diff) | |
small refactoring
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 6 | ||||
| -rw-r--r-- | Source/Houdini/ConcurrentHoudini.cs | 9 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
4 files changed, 11 insertions, 10 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 968333b2..5c18ddfe 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -399,7 +399,7 @@ namespace Microsoft.Boogie { public bool ExplainHoudini = false;
public bool ConcurrentHoudini = false;
public bool ModifyTopologicalSorting = false;
- public bool DebugParallelHoudini = false;
+ public bool DebugConcurrentHoudini = false;
public bool HoudiniUseCrossDependencies = false;
public string StagedHoudini = null;
public bool DebugStagedHoudini = false;
@@ -1190,9 +1190,9 @@ namespace Microsoft.Boogie { }
return true;
- case "debugParallelHoudini":
+ case "debugConcurrentHoudini":
if (ps.ConfirmArgumentCount(0)) {
- DebugParallelHoudini = true;
+ DebugConcurrentHoudini = true;
}
return true;
diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs index be7b1b79..687dfb78 100644 --- a/Source/Houdini/ConcurrentHoudini.cs +++ b/Source/Houdini/ConcurrentHoudini.cs @@ -91,7 +91,7 @@ namespace Microsoft.Boogie.Houdini RefutedAnnotation ra = refutedSharedAnnotations[key]; if (kv.Key != null) { - if (CommandLineOptions.Clo.DebugParallelHoudini) + if (CommandLineOptions.Clo.DebugConcurrentHoudini) Console.WriteLine("(+) " + ra.Constant + "," + ra.Kind + "," + ra.CalleeProc + "," + ra.RefutationSite); AddRelatedToWorkList(ra); @@ -100,9 +100,6 @@ namespace Microsoft.Boogie.Houdini } } - if (CommandLineOptions.Clo.DebugParallelHoudini) - Console.WriteLine("# refuted annotations received from the shared exchanging set: " + count); - return count > 0 ? true : false; } @@ -145,8 +142,8 @@ namespace Microsoft.Boogie.Houdini } } - if (CommandLineOptions.Clo.DebugParallelHoudini) - Console.WriteLine("# exchange set size: " + refutedSharedAnnotations.Count); + if (CommandLineOptions.Clo.DebugConcurrentHoudini) + Console.WriteLine("# number of shared refuted annotations: " + refutedSharedAnnotations.Count); if (ExchangeRefutedAnnotations()) dequeue = false; diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 4a5d23d6..b46e6fea 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -819,7 +819,9 @@ namespace Microsoft.Boogie.SMTLib FlushProverWarnings();
var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
- if (taskID >= 0) {
+
+ if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ Contract.Assert(taskID >= 0);
errorsLeft = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit;
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index f1c01758..85d0fb31 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1943,6 +1943,7 @@ namespace VC { Bpl.AssertCmd b = null;
if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ Contract.Assert(taskID >= 0);
if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvEntryAssert)
b = new Bpl.LoopInitAssertCmd(c.tok, Expr.True);
else
@@ -1956,6 +1957,7 @@ namespace VC { prefixOfPredicateCmdsInit.Add(b);
if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ Contract.Assert(taskID >= 0);
if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvMaintainedAssert)
b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);
else
|