diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 14 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 9 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 1 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 27 |
4 files changed, 42 insertions, 9 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 2237c2fc..549c700a 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -378,7 +378,7 @@ namespace Microsoft.Boogie { // -----------------------------------------------------------------------------------------------
public abstract class ProverInterface {
- public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {
+ public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
Contract.Requires(prog != null);
ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
@@ -393,7 +393,11 @@ namespace Microsoft.Boogie { options.TimeLimit = timeout * 1000;
}
- options.Parse(CommandLineOptions.Clo.ProverOptions);
+ if (taskID >= 0) {
+ options.Parse(CommandLineOptions.Clo.Cho[taskID].ProverOptions);
+ } else {
+ options.Parse(CommandLineOptions.Clo.ProverOptions);
+ }
ProverContext ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
@@ -492,7 +496,7 @@ namespace Microsoft.Boogie { throw new System.NotImplementedException();
}
[NoDefaultContract]
- public abstract Outcome CheckOutcome(ErrorHandler handler);
+ public abstract Outcome CheckOutcome(ErrorHandler handler, int taskID = -1);
public virtual string[] CalculatePath(int controlFlowConstant) {
throw new System.NotImplementedException();
}
@@ -560,7 +564,7 @@ namespace Microsoft.Boogie { throw new NotImplementedException();
}
- public virtual Outcome CheckOutcomeCore(ErrorHandler handler)
+ public virtual Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)
{
throw new NotImplementedException();
}
@@ -619,7 +623,7 @@ namespace Microsoft.Boogie { throw new NotImplementedException();
}
[NoDefaultContract]
- public override Outcome CheckOutcome(ErrorHandler handler) {
+ public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1) {
//Contract.Requires(handler != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
throw new NotImplementedException();
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ca5772ed..8fe4a5c6 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1342,7 +1342,14 @@ namespace VC { }
}
}
- IEnumerable sortedNodes = dag.TopologicalSort();
+
+ IEnumerable sortedNodes;
+ if (CommandLineOptions.Clo.ModifyTopologicalSorting) {
+ sortedNodes = dag.TopologicalSort(true);
+ } else {
+ sortedNodes = dag.TopologicalSort();
+ }
+
Contract.Assert(sortedNodes != null);
#endregion
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index bf3f267f..086dde15 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1079,6 +1079,7 @@ namespace VC { private Outcome CheckVC() {
prover.Check();
ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter);
+
return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index e9ca2fe6..2abe4a1b 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2016,7 +2016,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 taskID = -1)
{
Contract.Requires(impl != null);
impl.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
@@ -2081,11 +2081,32 @@ namespace VC { {
if (a is AssertCmd) {
Bpl.AssertCmd c = (AssertCmd) a;
- Bpl.AssertCmd b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);
+ 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
+ b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);
+ } else {
+ b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);
+ }
+
b.Attributes = c.Attributes;
b.ErrorData = c.ErrorData;
prefixOfPredicateCmdsInit.Add(b);
- b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
+
+ if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ Contract.Assert(taskID >= 0);
+ if (CommandLineOptions.Clo.Cho[taskID].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);
+ }
+
b.Attributes = c.Attributes;
b.ErrorData = c.ErrorData;
prefixOfPredicateCmdsMaintained.Add(b);
|