JDD: Throw CuddOfOutMemoryException for ptrToNode(NULL)

The native DD/CuDD methods return NULL to indicate that
an out-of-memory error in CuDD has occurred. Before, we
constructed a JDDNode for this NULL ptr, which would lead
to a SIGSEGV crash the next time any operation
(ref, deref, etc) would be performed on that JDDNode.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10472 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/include/JDD.h

@@ -667,3 +667,22 @@ JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToSpyFile
 }
 #endif
 #endif
+/* Header for class jdd_JDD_CuddOutOfMemoryException */
+
+#ifndef _Included_jdd_JDD_CuddOutOfMemoryException
+#define _Included_jdd_JDD_CuddOutOfMemoryException
+#ifdef __cplusplus
+extern "C" {
+#endif
+#undef jdd_JDD_CuddOutOfMemoryException_serialVersionUID
+#define jdd_JDD_CuddOutOfMemoryException_serialVersionUID -3042686055658047285LL
+#undef jdd_JDD_CuddOutOfMemoryException_serialVersionUID
+#define jdd_JDD_CuddOutOfMemoryException_serialVersionUID -3387516993124229948LL
+#undef jdd_JDD_CuddOutOfMemoryException_serialVersionUID
+#define jdd_JDD_CuddOutOfMemoryException_serialVersionUID -7034897190745766939LL
+#undef jdd_JDD_CuddOutOfMemoryException_serialVersionUID
+#define jdd_JDD_CuddOutOfMemoryException_serialVersionUID -3094099053041270477LL
+#ifdef __cplusplus
+}
+#endif
+#endif

prism/src/jdd/JDD.java

@@ -121,6 +121,23 @@ public class JDD
 	private static native void DD_ExportMatrixToMatlabFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, String name, String filename);
 	private static native void DD_ExportMatrixToSpyFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, int depth, String filename);
 
+	/**
+	 * An exception indicating that CuDD ran out of memory or that another internal error
+	 * occurred.
+	 * <br>
+	 * This exception is thrown by ptrToNode if a NULL pointer is returned by one of the native
+	 * DD methods. It is generally not safe to use the CuDD library after this error occurred,
+	 * so the program should quit as soon as feasible.
+	 */
+	public static class CuddOutOfMemoryException extends RuntimeException {
+		private static final long serialVersionUID = -3094099053041270477L;
+
+		/** Constructor */
+		CuddOutOfMemoryException() {
+			super("The MTBDD library CuDD seems to have run out of memory or encountered an internal error.");
+		}
+	}
+
 	static
 	{
 		try {
@@ -1336,10 +1353,14 @@ public class JDD
 
 	/**
 	 * Convert a (referenced) ptr returned from Cudd into a JDDNode.
+	 * <br>Throws a CuddOutOfMemoryException if the pointer is NULL.
 	 * <br>[ REFS: <i>none</i> ]
 	 */
 	public static JDDNode ptrToNode(long ptr)
 	{
+		if (ptr == 0L) {
+			throw new CuddOutOfMemoryException();
+		}
 		return new JDDNode(ptr);
 	}