From 958adc38ab800a8703687f60757ee33b9f3a0afe Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 15:12:34 +0000 Subject: [PATCH] IntegerVector: Check that number of states fit into int If the number of states is too large for the index of the vector to fit into a Java int throw a PrismNotSupportedException. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12023 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/dv/IntegerVector.java | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/prism/src/dv/IntegerVector.java b/prism/src/dv/IntegerVector.java index ce96d571..65246169 100644 --- a/prism/src/dv/IntegerVector.java +++ b/prism/src/dv/IntegerVector.java @@ -89,11 +89,17 @@ public class IntegerVector /** * Create a new IntegerVector from an existing MTBDD representation of an array. + *
[ DEREFS: none ] + * @throws PrismException if number of states is too large (uses Java int based indices) */ - public IntegerVector(JDDNode dd, JDDVars vars, ODDNode odd) + public IntegerVector(JDDNode dd, JDDVars vars, ODDNode odd) throws PrismException { + long numStates = odd.getEOff() + odd.getTOff(); + if (numStates > Integer.MAX_VALUE) { + throw new PrismNotSupportedException("Can not create IntegerVector with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states"); + } v = IV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr()); - n = (int)(odd.getEOff() + odd.getTOff()); + n = (int)numStates; } private native long IV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);