From 0732077773c80e86f8fbbc0be94ae9c034ad1924 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Thu, 29 Oct 2015 18:40:23 -0500
Subject: Add support for annotating implementations with k-ind. depth.

---
 Source/VCGeneration/VC.cs | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'Source')

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) {
-- 
cgit v1.2.3