From 90326ecfaf36d6b6863cb09b2902147f059db58f Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 7 Aug 2015 09:40:09 +0000
Subject: [PATCH] dd_term.cc: Add NULL checks for the return values of DD
 functions

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10477 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/dd/dd_term.cc | 41 +++++++++++++++++++++++++++++++++--------
 1 file changed, 33 insertions(+), 8 deletions(-)

diff --git a/prism/src/dd/dd_term.cc b/prism/src/dd/dd_term.cc
index 266bbd1b..1855ae92 100644
--- a/prism/src/dd/dd_term.cc
+++ b/prism/src/dd/dd_term.cc
@@ -30,6 +30,7 @@
 #include "dd_basics.h"
 #include "dd_term.h"
 #include "dd_export.h"
+#include "dd_cudd.h"
 
 //------------------------------------------------------------------------------
 
@@ -43,6 +44,7 @@ double threshold
 	DdNode *tmp, *tmp2;
 	
 	tmp = Cudd_addBddThreshold(ddman, dd, threshold);
+	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
 	Cudd_RecursiveDeref(ddman, dd);
 	tmp2 = Cudd_BddToAdd(ddman, tmp);	
@@ -64,6 +66,7 @@ double threshold
 	DdNode *tmp, *tmp2;
 	
 	tmp = Cudd_addBddStrictThreshold(ddman, dd, threshold);
+	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
 	Cudd_RecursiveDeref(ddman, dd);
 	tmp2 = Cudd_BddToAdd(ddman, tmp);	
@@ -106,7 +109,10 @@ DdNode *dd,
 double threshold
 )
 {
-	return DD_Not(ddman, DD_Threshold(ddman, dd, threshold));
+	DdNode* res;
+	res = DD_Threshold(ddman, dd, threshold);
+	if (res == NULL) return NULL;
+	return DD_Not(ddman, res);
 }
 
 //------------------------------------------------------------------------------
@@ -118,7 +124,10 @@ DdNode *dd,
 double threshold
 )
 {
-	return DD_Not(ddman, DD_StrictThreshold(ddman, dd, threshold));
+	DdNode* res;
+	res = DD_StrictThreshold(ddman, dd, threshold);
+	if (res == NULL) return NULL;
+	return DD_Not(ddman, res);
 }
 
 //------------------------------------------------------------------------------
@@ -144,14 +153,16 @@ double upper
 )
 {
 	DdNode *tmp, *tmp2;
-	
+
 	tmp = Cudd_addBddInterval(ddman, dd, lower, upper);
+	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
 	Cudd_RecursiveDeref(ddman, dd);
-	tmp2 = Cudd_BddToAdd(ddman, tmp);	
-	Cudd_Ref(tmp2);	
+	tmp2 = Cudd_BddToAdd(ddman, tmp);
+	if (tmp2 == NULL) return NULL;
+	Cudd_Ref(tmp2);
 	Cudd_RecursiveDeref(ddman, tmp);
-	
+
 	return tmp2;
 }
 
@@ -167,6 +178,7 @@ int places
 	DdNode *res;
 	
 	res = Cudd_addRoundOff(ddman, dd, places);
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, dd);
 	
@@ -213,7 +225,12 @@ DdManager *ddman,
 DdNode *dd	
 )
 {
-	return Cudd_V(Cudd_addFindMin(ddman, dd));
+	DdNode *v = Cudd_addFindMin(ddman, dd);
+	if (v == NULL) {
+		DD_SetErrorFlag();
+		return 0.0;
+	}
+	return Cudd_V(v);
 }
 
 //------------------------------------------------------------------------------
@@ -224,7 +241,12 @@ DdManager *ddman,
 DdNode *dd	
 )
 {
-	return Cudd_V(Cudd_addFindMax(ddman, dd));
+	DdNode *v = Cudd_addFindMax(ddman, dd);
+	if (v == NULL) {
+		DD_SetErrorFlag();
+		return 0.0;
+	}
+	return Cudd_V(v);
 }
 
 //------------------------------------------------------------------------------
@@ -243,16 +265,19 @@ int num_vars
 	// construct filter to get first non-zero element
 	ptr = dd;
 	filter = DD_Constant(ddman, 1);
+	if (filter == NULL) return NULL;
 	for (i = 0; i < num_vars; i++) {
 		next_ptr = (ptr->index > vars[i]->index) ? ptr : Cudd_E(ptr);
 		if (next_ptr != Cudd_ReadZero(ddman)) {
 			Cudd_Ref(vars[i]);
 			filter = DD_And(ddman, filter, DD_Not(ddman, vars[i]));
+			if (filter == NULL) return NULL;
 		}
 		else {
 			next_ptr = (ptr->index > vars[i]->index) ? ptr : Cudd_T(ptr);
 			Cudd_Ref(vars[i]);
 			filter = DD_And(ddman, filter, vars[i]);
+			if (filter == NULL) return NULL;
 		}
 		ptr = next_ptr;
 	}