diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-09-29 11:39:05 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-09-29 11:39:05 +0100 |
| commit | 0b4388429f5eb571fce4b1aff508be891ad75b87 (patch) | |
| tree | b6dcfefbda32bbafc553859e0e3f5268c6eff9a2 /Source/VCGeneration/VC.cs | |
| parent | 99945de38ce51bcc7e2370bffdd00f2f8a203345 (diff) | |
more changes towards parallelisation of Houdini
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 3d9698fd..5880eb16 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1875,7 +1875,7 @@ namespace VC { }
}
- public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null)
+ public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null, int threadID = -1)
{
Contract.Requires(impl != null);
impl.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
@@ -1945,6 +1945,17 @@ namespace VC { b.ErrorData = c.ErrorData;
prefixOfPredicateCmdsInit.Add(b);
+ if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ if (CommandLineOptions.Clo.Cho[threadID].DisableLoopInvMaintainedAssert)
+ b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);
+ else
+ b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
+ } else {
+ b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
+ }
+
+ if (threadID >= 0 && CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)
+
if (CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)
b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);
else
|