Version abc80702

24 files changed, 141 insertions, 144 deletions

diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
index 84d1e97b..a27e994f 100644
--- a/src/bdd/cas/casCore.c
+++ b/src/bdd/cas/casCore.c
@@ -459,16 +459,16 @@ void Experiment2( BFunc * pFunc )
 ////////////////////////////////////////////////////////////////////////
 
 // the bit count for the first 256 integer numbers
-static unsigned char BitCount8[256] = {
-    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
-    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
-};
+//static unsigned char BitCount8[256] = {
+//    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+//    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+//    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+//    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+//    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+//    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+//    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+//    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+//};
 
 /////////////////////////////////////////////////////////////
 static int s_SuppSize[MAXOUTPUTS];
@@ -605,7 +605,6 @@ DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, in
 
     DdNode * bSupp, * bTemp;
     int i, Counter;
-    int nSuppPrev = -1;
     DdNode * bFunc;
     DdNode * aFunc;
 
@@ -669,7 +668,6 @@ DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutput
 
     DdNode * bSupp, * bTemp;
     int i, v, Counter;
-    int nSuppPrev = -1;
     DdNode * bFunc;
 
     // these are in the new manager
diff --git a/src/bdd/cudd/cuddAddIte.c b/src/bdd/cudd/cuddAddIte.c
index 71f8070f..bcfae83a 100644
--- a/src/bdd/cudd/cuddAddIte.c
+++ b/src/bdd/cudd/cuddAddIte.c
@@ -421,7 +421,7 @@ cuddAddIteRecur(
     DdNode *one,*zero;
     DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
     unsigned int topf,topg,toph,v;
-    int index;
+    int index = 0; // Suppress "might be used uninitialized"
 
     statLine(dd);
     /* Trivial cases. */
diff --git a/src/bdd/cudd/cuddAddWalsh.c b/src/bdd/cudd/cuddAddWalsh.c
index c6a67e34..90a57b3c 100644
--- a/src/bdd/cudd/cuddAddWalsh.c
+++ b/src/bdd/cudd/cuddAddWalsh.c
@@ -271,7 +271,8 @@ addWalshInt(
   int  n)
 {
     DdNode *one, *minusone;
-    DdNode *t, *u, *t1, *u1, *v, *w;
+    DdNode *t = NULL; // Suppress "might be used uninitialized"
+    DdNode *u, *t1, *u1, *v, *w;
     int     i;
 
     one = DD_ONE(dd);
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index b44e40de..672d6344 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -572,7 +572,7 @@ cuddBddIteRecur(
     DdNode     *one, *zero, *res;
     DdNode     *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
     unsigned int topf, topg, toph, v;
-    int         index;
+    int         index = 0; // Suppress "might be used uninitialized"
     int         comple;
 
     statLine(dd);
diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c
index 4fde7392..35a77b8c 100644
--- a/src/bdd/cudd/cuddDecomp.c
+++ b/src/bdd/cudd/cuddDecomp.c
@@ -1662,7 +1662,8 @@ BuildConjuncts(
   st_table * mintermTable)
 {
     int topid, distance;
-    Conjuncts *factorsNv, *factorsNnv, *factors;
+    Conjuncts *factorsNv = NULL, *factorsNnv = NULL; // Suppress "might be used uninitialized"
+    Conjuncts *factors;
     Conjuncts *dummy;
     DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv;
     double minNv = 0.0, minNnv = 0.0;
diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c
index 81c05d2c..fbf8b6dd 100644
--- a/src/bdd/cudd/cuddGroup.c
+++ b/src/bdd/cudd/cuddGroup.c
@@ -1455,7 +1455,7 @@ ddGroupMove(
     Move *move;
     int  size;
     int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
-    int  swapx,swapy;
+    int  swapx=-1,swapy=-1; // Suppress "might be used uninitialized"
 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
     int  initialSize,bestSize;
 #endif
@@ -1635,7 +1635,7 @@ ddGroupSiftingBackward(
 {
     Move *move;
     int  res;
-    Move *end_move;
+    Move *end_move = NULL;
     int diff, tmp_diff;
     int index, pairlev;
 
diff --git a/src/bdd/cudd/cuddHarwell.c b/src/bdd/cudd/cuddHarwell.c
index 063f1922..59394ce4 100644
--- a/src/bdd/cudd/cuddHarwell.c
+++ b/src/bdd/cudd/cuddHarwell.c
@@ -113,7 +113,7 @@ Cudd_addHarwell(
     DdNode *cubex, *cubey, *minterm1;
     int u, v, err, i, j, nv;
     double val;
-    DdNode **lx, **ly, **lxn, **lyn;    /* local copies of x, y, xn, yn_ */
+    DdNode **lx = NULL, **ly = NULL, **lxn = NULL, **lyn = NULL;    /* local copies of x, y, xn, yn_ */ /* Suppress "might be used uninitialized */
     int lnx, lny;            /* local copies of nx and ny */
     char title[73], key[9], mxtype[4], rhstyp[4];
     int totcrd, ptrcrd, indcrd, valcrd, rhscrd,
diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c
index 7f6b3678..95624a9e 100644
--- a/src/bdd/cudd/cuddLinear.c
+++ b/src/bdd/cudd/cuddLinear.c
@@ -836,7 +836,7 @@ cuddLinearInPlace(
     int    posn;
     int    isolated;
     DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
-    DdNode *g,*next,*last;
+    DdNode *g,*next,*last = NULL; // Suppress "might be used uninitialized"
     DdNodePtr *previousP;
     DdNode *tmp;
     DdNode *sentinel = &(table->sentinel);
diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c
index 788fc712..2895fa0b 100644
--- a/src/bdd/cudd/cuddPriority.c
+++ b/src/bdd/cudd/cuddPriority.c
@@ -937,7 +937,8 @@ cuddCProjectionRecur(
 {
     DdNode *res, *res1, *res2, *resA;
     DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha;
-    unsigned int topR, topY, top, index;
+    unsigned int topR, topY, top;
+    unsigned int index = 0; // Suppress "might be used uninitialized"
     DdNode *one = DD_ONE(dd);
 
     statLine(dd);
diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c
index 1387196f..4e62ce34 100644
--- a/src/bdd/cudd/cuddReorder.c
+++ b/src/bdd/cudd/cuddReorder.c
@@ -577,7 +577,7 @@ cuddSwapping(
     int    iterate;
     int previousSize;
     Move *moves, *move;
-    int    pivot;
+    int    pivot = 0; // Suppress "might be used uninitialized"
     int    modulo;
     int result;
 
@@ -2005,7 +2005,7 @@ ddUpdateMtrTree(
   int * invperm)
 {
     int    i, size, index, level;
-    int    minLevel, maxLevel, minIndex;
+    int    minLevel = table->size, maxLevel = 0, minIndex = 0; // Suppress "might be used uninitialized"
 
     if (treenode == NULL) return(1);
 
diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c
index 55ee3470..e3d39a0e 100644
--- a/src/bdd/cudd/cuddSubsetSP.c
+++ b/src/bdd/cudd/cuddSubsetSP.c
@@ -1224,12 +1224,14 @@ BuildSubsetBdd(
 {
     DdNode *N, *Nv, *Nnv;
     DdNode *ThenBranch, *ElseBranch, *childBranch;
-    DdNode *child, *regChild, *regNnv, *regNv;
+    DdNode *child, *regChild;
+    DdNode *regNnv = NULL, *regNv = NULL; // Suppress "might be used uninitialized"
     NodeDist_t *nodeStatNv, *nodeStat, *nodeStatNnv;
     DdNode *neW, *topv, *regNew;
     char *entry;
     unsigned int topid;
-    unsigned int childPathLength, oddLen, evenLen, NnvPathLength, NvPathLength;
+    unsigned int childPathLength, oddLen, evenLen;
+    unsigned int NnvPathLength = -1, NvPathLength = -1; // Suppress "might be used uninitialized"
     unsigned int NvBotDist, NnvBotDist;
     int tiebreakChild;
     int  processingDone, thenDone, elseDone;
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index e5488b17..aef6abc6 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -1445,10 +1445,10 @@ ddSymmGroupMove(
   Move ** moves)
 {
     Move *move;
-    int     size;
+    int     size = 0; // Suppress "might be used uninitialized"
     int  i,j;
     int  xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
-    int  swapx,swapy;
+    int  swapx = 0,swapy = 0; // Suppress "might be used uninitialized"
 
 #if DD_DEBUG
     assert(x < y);    /* we assume that x < y */
@@ -1524,7 +1524,7 @@ ddSymmGroupMoveBackward(
   int  x,
   int  y)
 {
-    int    size;
+    int    size = 0; // Suppress "might be used uninitialized"
     int i,j;
     int    xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
 
diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c
index 7f14aed1..458f19e6 100644
--- a/src/bdd/cudd/cuddTable.c
+++ b/src/bdd/cudd/cuddTable.c
@@ -1768,7 +1768,8 @@ cuddInsertSubtables(
     int oldsize,newsize;
     int i,j,index,reorderSave;
     unsigned int numSlots = unique->initSlots;
-    int *newperm, *newinvperm, *newmap;
+    int *newperm, *newinvperm;
+    int *newmap = NULL; // Suppress "might be used uninitialized"
     DdNode *one, *zero;
 
 #ifdef DD_DEBUG
@@ -2499,7 +2500,8 @@ ddResizeTable(
     int oldsize,newsize;
     int i,j,reorderSave;
     int numSlots = unique->initSlots;
-    int *newperm, *newinvperm, *newmap;
+    int *newperm, *newinvperm;
+    int *newmap = NULL; // Suppress "might be used uninitialized"
     DdNode *one, *zero;
 
     oldsize = unique->size;
diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c
index d5fa18e2..bc1a17eb 100644
--- a/src/bdd/cudd/cuddUtil.c
+++ b/src/bdd/cudd/cuddUtil.c
@@ -1357,7 +1357,8 @@ Cudd_bddPickArbitraryMinterms(
     DdNode **old, *neW;
     double minterms;
     char *saveString;
-    int saveFlag, savePoint, isSame;
+    int saveFlag, isSame;
+    int savePoint = 0; // Suppress "might be used uninitialized"
 
     minterms = Cudd_CountMinterm(dd,f,n);
     if ((double)k > minterms) {
diff --git a/src/bdd/cudd/cuddZddGroup.c b/src/bdd/cudd/cuddZddGroup.c
index 621fa43f..c26ea533 100644
--- a/src/bdd/cudd/cuddZddGroup.c
+++ b/src/bdd/cudd/cuddZddGroup.c
@@ -1060,7 +1060,7 @@ zddGroupMove(
     Move *move;
     int  size;
     int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
-    int  swapx,swapy;
+    int  swapx = 0,swapy = 0; // Suppress "might be used uninitialized"
 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
     int  initialSize,bestSize;
 #endif
diff --git a/src/bdd/cudd/cuddZddReord.c b/src/bdd/cudd/cuddZddReord.c
index e2da37f2..6e7d3438 100644
--- a/src/bdd/cudd/cuddZddReord.c
+++ b/src/bdd/cudd/cuddZddReord.c
@@ -464,7 +464,8 @@ cuddZddSwapInPlace(
     int        i;
     int        posn;
     DdNode    *f, *f1, *f0, *f11, *f10, *f01, *f00;
-    DdNode    *newf1, *newf0, *next;
+    DdNode    *newf1 = NULL; // Suppress "might be used uninitialized"
+    DdNode      *newf0, *next;
     DdNodePtr    g, *lastP, *previousP;
 
 #ifdef DD_DEBUG
@@ -725,7 +726,7 @@ cuddZddSwapping(
     int iterate;
     int previousSize;
     Move *moves, *move;
-    int    pivot;
+    int    pivot = -1; // Suppress "might be used uninitialized"
     int modulo;
     int result;
 
diff --git a/src/bdd/cudd/cuddZddSymm.c b/src/bdd/cudd/cuddZddSymm.c
index 54019892..0930e077 100644
--- a/src/bdd/cudd/cuddZddSymm.c
+++ b/src/bdd/cudd/cuddZddSymm.c
@@ -1459,7 +1459,7 @@ zdd_group_move(
     Move    *move;
     int        size;
     int        i, temp, gxtop, gxbot, gytop, gybot, yprev;
-    int        swapx, swapy;
+    int        swapx = 0, swapy = 0; // Suppress "might be used uninitialized"
 
 #ifdef DD_DEBUG
     assert(x < y);    /* we assume that x < y */
@@ -1563,7 +1563,7 @@ zdd_group_move_backward(
   int  x,
   int  y)
 {
-    int           size;
+    int           size = -1; // Suppress "might be used uninitialized"
     int        i, temp, gxtop, gxbot, gytop, gybot, yprev;
 
 #ifdef DD_DEBUG
diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c
index 58b824d2..ce466a71 100644
--- a/src/bdd/dsd/dsdCheck.c
+++ b/src/bdd/dsd/dsdCheck.c
@@ -183,7 +183,7 @@ int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF
          pCache->pTable[HKey].bX[3] == bC2 )
     {
         pCache->nSuccess++;
-        return (int)pCache->pTable[HKey].bX[4]; // the last bit records the result (yes/no)
+        return (int)(PORT_PTRUINT_T)pCache->pTable[HKey].bX[4]; // the last bit records the result (yes/no)
     }
     else
     {
@@ -302,7 +302,7 @@ int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF
         // set cache
         for ( i = 0; i < 4; i++ )
             pCache->pTable[HKey].bX[i] = bA[i];
-        pCache->pTable[HKey].bX[4] = (DdNode*)RetValue;
+        pCache->pTable[HKey].bX[4] = (DdNode*)(PORT_PTRUINT_T)RetValue;
 
         return RetValue;
     }
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c
index 543ad387..45c0986f 100644
--- a/src/bdd/dsd/dsdProc.c
+++ b/src/bdd/dsd/dsdProc.c
@@ -48,27 +48,21 @@ static int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * p
 static int s_Mark;
 
 // debugging flag
-static int s_Show = 0;
+//static int s_Show = 0;
 // temporary var used for debugging
 static int Depth = 0;
 
 static int s_Loops1;
 static int s_Loops2;
 static int s_Loops3;
-static int s_Pivot;
-static int s_PivotNo;
 static int s_Common;
 static int s_CommonNo;
 
 static int s_Case4Calls;
 static int s_Case4CallsSpecial;
 
-static int s_Case5;
-static int s_Loops2Useless;
-
-
-static int s_DecNodesTotal;
-static int s_DecNodesUsed;
+//static int s_Case5;
+//static int s_Loops2Useless;
 
 // statistical variables
 static int   s_nDecBlocks;
@@ -76,10 +70,6 @@ static int   s_nLiterals;
 static int   s_nExorGates; 
 static int   s_nReusedBlocks;
 static int   s_nCascades;
-static float s_nArea;    
-static float s_MaxDelay;
-static long  s_Time;
-static int   s_nInvertors;
 static int   s_nPrimeBlocks;
 
 static int HashSuccess = 0;
@@ -451,14 +441,14 @@ if ( s_Show )
     if ( fContained )
     {
         Dsd_Node_t * pSmall, * pLarge;
-        int c, iCompLarge; // the number of the component is Large is equal to the whole of Small
+        int c, iCompLarge = -1; // the number of the component is Large is equal to the whole of Small; suppress "might be used uninitialized"
         int fLowIsLarge;
 
         DdNode * bFTemp;     // the changed input function
         Dsd_Node_t * pDETemp, * pDENew;
 
         Dsd_Node_t * pComp = NULL;
-        int  nComp;
+        int  nComp = -1; // Suppress "might be used uninitialized"
 
         if ( pSmallR == pLR )
         { // Low is Small => High is Large
@@ -495,7 +485,7 @@ if ( s_Show )
             // as discribed in the previous example.
 
             // find the component, which when substituted for 0 or 1, produces the desired result
-            int g, fFoundComp; // {0,1} depending on whether setting cofactor to 0 or 1 worked out
+            int g, fFoundComp = -1; // {0,1} depending on whether setting cofactor to 0 or 1 worked out; suppress "might be used uninitialized"
 
             DdNode * bLarge, * bSmall;
             if ( fLowIsLarge )
@@ -575,7 +565,7 @@ if ( s_Show )
 
             // try to find a group of common components
             if ( pLargeR->Type == pSmallR->Type &&
-                (pLargeR->Type == DSD_NODE_EXOR || pSmallR->Type == DSD_NODE_OR&& ((pLarge==pLargeR) == (pSmall==pSmallR))) )
+                (pLargeR->Type == DSD_NODE_EXOR || (pSmallR->Type == DSD_NODE_OR && ((pLarge==pLargeR) == (pSmall==pSmallR)))) )
             {
                 Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; 
                 int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLargeR, pSmallR, &pCommon, &pLastDiffL, &pLastDiffH );
@@ -618,12 +608,12 @@ if ( s_Show )
                     //              <>    <> .......<=>... /..|..<> | 
                     //             /        \             /   |    \|
                     //          [OR]        [C]          S1   S2    C 
-                    //          /  \
-                    //        <>    \
-                    //       /       \
-                    //     [OR]      [x]
-                    //     /  \
-                    //    S1   S2
+                    //          /  \      .
+                    //        <>    \     .
+                    //       /       \    .
+                    //     [OR]      [x]  .
+                    //     /  \           .
+                    //    S1   S2         .
                     //
 
 
@@ -673,12 +663,12 @@ if ( s_Show )
                 //              /     \                /  |  \  | 
                 //             /        \             /   |    \|
                 //          [OR]        [C]          S1   S2    C 
-                //          /  \
-                //        <>    \
-                //       /       \
-                //    [XOR]      [x]
-                //     /  \
-                //    S1   S2
+                //          /  \     .
+                //        <>    \    .
+                //       /       \   .
+                //    [XOR]      [x] .
+                //     /  \          .
+                //    S1   S2        .
                 //
 
                 assert( fComp2 == 0 );
@@ -740,7 +730,7 @@ if ( s_Show )
     // and if they are PRIME, their dec numbers should be the same
     if ( pLR->Type == pHR->Type && 
          pLR->Type != DSD_NODE_BUF &&           
-        (pLR->Type != DSD_NODE_OR    || ( pL == pLR && pH == pHR || pL != pLR && pH != pHR ) ) &&
+        (pLR->Type != DSD_NODE_OR    || ( (pL == pLR && pH == pHR) || (pL != pLR && pH != pHR) ) ) &&
         (pLR->Type != DSD_NODE_PRIME || pLR->nDecs == pHR->nDecs)  )
     {
         // array to store common comps in pL and pH
@@ -947,7 +937,8 @@ if ( s_Show )
     int nEntries = 0;
 
     DdNode * SuppL, * SuppH, * SuppL_init, * SuppH_init;
-    Dsd_Node_t *pHigher, *pLower, * pTemp, * pDENew;
+    Dsd_Node_t *pHigher = NULL; // Suppress "might be used uninitialized"
+        Dsd_Node_t *pLower, * pTemp, * pDENew;
 
 
     int levTopSuppL;
@@ -1146,7 +1137,7 @@ if ( s_Show )
                     pMarkedLeft[ nMarkedLeft ] = pTempL;
                     pMarkedPols[ nMarkedLeft ] = fPolarity;
                     nMarkedLeft++;
-                } while ( pTempL = dsdKernelFindContainingComponent( pDsdMan, pTempL, bVarTop, &fPolarity ) );
+                } while ( (pTempL = dsdKernelFindContainingComponent( pDsdMan, pTempL, bVarTop, &fPolarity )) );
 
                 // go over the dec list of pH, and find the component that is marked and the previos one
                 // (such component always exists, because they have common variables)
@@ -1431,7 +1422,8 @@ int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd
 void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor )
 {
     DdManager * dd = pDsdMan->dd;
-    DdNode * bF, * bS, * bFadd, * bTemp;
+    DdNode * bF, * bFadd, * bTemp;
+        DdNode * bS = NULL; // Suppress "might be used uninitialized"
     Dsd_Node_t * pDE, * pDER;
     int i;
 
@@ -1565,7 +1557,6 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
 {
     DdManager * dd = pDsdMan->dd;
     Dsd_Node_t * pR    = Dsd_Regular(pDE);
-    int fCompP = (int)( pDE != pR );
     int RetValue;
 
     DdNode * bRes;
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index 2855d68d..5d69f2f4 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -38,11 +38,6 @@ static void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char
 static int s_DepthMax;
 static int s_GateSizeMax;
 
-static int s_CounterBlocks;
-static int s_CounterPos;
-static int s_CounterNeg;
-static int s_CounterNo;
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -1009,7 +1004,6 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR
 {
     DdNode * bCof0,  * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp;
     int i;
-    int fAllBuffs = 1;
     static int Permute[MAXINPUTS];
 
     assert( pNode );
diff --git a/src/bdd/parse/parseCore.c b/src/bdd/parse/parseCore.c
index eb89b3e3..0071fb5a 100644
--- a/src/bdd/parse/parseCore.c
+++ b/src/bdd/parse/parseCore.c
@@ -120,7 +120,8 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
     char * pTemp;
     int nParans, fFound, Flag;
     int Oper, Oper1, Oper2;
-    int i, v, fLower;
+    int i, fLower;
+    int v = -1; // Suppress "might be used uninitialized"
 
     // make sure that the number of vars and ranks is correct
     if ( nVars * (nRanks + 1) > dd->size )
diff --git a/src/bdd/reo/reoSwap.c b/src/bdd/reo/reoSwap.c
index 4afa650c..d3a9c7a5 100644
--- a/src/bdd/reo/reoSwap.c
+++ b/src/bdd/reo/reoSwap.c
@@ -47,7 +47,8 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
     // the new nodes on lev0
     reo_unit * pLoop, * pUnit;
     // the new nodes on lev1
-    reo_unit * pNewPlane20, * pNewPlane21, * pNewPlane20R;
+    reo_unit * pNewPlane20 = NULL, * pNewPlane21 = NULL; // Suppress "might be used uninitialized"
+        reo_unit * pNewPlane20R;
     reo_unit * pUnitE, * pUnitER, * pUnitT;
     // the nodes below lev1
     reo_unit * pNew1E, * pNew1T, * pNew2E, * pNew2T;
@@ -60,18 +61,19 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
     reo_unit * pListNew1 = NULL, ** ppListNew1 = &pListNew1; 
     reo_unit * pListTemp = NULL, ** ppListTemp = &pListTemp; 
     // various integer variables
-    int fComp, fCompT, fFound, nWidthCofs, HKey, fInteract, temp, c;
+    int fComp, fCompT, fFound, HKey, fInteract, temp, c;
+        int nWidthCofs = -1; // Suppress "might be used uninitialized"
     // statistical variables
     int nNodesUpMovedDown  = 0;
     int nNodesDownMovedUp  = 0;
     int nNodesUnrefRemoved = 0;
     int nNodesUnrefAdded   = 0;
     int nWidthReduction    = 0;
-    double AplWeightTotalLev0;
-    double AplWeightTotalLev1;
-    double AplWeightHalf;
-    double AplWeightPrev;
-    double AplWeightAfter;
+    double AplWeightTotalLev0 = 0.0; // Suppress "might be used uninitialized"
+    double AplWeightTotalLev1 = 0.0; // Suppress "might be used uninitialized"
+    double AplWeightHalf      = 0.0; // Suppress "might be used uninitialized"
+    double AplWeightPrev      = 0.0; // Suppress "might be used uninitialized"
+    double AplWeightAfter     = 0.0; // Suppress "might be used uninitialized"
     double nCostGain;     
 
     // set the old lists
@@ -248,14 +250,14 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
         {
             //                before                        after
             //
-            //                 <p1>           
-            //              0 /    \ 1         
-            //               /      \          
-            //              /        \         
-            //             /          \                     <p2n>   
-            //            /            \                  0 /  \ 1 
-            //           /              \                  /    \  
-            //          /                \                /      \ 
+            //                 <p1>                                 .
+            //              0 /    \ 1                              .
+            //               /      \                               .
+            //              /        \                              .
+            //             /          \                     <p2n>   .
+            //            /            \                  0 /  \ 1  .
+            //           /              \                  /    \   .
+            //          /                \                /      \  .
             //         F0                F1              F0      F1
 
             // move to plane-2-new
@@ -333,15 +335,15 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             {
                 //                before                        after
                 //
-                //                 <p1>                          <p1n>
-                //              0 /    \ 1                    0 /    \ 1            
-                //               /      \                      /      \           
-                //              /        \                    /        \         
-                //           <p2>        <p2>              <p2n>       <p2n>          
-                //        0 /   \ 1    0 /  \ 1          0 /  \ 1    0 /   \ 1    
-                //         /     \      /    \            /    \      /     \   
-                //        /       \    /      \          /      \    /       \   
-                //       F0       F1  F2      F3        F0      F2  F1       F3  
+                //                 <p1>                          <p1n>              .
+                //              0 /    \ 1                    0 /    \ 1            .
+                //               /      \                      /      \             .
+                //              /        \                    /        \            .
+                //           <p2>        <p2>              <p2n>       <p2n>        .
+                //        0 /   \ 1    0 /  \ 1          0 /  \ 1    0 /   \ 1      .
+                //         /     \      /    \            /    \      /     \       .
+                //        /       \    /      \          /      \    /       \      .
+                //       F0       F1  F2      F3        F0      F2  F1       F3     .
                 //                                 pNew1E   pNew1T  pNew2E   pNew2T
                 //
                 pNew1E = pUnitE->pE;   // F0
@@ -354,15 +356,15 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             {
                 //                before                        after
                 //
-                //                 <p1>                          <p1n>
-                //              0 .    \ 1                    0 /    \ 1            
-                //               .      \                      /      \           
-                //              .        \                    /        \         
-                //           <p2>        <p2>              <p2n>       <p2n>          
-                //        0 /   \ 1    0 /  \ 1          0 .  \ 1    0 .   \ 1    
-                //         /     \      /    \            .    \      .     \   
-                //        /       \    /      \          .      \    .       \   
-                //       F0       F1  F2      F3        F0      F2  F1       F3  
+                //                 <p1>                          <p1n>           .
+                //              0 .    \ 1                    0 /    \ 1         .
+                //               .      \                      /      \          .
+                //              .        \                    /        \         .
+                //           <p2>        <p2>              <p2n>       <p2n>     .
+                //        0 /   \ 1    0 /  \ 1          0 .  \ 1    0 .   \ 1   .
+                //         /     \      /    \            .    \      .     \    .
+                //        /       \    /      \          .      \    .       \   .
+                //       F0       F1  F2      F3        F0      F2  F1       F3  .
                 //                                 pNew1E   pNew1T  pNew2E   pNew2T
                 //
                 pNew1E = Unit_Not(pUnitER->pE);  // F0
@@ -389,15 +391,15 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             {
                 //                before                        after
                 //
-                //                 <p1>                          <p1n>
-                //              0 /    \ 1                    0 /    \ 1            
-                //               /      \                      /      \           
-                //              /        \                    /        \         
-                //           <p2>         \               <p2n>       <p2n>           
-                //        0 /   \ 1        \            0 /  \ 1    0 /   \ 1    
-                //         /     \          \            /    \      /     \   
-                //        /       \          \          /      \    /       \   
-                //       F0       F1         F3        F0      F3  F1       F3  
+                //                 <p1>                          <p1n>          .
+                //              0 /    \ 1                    0 /    \ 1        .
+                //               /      \                      /      \         .
+                //              /        \                    /        \        .
+                //           <p2>         \               <p2n>       <p2n>     .
+                //        0 /   \ 1        \            0 /  \ 1    0 /   \ 1   .
+                //         /     \          \            /    \      /     \    .
+                //        /       \          \          /      \    /       \   .
+                //       F0       F1         F3        F0      F3  F1       F3  .
                 //                                 pNew1E   pNew1T  pNew2E   pNew2T
                 //
                 pNew1E = pUnitER->pE;      // F0
@@ -410,15 +412,15 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             {
                 //                before                        after
                 //
-                //                 <p1>                          <p1n>
-                //              0 .    \ 1                    0 /    \ 1            
-                //               .      \                      /      \           
-                //              .        \                    /        \         
-                //           <p2>         \                <p2n>       <p2n>          
-                //        0 /   \ 1        \            0 .  \ 1    0 .   \ 1    
-                //         /     \          \            .    \      .     \   
-                //        /       \          \          .      \    .       \   
-                //       F0       F1         F3        F0      F3  F1       F3  
+                //                 <p1>                          <p1n>          .
+                //              0 .    \ 1                    0 /    \ 1        .
+                //               .      \                      /      \         .
+                //              .        \                    /        \        .
+                //           <p2>         \                <p2n>       <p2n>    .
+                //        0 /   \ 1        \            0 .  \ 1    0 .   \ 1   .
+                //         /     \          \            .    \      .     \    .
+                //        /       \          \          .      \    .       \   .
+                //       F0       F1         F3        F0      F3  F1       F3  .
                 //                                 pNew1E   pNew1T  pNew2E   pNew2T
                 //
                 pNew1E = Unit_Not(pUnitER->pE);  // F0
@@ -443,15 +445,15 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
         {
             //                before                        after
             //
-            //                 <p1>                          <p1n>
-            //              0 /    \ 1                    0 /    \ 1            
-            //               /      \                      /      \           
-            //              /        \                    /        \         
-            //             /         <p2>              <p2n>       <p2n>            
-            //            /       0 /   \ 1          0 /  \ 1    0 /   \ 1    
-            //           /         /     \            /    \      /     \   
-            //          /         /       \          /      \    /       \   
-            //         F0        F2       F3        F0      F2  F0       F3  
+            //                 <p1>                          <p1n>           .
+            //              0 /    \ 1                    0 /    \ 1         .
+            //               /      \                      /      \          .
+            //              /        \                    /        \         .
+            //             /         <p2>              <p2n>       <p2n>     .
+            //            /       0 /   \ 1          0 /  \ 1    0 /   \ 1   .
+            //           /         /     \            /    \      /     \    .
+            //          /         /       \          /      \    /       \   .
+            //         F0        F2       F3        F0      F2  F0       F3  .
             //                                 pNew1E   pNew1T  pNew2E   pNew2T
             //
             pNew1E =     pUnitE;    // F0
diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
index 65d31d01..26a6689e 100644
--- a/src/bdd/reo/reoTransfer.c
+++ b/src/bdd/reo/reoTransfer.c
@@ -41,7 +41,8 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
 {
     DdManager * dd = p->dd;
     reo_unit * pUnit;
-    int HKey, fComp;
+    int HKey = -1; // Suppress "might be used uninitialized"
+        int fComp;
     
     fComp = Cudd_IsComplement(F);
     F = Cudd_Regular(F);
@@ -68,7 +69,7 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
     if ( cuddIsConstant(F) )
     {
         pUnit->lev    = REO_CONST_LEVEL;
-        pUnit->pE     = (reo_unit*)((int)(cuddV(F)));
+        pUnit->pE     = (reo_unit*)((int)(PORT_PTRUINT_T)(cuddV(F)));
         pUnit->pT     = NULL;
         // check if the diagram that is being reordering has complement edges
         if ( F != dd->one )
@@ -117,7 +118,8 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
 {
     DdManager * dd = p->dd;
     DdNode * bRes, * E, * T;
-    int HKey, fComp;
+    int HKey = -1; // Suppress "might be used uninitialized"
+        int fComp;
 
     fComp = Cudd_IsComplement(pUnit);
     pUnit = Unit_Regular(pUnit);
@@ -137,7 +139,7 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
     // treat the case of constants
     if ( Unit_IsConstant(pUnit) )
     {
-        bRes = cuddUniqueConst( dd, ((double)((int)(pUnit->pE))) );
+        bRes = cuddUniqueConst( dd, ((double)((int)(PORT_PTRUINT_T)(pUnit->pE))) );
         cuddRef( bRes );
     }
     else
diff --git a/src/bdd/reo/reoUnits.c b/src/bdd/reo/reoUnits.c
index aa86516e..52137027 100644
--- a/src/bdd/reo/reoUnits.c
+++ b/src/bdd/reo/reoUnits.c
@@ -84,7 +84,7 @@ void reoUnitsRecycleUnit( reo_man * p, reo_unit * pUnit )
 void reoUnitsRecycleUnitList( reo_man * p, reo_plane * pPlane )
 {
     reo_unit * pUnit;
-    reo_unit * pTail;
+    reo_unit * pTail = NULL; // Suppress "might be used uninitialized"
 
     if ( pPlane->pHead == NULL )
         return;