From ef2d15c256d810bb66529d34104df7cd0f77de19 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 7 Jun 2016 10:17:46 +0000 Subject: [PATCH] JDDNode.getThen() / getElse(): reintroduce sanity check against asking constant nodes for then/else The check disappeared during refactoring to the ptrToNode functionality + minor whitespace + copyright git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11392 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jdd/JDDNode.java | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) diff --git a/prism/src/jdd/JDDNode.java b/prism/src/jdd/JDDNode.java index 1c3583ac..4ac51b8a 100644 --- a/prism/src/jdd/JDDNode.java +++ b/prism/src/jdd/JDDNode.java @@ -4,6 +4,7 @@ // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) // * Christian von Essen (VERIMAG) +// * Joachim Klein (TU Dresden) // //------------------------------------------------------------------------------ // @@ -88,12 +89,16 @@ public class JDDNode */ public JDDNode getThen() { - assert !this.isConstant(); - + long thenPtr = DDN_GetThen(ptr); + if (thenPtr == 0) { + if (isConstant()) { + throw new RuntimeException("Trying to access the 'then' child of a constant MTBDD node"); + } else { + throw new RuntimeException("getThen: CUDD returned NULL, but node is not a constant node. Out of memory or corrupted MTBDD?"); + } + } // 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)); + return new JDDNode(thenPtr); } /** @@ -105,15 +110,19 @@ public class JDDNode */ public JDDNode getElse() { - assert !this.isConstant(); - + long elsePtr = DDN_GetElse(ptr); + if (elsePtr == 0) { + if (isConstant()) { + throw new RuntimeException("Trying to access the 'else' child of a constant MTBDD node"); + } else { + throw new RuntimeException("getElse: CUDD returned NULL, but node is not a constant node. Out of memory or corrupted MTBDD?"); + } + } // just return the node, even if DebugJDD is enabled - // 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)); + return new JDDNode(elsePtr); } - public boolean equals(Object o) + public boolean equals(Object o) { return (o instanceof JDDNode) && (((JDDNode) o).ptr == ptr); }