Applied patch from David Ramos that fixes a bug in minDistToUncovered

   calculation: "Functions with a single instruction were erroneously
   treated as never returning. This propagated far, making many
   instructions unreachable according to this metric."



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

1 files changed, 8 insertions, 2 deletions

diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 7dcca6b2..4906dead 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -714,12 +714,18 @@ void StatsTracker::computeReachableUncovered() {
                 best = val;
             }
           }
-          if (best != cur) {
+          // there's a corner case here when a function only includes a single
+          // instruction (a ret). in that case, we MUST update
+          // functionShortestPath, or it will remain 0 (erroneously indicating
+          // that no return instructions are reachable)
+          Function *f = inst->getParent()->getParent();
+          if (best != cur
+              || (inst == f->begin()->begin()
+                  && functionShortestPath[f] != best)) {
             sm.setIndexedValue(stats::minDistToReturn, id, best);
             changed = true;
 
             // Update shortest path if this is the entry point.
-            Function *f = inst->getParent()->getParent();
             if (inst==f->begin()->begin())
               functionShortestPath[f] = best;
           }