From ab136ae5e2a1872520695aa4ad8a9083cbb346c6 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Aug 2015 10:08:18 +0000 Subject: [PATCH] JDDNode.getThen() and getElse(): Protect against calls for a constant node, which is invalid. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10508 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jdd/JDD.cc | 8 ++++++-- prism/src/jdd/JDDNode.java | 6 +++++- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/prism/src/jdd/JDD.cc b/prism/src/jdd/JDD.cc index 5ca51796..f8c37a9a 100644 --- a/prism/src/jdd/JDD.cc +++ b/prism/src/jdd/JDD.cc @@ -807,7 +807,9 @@ JNIEXPORT jdouble JNICALL Java_jdd_JDDNode_DDN_1GetValue(JNIEnv *env, jclass cls JNIEXPORT jlong __jlongpointer JNICALL Java_jdd_JDDNode_DDN_1GetThen(JNIEnv *env, jclass cls, jlong __jlongpointer dd) { - return ptr_to_jlong(Cudd_T(jlong_to_DdNode(dd))); + DdNode *node = jlong_to_DdNode(dd); + if (Cudd_IsConstant(node)) return ptr_to_jlong(NULL); + return ptr_to_jlong(Cudd_T(node)); } //------------------------------------------------------------------------------ @@ -815,7 +817,9 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_jdd_JDDNode_DDN_1GetThen(JNIEnv *env JNIEXPORT jlong __jlongpointer JNICALL Java_jdd_JDDNode_DDN_1GetElse(JNIEnv *env, jclass cls, jlong __jlongpointer dd) { - return ptr_to_jlong(Cudd_E(jlong_to_DdNode(dd))); + DdNode *node = jlong_to_DdNode(dd); + if (Cudd_IsConstant(node)) return ptr_to_jlong(NULL); + return ptr_to_jlong(Cudd_E(node)); } //============================================================================== diff --git a/prism/src/jdd/JDDNode.java b/prism/src/jdd/JDDNode.java index 6670ef35..3d48d4bd 100644 --- a/prism/src/jdd/JDDNode.java +++ b/prism/src/jdd/JDDNode.java @@ -91,6 +91,8 @@ public class JDDNode assert !this.isConstant(); // just return the node, even if DebugJDD is enabled + // DDN_GetThen will return NULL if the current node is a + // constant, raising an Exception in the JDDNode constructor return new JDDNode(DDN_GetThen(ptr)); } @@ -106,7 +108,9 @@ public class JDDNode assert !this.isConstant(); // just return the node, even if DebugJDD is enabled - return new JDDNode(DDN_GetElse(ptr)); + // DDN_GetElse will return NULL if the current node is a + // constant, raising an Exception in the JDDNode constructor + return new JDDNode(DDN_GetElse(ptr)); } public boolean equals(Object o)