s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

dd_matrix.cc: Add NULL checks for the return values of DD functions 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10479 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 11 years ago
parent
efe6fe0ef9
commit
e9897b4838
1 changed files with 44 additions and 4 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 48
      prism/src/dd/dd_matrix.cc

48
prism/src/dd/dd_matrix.cc
View File

@ -33,6 +33,7 @@
#include <cuddInt.h>
#include "dd_matrix.h"
#include "dd_basics.h"
#include "dd_cudd.h"
extern FILE *dd_out;
@ -53,15 +54,18 @@ double value
// build a 0-1 ADD to store position of element of the vector
f = DD_Constant(ddman, 1);
if (f == NULL) return NULL;
for (i = 0; i < num_vars; i++) {
Cudd_Ref(tmp = vars[i]);
if ((index & (1l<<(num_vars-i-1))) == 0) {
tmp2 = Cudd_addCmpl(ddman, tmp);
if (tmp2 == NULL) return NULL;
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(ddman, tmp);
tmp = tmp2;
}
tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
if (tmp_f == NULL) return NULL;
Cudd_Ref(tmp_f);
Cudd_RecursiveDeref(ddman, tmp);
Cudd_RecursiveDeref(ddman, f);
@ -69,9 +73,11 @@ double value
}
g = DD_Constant(ddman, value);
if (g == NULL) return NULL;
// compute new vector
res = Cudd_addIte(ddman, f, g, dd);
if (res == NULL) return NULL;
Cudd_Ref(res);
Cudd_RecursiveDeref(ddman, f);
Cudd_RecursiveDeref(ddman, g);
@ -100,15 +106,18 @@ double value
// build a 0-1 ADD to store position of element of the matrix
f = DD_Constant(ddman, 1);
if (f == NULL) return NULL;
for (i = 0; i < num_rvars; i++) {
Cudd_Ref(tmp = rvars[i]);
if ((rindex & (1l<<(num_rvars-i-1))) == 0) {
tmp2 = Cudd_addCmpl(ddman, tmp);
if (tmp2 == NULL) return NULL;
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(ddman, tmp);
tmp = tmp2;
}
tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
if (tmp_f == NULL) return NULL;
Cudd_Ref(tmp_f);
Cudd_RecursiveDeref(ddman, tmp);
Cudd_RecursiveDeref(ddman, f);
@ -118,11 +127,13 @@ double value
Cudd_Ref(tmp = cvars[i]);
if ((cindex & (1l<<(num_cvars-i-1))) == 0) {
tmp2 = Cudd_addCmpl(ddman, tmp);
if (tmp2 == NULL) return NULL;
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(ddman, tmp);
tmp = tmp2;
}
tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
if (tmp_f == NULL) return NULL;
Cudd_Ref(tmp_f);
Cudd_RecursiveDeref(ddman, tmp);
Cudd_RecursiveDeref(ddman, f);
@ -130,9 +141,11 @@ double value
}
g = DD_Constant(ddman, value);
if (g == NULL) return NULL;
// compute new vector
res = Cudd_addIte(ddman, f, g, dd);
if (res == NULL) return NULL;
Cudd_Ref(res);
Cudd_RecursiveDeref(ddman, f);
Cudd_RecursiveDeref(ddman, g);
@ -164,15 +177,18 @@ double value
// build a 0-1 ADD to store position of element of the matrix
f = DD_Constant(ddman, 1);
if (f == NULL) return NULL;
for (i = 0; i < num_rvars; i++) {
Cudd_Ref(tmp = rvars[i]);
if ((rindex & (1l<<(num_rvars-i-1))) == 0) {
tmp2 = Cudd_addCmpl(ddman, tmp);
if (tmp2 == NULL) return NULL;
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(ddman, tmp);
tmp = tmp2;
}
tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
if (tmp_f == NULL) return NULL;
Cudd_Ref(tmp_f);
Cudd_RecursiveDeref(ddman, tmp);
Cudd_RecursiveDeref(ddman, f);
@ -182,11 +198,13 @@ double value
Cudd_Ref(tmp = cvars[i]);
if ((cindex & (1l<<(num_cvars-i-1))) == 0) {
tmp2 = Cudd_addCmpl(ddman, tmp);
if (tmp2 == NULL) return NULL;
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(ddman, tmp);
tmp = tmp2;
}
tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
if (tmp_f == NULL) return NULL;
Cudd_Ref(tmp_f);
Cudd_RecursiveDeref(ddman, tmp);
Cudd_RecursiveDeref(ddman, f);
@ -196,11 +214,13 @@ double value
Cudd_Ref(tmp = lvars[i]);
if ((lindex & (1l<<(num_lvars-i-1))) == 0) {
tmp2 = Cudd_addCmpl(ddman, tmp);
if (tmp2 == NULL) return NULL;
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(ddman, tmp);
tmp = tmp2;
}
tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
if (tmp_f == NULL) return NULL;
Cudd_Ref(tmp_f);
Cudd_RecursiveDeref(ddman, tmp);
Cudd_RecursiveDeref(ddman, f);
@ -208,9 +228,11 @@ double value
}
g = DD_Constant(ddman, value);
if (g == NULL) return NULL;
// compute new vector
res = Cudd_addIte(ddman, f, g, dd);
if (res == NULL) return NULL;
Cudd_Ref(res);
Cudd_RecursiveDeref(ddman, f);
Cudd_RecursiveDeref(ddman, g);
@ -246,6 +268,10 @@ long x
inputs[vars[i]->index] = ((x & (1l<<(num_vars-i-1))) == 0) ? 0 : 1;
}
node = Cudd_Eval(ddman, dd, inputs);
if (node == NULL) {
DD_SetErrorFlag();
return 0;
}
val = Cudd_V(node);
if (inputs != NULL) {
@ -268,6 +294,7 @@ int num_vars
DdNode *tmp;
tmp = Cudd_addXeqy(ddman, num_vars, rvars, cvars);
if (tmp == NULL) return NULL;
Cudd_Ref(tmp);
return tmp;
@ -330,7 +357,8 @@ int num_vars
permut[row_vars[i]->index] = col_vars[i]->index;
permut[col_vars[i]->index] = row_vars[i]->index;
}
res = Cudd_addPermute(ddman, dd, permut);
res = Cudd_addPermute(ddman, dd, permut);
if (res == NULL) return NULL;
Cudd_Ref(res);
Cudd_RecursiveDeref(ddman, dd);
@ -385,6 +413,10 @@ int accuracy
inputs[vars[j]->index] = ((i & (1l<<(num_vars-j-1))) == 0) ? 0 : 1;
}
node = Cudd_Eval(ddman, dd, inputs);
if (node == NULL) {
DD_SetErrorFlag();
return;
}
val = Cudd_V(node);
switch (accuracy) {
case ACCURACY_ZERO_ONE: fprintf(dd_out, "%c", val>0?'1':'0'); break;
@ -454,6 +486,10 @@ int accuracy
inputs[cvars[k]->index] = ((j & (1l<<(num_cvars-k-1))) == 0) ? 0 : 1;
}
node = Cudd_Eval(ddman, dd, inputs);
if (node == NULL) {
DD_SetErrorFlag();
return;
}
val = Cudd_V(node);
switch (accuracy) {
case ACCURACY_ZERO_ONE: fprintf(dd_out, "%c", val>0?'1':'0'); break;
@ -521,6 +557,10 @@ int accuracy
inputs[vars[j]->index] = ((i & (1l<<(num_vars-j-1))) == 0) ? 0 : 1;
}
node = Cudd_Eval(ddman, dd, inputs);
if (node == NULL) {
DD_SetErrorFlag();
return;
}
val = Cudd_V(node);
switch (accuracy) {
case ACCURACY_ZERO_ONE: fprintf(dd_out, "%c", val>0?'1':'0'); break;

Write Preview
Loading…
Cancel
Save