commit 6a6719a3a11087b48d9f1a4eb08b3bd43cb05a65
author Ted Kremenek <kremenek@apple.com> Fri Feb 29 20:27:50 2008 +0000
committer Ted Kremenek <kremenek@apple.com> Fri Feb 29 20:27:50 2008 +0000
tree fa01ab5062491a62eb21ad3016921384d3468ff2
parent fce90e324bfc0608ed9f0a778dde915c7291ad0c

"Refinement" of hack to bound loop-traversals: visit any block at a maximum of 3 times along a given path.


git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@47766 91177308-0d34-0410-b5e6-96231b3b80d8

Analysis/GRExprEngine.cpp

diff --git a/Analysis/GRExprEngine.cpp b/Analysis/GRExprEngine.cpp
index 74f3a9a..2b94b4f 100644
--- a/Analysis/GRExprEngine.cpp
+++ b/Analysis/GRExprEngine.cpp
@@ -147,6 +147,12 @@
   }
 }
 
+bool GRExprEngine::ProcessBlockEntrance(CFGBlock* B, ValueState*,
+                                        GRBlockCounter BC) {
+  
+  return BC.getNumVisited(B->getBlockID()) < 3;
+}
+
 void GRExprEngine::ProcessBranch(Expr* Condition, Stmt* Term,
                                  BranchNodeBuilder& builder) {
 
@@ -156,15 +162,6 @@
   // Check for NULL conditions; e.g. "for(;;)"
   if (!Condition) { 
     builder.markInfeasible(false);
-    
-    // Get the current block counter.
-    GRBlockCounter BC = builder.getBlockCounter();
-    unsigned BlockID = builder.getTargetBlock(true)->getBlockID();
-    unsigned NumVisited = BC.getNumVisited(BlockID);
-        
-    if (NumVisited < 1) builder.generateNode(PrevState, true);
-    else builder.markInfeasible(true);
-
     return;
   }
   
@@ -191,46 +188,25 @@
       return;
     }      
   }
-  
-  // Get the current block counter.
-  GRBlockCounter BC = builder.getBlockCounter();
-  unsigned BlockID = builder.getTargetBlock(true)->getBlockID();
-  unsigned NumVisited = BC.getNumVisited(BlockID);
-  
-  if (isa<nonlval::ConcreteInt>(V) || 
-      BC.getNumVisited(builder.getTargetBlock(true)->getBlockID()) < 1) {
     
-    // Process the true branch.
 
-    bool isFeasible = true;
-    
-    ValueState* St = Assume(PrevState, V, true, isFeasible);
+  // Process the true branch.
 
-    if (isFeasible)
-      builder.generateNode(MarkBranch(St, Term, true), true);
-    else
-      builder.markInfeasible(true);
-  }
+  bool isFeasible = true;  
+  ValueState* St = Assume(PrevState, V, true, isFeasible);
+
+  if (isFeasible)
+    builder.generateNode(MarkBranch(St, Term, true), true);
   else
     builder.markInfeasible(true);
+      
+  // Process the false branch.  
   
-  BlockID = builder.getTargetBlock(false)->getBlockID();
-  NumVisited = BC.getNumVisited(BlockID);
+  isFeasible = false;
+  St = Assume(PrevState, V, false, isFeasible);
   
-  if (isa<nonlval::ConcreteInt>(V) || 
-      BC.getNumVisited(builder.getTargetBlock(false)->getBlockID()) < 1) {
-    
-    // Process the false branch.  
-    
-    bool isFeasible = false;
-    
-    ValueState* St = Assume(PrevState, V, false, isFeasible);
-    
-    if (isFeasible)
-      builder.generateNode(MarkBranch(St, Term, false), false);
-    else
-      builder.markInfeasible(false);
-  }
+  if (isFeasible)
+    builder.generateNode(MarkBranch(St, Term, false), false);
   else
     builder.markInfeasible(false);
 }