From 3be99a61cfb12fac43926924fb7972ae5b8e078b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 7 Aug 2015 09:39:19 +0000 Subject: [PATCH] dd_abstr.cc: Add NULL checks for the return values of DD functions git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10475 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/dd/dd_abstr.cc | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/prism/src/dd/dd_abstr.cc b/prism/src/dd/dd_abstr.cc index 70fa002e..9dbd35af 100644 --- a/prism/src/dd/dd_abstr.cc +++ b/prism/src/dd/dd_abstr.cc @@ -42,8 +42,10 @@ int num_vars DdNode *cube, *res; cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars); + if (cube == NULL) return NULL; Cudd_Ref(cube); res = Cudd_addOrAbstract(ddman, dd, cube); + if (res == NULL) return NULL; Cudd_Ref(res); Cudd_RecursiveDeref(ddman, dd); Cudd_RecursiveDeref(ddman,cube); @@ -64,8 +66,10 @@ int num_vars DdNode *cube, *res; cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars); + if (cube == NULL) return NULL; Cudd_Ref(cube); - res = Cudd_addUnivAbstract(ddman, dd, cube); + res = Cudd_addUnivAbstract(ddman, dd, cube); + if (res == NULL) return NULL; Cudd_Ref(res); Cudd_RecursiveDeref(ddman, dd); Cudd_RecursiveDeref(ddman, cube); @@ -86,8 +90,10 @@ int num_vars DdNode *cube, *res; cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars); + if (cube == NULL) return NULL; Cudd_Ref(cube); res = Cudd_addExistAbstract(ddman, dd, cube); + if (res == NULL) return NULL; Cudd_Ref(res); Cudd_RecursiveDeref(ddman, dd); Cudd_RecursiveDeref(ddman, cube); @@ -108,8 +114,10 @@ int num_vars DdNode *cube, *res; cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars); + if (cube == NULL) return NULL; Cudd_Ref(cube); res = Cudd_addUnivAbstract(ddman, dd, cube); + if (res == NULL) return NULL; Cudd_Ref(res); Cudd_RecursiveDeref(ddman, dd); Cudd_RecursiveDeref(ddman, cube); @@ -130,8 +138,10 @@ int num_vars DdNode *cube, *res; cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars); + if (cube == NULL) return NULL; Cudd_Ref(cube); res = Cudd_addMinAbstract(ddman, dd, cube); + if (res == NULL) return NULL; Cudd_Ref(res); Cudd_RecursiveDeref(ddman, dd); Cudd_RecursiveDeref(ddman, cube); @@ -152,8 +162,10 @@ int num_vars DdNode *cube, *res; cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars); + if (cube == NULL) return NULL; Cudd_Ref(cube); res = Cudd_addMaxAbstract(ddman, dd, cube); + if (res == NULL) return NULL; Cudd_Ref(res); Cudd_RecursiveDeref(ddman, dd); Cudd_RecursiveDeref(ddman, cube);