From 2ea5de4d680ab90136ef22e19ab46398b8e58c7e Mon Sep 17 00:00:00 2001
From: Pav Lucistnik <pav@FreeBSD.org>
Date: Sat, 13 Dec 2003 01:22:09 +0000
Subject: Add The SMV (Symbolic Model Verifier), a tool for checking finite
 state systems against specifications the temporal logic CTL (Computational
 Tree Logic).

PR:		ports/59429
Submitted by:	Marc van Woerkom <marc.vanwoerkom@fernuni-hagen.de>
---
 devel/smv/files/patch-bdd.c | 51 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)
 create mode 100644 devel/smv/files/patch-bdd.c

(limited to 'devel/smv/files/patch-bdd.c')

diff --git a/devel/smv/files/patch-bdd.c b/devel/smv/files/patch-bdd.c
new file mode 100644
index 000000000000..512686ff0fcb
--- /dev/null
+++ b/devel/smv/files/patch-bdd.c
@@ -0,0 +1,51 @@
+--- bdd.c
++++ bdd.c
+@@ -113,7 +113,7 @@
+    /* Initialize a keytable. */
+    kp->n = n;
+    kp->elements_in_table = 0;
+-   kp->hash_table_buf = (bdd_ptr *)malloc(n*sizeof(bdd_ptr));
++   kp->hash_table_buf = (bdd_ptr *)smv_malloc(n*sizeof(bdd_ptr));
+ 
+    {  /* Initialize hash bin list pointers to NULL. */
+       register int i;
+@@ -139,7 +139,7 @@
+    /* Create key tables. */
+    create_keytable(&reduce_table, KEYTABLESIZE);
+    apply_cache_size = APPLY_CACHE_SIZE;
+-   apply_cache = (apply_rec *)malloc(sizeof(apply_rec)*apply_cache_size);
++   apply_cache = (apply_rec *)smv_malloc(sizeof(apply_rec)*apply_cache_size);
+    {
+      int i;
+      for(i=0;i<apply_cache_size;i++)apply_cache[i].op = 0;
+@@ -1446,7 +1446,7 @@
+ }
+ 
+ /* An "infinity" constant - big enough power of 2 not to care about */
+-#define INFINITY 1000
++#define SMV_INFINITY 1000
+ 
+ /* similar to auxcount_bdd, but computes log2 of the fraction */
+ 
+@@ -1457,18 +1457,18 @@
+   union {float a; bdd_ptr b;} temp;     /* very dangerous!!! */
+   double l,r;
+ 
+-  if(d==ZERO)return(-INFINITY); /* = log(0) */
++  if(d==ZERO)return(-SMV_INFINITY); /* = log(0) */
+   if(d==ONE)return(0.0);        /* = log2(1) */
+   temp.b = find_apply(COUNT_OP,d,ZERO);
+   if(temp.b==NULL) {
+     l = auxcount_bdd_log2(d->left,n);
+     r = auxcount_bdd_log2(d->right,n);
+     if(l < r) {
+-      if(r - l > INFINITY) temp.a = r;
++      if(r - l > SMV_INFINITY) temp.a = r;
+       else temp.a = l - 1.0 + log2(1.0 + pow(2.0,r-l));
+     }
+     else {
+-      if(l - r > INFINITY) temp.a = l;
++      if(l - r > SMV_INFINITY) temp.a = l;
+       else temp.a = r - 1.0 + log2(1.0 + pow(2.0,l-r));
+     }
+   }
-- 
cgit v1.2.3