From 950c823ddec56d59edb88e6ef81ba541aa5a34df Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Fri, 23 Dec 2016 16:38:21 +0000
Subject: Silenced two "control may reach end of non-void function
 [-Wreturn-type]" compiler warnings, one by adding an assert, and the other by
 refactoring the choose() function.

---
 include/klee/Internal/ADT/DiscretePDF.inc | 42 +++++++++++++++----------------
 1 file changed, 21 insertions(+), 21 deletions(-)

(limited to 'include')

diff --git a/include/klee/Internal/ADT/DiscretePDF.inc b/include/klee/Internal/ADT/DiscretePDF.inc
index 5aee2de5..eb7bd860 100644
--- a/include/klee/Internal/ADT/DiscretePDF.inc
+++ b/include/klee/Internal/ADT/DiscretePDF.inc
@@ -162,32 +162,32 @@ void DiscretePDF<T>::update(T item, weight_type weight) {
 
 template <class T>
 T DiscretePDF<T>::choose(double p) {
-  if (p<0.0 || p>=1.0) {
+  if ((p < 0.0) || (p >= 1.0))
     assert(0 && "choose: argument(p) outside valid range");
-  } else if (!m_root) {
+
+  if (!m_root)
     assert(0 && "choose: choose() called on empty tree");
-  } else {
-    weight_type w = (weight_type) (m_root->sumWeights * p);
-    Node *n = m_root;
-
-    while (1) {
-      if (n->left) {
-        if (w<n->left->sumWeights) {
-          n = n->left;
-          continue;
-        } else {
-          w -= n->left->sumWeights;
-        }
-      }
-      if (w<n->weight || !n->right) {
-        break; // !n->right condition shouldn't be necessary, just sanity check
+
+  weight_type w = (weight_type) (m_root->sumWeights * p);
+  Node *n = m_root;
+
+  while (1) {
+    if (n->left) {
+      if (w<n->left->sumWeights) {
+	n = n->left;
+	continue;
+      } else {
+	w -= n->left->sumWeights;
       }
-      w -= n->weight;
-      n = n->right;
     }
-
-    return n->key;
+    if (w<n->weight || !n->right) {
+      break; // !n->right condition shouldn't be necessary, just sanity check
+    }
+    w -= n->weight;
+    n = n->right;
   }
+
+  return n->key;
 }
 
 template <class T>
-- 
cgit 1.4.1