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

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10478 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/dd/dd_vars.cc | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/prism/src/dd/dd_vars.cc b/prism/src/dd/dd_vars.cc
index fecfe9b8..60973945 100644
--- a/prism/src/dd/dd_vars.cc
+++ b/prism/src/dd/dd_vars.cc
@@ -54,6 +54,7 @@ int num_vars
 		permut[old_vars[i]->index] = new_vars[i]->index;
 	}	
 	res = Cudd_addPermute(ddman, dd, permut);	
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, dd);
 
@@ -80,7 +81,7 @@ int num_vars
 	DdNode *res;
 	
 	res = Cudd_addSwapVariables(ddman, dd, old_vars, new_vars, num_vars);
-	Cudd_Ref(res);
+	if (res != NULL) Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, dd);
 	
 	return res;
@@ -108,15 +109,19 @@ int num_vars
 	y_bdd_vars = new DdNode*[num_vars];
 	for (i = 0; i < num_vars; i++) {
 		x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
+		if (x_bdd_vars[i] == NULL) return NULL;
 		Cudd_Ref(x_bdd_vars[i]);
 		y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
+		if (y_bdd_vars[i] == NULL) return NULL;
 		Cudd_Ref(y_bdd_vars[i]);
 	}
 	// call main function
 	tmp = Cudd_Xgty(ddman, num_vars, NULL, x_bdd_vars, y_bdd_vars);
+	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
 	// convert bdd to add
 	res = Cudd_BddToAdd(ddman, tmp);
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, tmp);
 	// free variables
@@ -143,7 +148,9 @@ DdNode **y_vars,
 int num_vars
 )
 {
-	return DD_Not(ddman, DD_VariablesLessThan(ddman, x_vars, y_vars, num_vars));
+	DdNode* res = DD_VariablesLessThan(ddman, x_vars, y_vars, num_vars);
+	if (res == NULL) return NULL;
+	return DD_Not(ddman, res);
 }
 
 //------------------------------------------------------------------------------
@@ -168,15 +175,19 @@ int num_vars
 	y_bdd_vars = new DdNode*[num_vars];
 	for (i = 0; i < num_vars; i++) {
 		x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
+		if (x_bdd_vars[i] == NULL) return NULL;
 		Cudd_Ref(x_bdd_vars[i]);
 		y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
+		if (y_bdd_vars[i] == NULL) return NULL;
 		Cudd_Ref(y_bdd_vars[i]);
 	}
 	// call main function
 	tmp = Cudd_Xgty(ddman, num_vars, NULL, y_bdd_vars, x_bdd_vars);
+	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
 	// convert bdd to add
 	res = Cudd_BddToAdd(ddman, tmp);
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, tmp);
 	// free variables
@@ -203,7 +214,8 @@ DdNode **y_vars,
 int num_vars
 )
 {
-	return DD_Not(ddman, DD_VariablesGreaterThan(ddman, x_vars, y_vars, num_vars));
+	DdNode* res = DD_VariablesGreaterThan(ddman, x_vars, y_vars, num_vars);
+	return DD_Not(ddman, res);
 }
 
 //------------------------------------------------------------------------------
@@ -228,15 +240,19 @@ int num_vars
 	y_bdd_vars = new DdNode*[num_vars];
 	for (i = 0; i < num_vars; i++) {
 		x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
+		if (x_bdd_vars[i] == NULL) return NULL;
 		Cudd_Ref(x_bdd_vars[i]);
 		y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
+		if (y_bdd_vars[i] == NULL) return NULL;
 		Cudd_Ref(y_bdd_vars[i]);
 	}
 	// call main function
 	tmp = Cudd_Xeqy(ddman, num_vars, x_bdd_vars, y_bdd_vars);
+	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
 	// convert bdd to add
 	res = Cudd_BddToAdd(ddman, tmp);
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, tmp);
 	// free variables