summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/VCGeneration/VC.cs11
1 files changed, 5 insertions, 6 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 33e2f928..79f56934 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2229,10 +2229,11 @@ namespace VC {
impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })));
ResetPredecessors(impl.Blocks);
- if(CommandLineOptions.Clo.KInductionDepth < 0) {
+ var k = Math.Max(CommandLineOptions.Clo.KInductionDepth, QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1));
+ if(k < 0) {
ConvertCFG2DAGStandard(impl, edgesCut, taskID);
} else {
- ConvertCFG2DAGKInduction(impl, edgesCut, taskID);
+ ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k);
}
#region Debug Tracing
@@ -2497,14 +2498,12 @@ namespace VC {
return referencedVars;
}
- private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID) {
+ private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID, int inductionK) {
// K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses
Contract.Requires(edgesCut == null);
Contract.Requires(taskID == -1);
-
- int inductionK = CommandLineOptions.Clo.KInductionDepth;
- Contract.Assume(inductionK >= 0);
+ Contract.Requires(0 <= inductionK);
bool contRuleApplication = true;
while (contRuleApplication) {