From 9883fe5a1ddbc0c7a70eeb51758a78df6852068b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 15:13:23 +0000 Subject: [PATCH] iv.cc: convert indexing from long to int64_t Consistently use 64-bit index variables (to match size used for ODD offsets). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12025 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/dv/iv.cc | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/prism/src/dv/iv.cc b/prism/src/dv/iv.cc index e20514d5..8101bd63 100644 --- a/prism/src/dv/iv.cc +++ b/prism/src/dv/iv.cc @@ -28,11 +28,12 @@ #include "iv.h" #include #include +#include // local function prototypes -static void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, long n, int *res); -static DdNode *integer_vector_to_mtbdd_rec(DdManager *ddman, int *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); +static void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o, int64_t n, int *res); +static DdNode *integer_vector_to_mtbdd_rec(DdManager *ddman, int *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o); //------------------------------------------------------------------------------ @@ -51,7 +52,7 @@ EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars, EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd, int *res) { - long i, n; + int64_t i, n; // determine size n = odd->eoff + odd->toff; @@ -67,7 +68,7 @@ EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars, return res; } -void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, long n, int *res) +void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o, int64_t n, int *res) { DdNode *e, *t; @@ -102,7 +103,7 @@ EXPORT DdNode *integer_vector_to_mtbdd(DdManager *ddman, int *vec, DdNode **vars return integer_vector_to_mtbdd_rec(ddman, vec, vars, num_vars, 0, odd, 0); } -DdNode *integer_vector_to_mtbdd_rec(DdManager *ddman, int *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o) +DdNode *integer_vector_to_mtbdd_rec(DdManager *ddman, int *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o) { DdNode *e, *t;