diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-16 23:40:23 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-16 23:40:23 -0800 |
commit | 97856d021a1282cf3fb9a86701fff3ec403fe912 (patch) | |
tree | 7dbd5471eb417540ad39fa6079ac8c32a2e06222 /src/proof/llb | |
parent | 791b107e7a225103ee76c921c3c4a96d0e1adae2 (diff) | |
download | abc-97856d021a1282cf3fb9a86701fff3ec403fe912.tar.gz abc-97856d021a1282cf3fb9a86701fff3ec403fe912.tar.bz2 abc-97856d021a1282cf3fb9a86701fff3ec403fe912.zip |
Silencing some of the gcc warnings.
Diffstat (limited to 'src/proof/llb')
-rw-r--r-- | src/proof/llb/llb1Pivot.c | 2 | ||||
-rw-r--r-- | src/proof/llb/llb1Reach.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb1Sched.c | 2 | ||||
-rw-r--r-- | src/proof/llb/llb2Core.c | 6 | ||||
-rw-r--r-- | src/proof/llb/llb2Driver.c | 2 | ||||
-rw-r--r-- | src/proof/llb/llb2Flow.c | 8 | ||||
-rw-r--r-- | src/proof/llb/llb2Image.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb3Image.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb3Nonlin.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb4Cex.c | 2 | ||||
-rw-r--r-- | src/proof/llb/llb4Image.c | 6 | ||||
-rw-r--r-- | src/proof/llb/llb4Nonlin.c | 6 |
12 files changed, 25 insertions, 25 deletions
diff --git a/src/proof/llb/llb1Pivot.c b/src/proof/llb/llb1Pivot.c index d42bf659..688060bc 100644 --- a/src/proof/llb/llb1Pivot.c +++ b/src/proof/llb/llb1Pivot.c @@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START int Llb_ManTracePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pPivot ) { Aig_Obj_t * pFanout; - int k, iFan; + int k, iFan = -1; if ( Aig_ObjIsTravIdPrevious(p, pObj) ) return 0; if ( Aig_ObjIsTravIdCurrent(p, pObj) ) diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c index fbf91351..722a8342 100644 --- a/src/proof/llb/llb1Reach.c +++ b/src/proof/llb/llb1Reach.c @@ -465,7 +465,7 @@ Abc_Cex_t * Llb_ManReachDeriveCex( Llb_Man_t * p ) { Abc_Cex_t * pCex; Aig_Obj_t * pObj; - DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing; + DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing; int i, v, RetValue, nPiOffset; char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) ); assert( Vec_PtrSize(p->vRings) > 0 ); @@ -582,7 +582,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube; DdNode * bConstrCs, * bConstrNs; int clk2, clk = clock(), nIters, nBddSize = 0; - int nThreshold = 10000; +// int nThreshold = 10000; // compute time to stop p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0; diff --git a/src/proof/llb/llb1Sched.c b/src/proof/llb/llb1Sched.c index 6bdae42e..51de973a 100644 --- a/src/proof/llb/llb1Sched.c +++ b/src/proof/llb/llb1Sched.c @@ -80,7 +80,7 @@ void Llb_MtrSwapColumns( Llb_Mtr_t * p, int iCol1, int iCol2 ) int Llb_MtrFindBestColumn( Llb_Mtr_t * p, int iGrpStart ) { int Cost, Cost2, CostBest = ABC_INFINITY, Cost2Best = ABC_INFINITY; - int WeightCur, WeightBest = -ABC_INFINITY, iGrp, iGrpBest = -1; + int WeightCur, WeightBest = -ABC_INFINITY, iGrp = -1, iGrpBest = -1; int k, c, iVar, Counter; // find partition that reduces partial product as much as possible for ( iVar = 0; iVar < p->nRows - p->nFfs; iVar++ ) diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c index c15574c2..626acbd2 100644 --- a/src/proof/llb/llb2Core.c +++ b/src/proof/llb/llb2Core.c @@ -99,7 +99,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p ) Abc_Cex_t * pCex; Aig_Obj_t * pObj; Vec_Ptr_t * vSupps, * vQuant0, * vQuant1; - DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing; + DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing; int i, v, RetValue, nPiOffset; char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) ); assert( Vec_PtrSize(p->vRings) > 0 ); @@ -209,7 +209,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ int * pLoc2GloR = p->pPars->fBackward? Vec_IntArray( p->vNs2Glo ) : Vec_IntArray( p->vCs2Glo ); int * pGlo2Loc = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs ); DdNode * bCurrent, * bReached, * bNext, * bTemp; - int clk2, clk = clock(), nIters, nBddSize, iOutFail = -1; + int clk2, clk = clock(), nIters, nBddSize;//, iOutFail = -1; /* // compute time to stop if ( p->pPars->TimeLimit ) @@ -533,7 +533,7 @@ Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t { DdManager * dd; Vec_Ptr_t * vDdMans; - Vec_Ptr_t * vLower, * vUpper; + Vec_Ptr_t * vLower, * vUpper = NULL; int i; vDdMans = Vec_PtrStart( Vec_PtrSize(vResult) ); Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vResult, vLower, i ) diff --git a/src/proof/llb/llb2Driver.c b/src/proof/llb/llb2Driver.c index 041a39d5..4998b1ad 100644 --- a/src/proof/llb/llb2Driver.c +++ b/src/proof/llb/llb2Driver.c @@ -161,7 +161,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager ***********************************************************************/ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget ) { - int fVerbose = 1; +// int fVerbose = 1; DdManager * dd; DdNode * bVar1, * bVar2, * bProd, * bRes, * bTemp; Aig_Obj_t * pObj; diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c index ebb4e038..544d7c04 100644 --- a/src/proof/llb/llb2Flow.c +++ b/src/proof/llb/llb2Flow.c @@ -273,7 +273,7 @@ int Llb_ManCutLiNum( Aig_Man_t * p, Vec_Ptr_t * vMinCut ) { Aig_Obj_t * pFanout; Aig_Obj_t * pObj; - int i, k, iFanout, Counter = 0; + int i, k, iFanout = -1, Counter = 0; Vec_PtrForEachEntry( Aig_Obj_t *, vMinCut, pObj, i ) { if ( Aig_ObjIsPi(pObj) ) @@ -1018,7 +1018,7 @@ void Llb_ManFlowUnmarkCone( Aig_Man_t * p, Vec_Ptr_t * vCone ) void Llb_ManFlowCollectAndMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vCone ) { Aig_Obj_t * pFanout; - int i, iFanout; + int i, iFanout = -1; if ( Saig_ObjIsLi(p, pObj) ) return; if ( pObj->fMarkB ) @@ -1225,7 +1225,7 @@ Vec_Ptr_t * Llb_ManFlowFindBestCut( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryVerbose ) { int nVolMax = Aig_ManNodeNum(p) / Num; - Vec_Ptr_t * vResult, * vMinCut, * vLower, * vUpper; + Vec_Ptr_t * vResult, * vMinCut = NULL, * vLower, * vUpper; int i, k, nVol, clk = clock(); vResult = Vec_PtrAlloc( 100 ); Vec_PtrPush( vResult, Llb_ManComputeCutLo(p) ); @@ -1336,7 +1336,7 @@ void Llb_ManMinCutTest( Aig_Man_t * pAig, int Num ) extern void Llb_BddExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, Vec_Ptr_t * vMaps ); - int fVerbose = 1; +// int fVerbose = 1; Gia_ParLlb_t Pars, * pPars = &Pars; Vec_Ptr_t * vResult;//, * vSupps, * vMaps; Aig_Man_t * p; diff --git a/src/proof/llb/llb2Image.c b/src/proof/llb/llb2Image.c index 5baa5c57..99ffbdc4 100644 --- a/src/proof/llb/llb2Image.c +++ b/src/proof/llb/llb2Image.c @@ -121,7 +121,7 @@ Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vSt void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose ) { Vec_Int_t * vOne; - int nVarsAll, Counter, iSupp, Entry, i, k; + int nVarsAll, Counter, iSupp = -1, Entry, i, k; // start quantification arrays *pvQuant0 = Vec_PtrAlloc( Vec_PtrSize(vSupps) ); *pvQuant1 = Vec_PtrAlloc( Vec_PtrSize(vSupps) ); @@ -362,7 +362,7 @@ DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, int TimeTarget, int fBackward, int fReorder, int fVerbose ) { - int fCheckSupport = 0; +// int fCheckSupport = 0; DdManager * ddPart; DdNode * bImage, * bGroup, * bCube, * bTemp; int i, clk, clk0 = clock(); diff --git a/src/proof/llb/llb3Image.c b/src/proof/llb/llb3Image.c index f674d4b1..708af6d5 100644 --- a/src/proof/llb/llb3Image.c +++ b/src/proof/llb/llb3Image.c @@ -345,8 +345,8 @@ int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, Vec_Ptr_t * vSingles; DdNode * bCube, * bFunc; int i, RetValue, nSuppSize; - int iPart1 = pPart1->iPart; - int iPart2 = pPart2->iPart; +// int iPart1 = pPart1->iPart; +// int iPart2 = pPart2->iPart; // create cube to be quantified bCube = Llb_NonlinCreateCube2( p, pPart1, pPart2 ); Cudd_Ref( bCube ); diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c index 45f6f11e..d28edecc 100644 --- a/src/proof/llb/llb3Nonlin.c +++ b/src/proof/llb/llb3Nonlin.c @@ -247,7 +247,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) Abc_Cex_t * pCex; Aig_Obj_t * pObj; Vec_Int_t * vVarsNs; - DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing; + DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing; int i, v, RetValue, nPiOffset; char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) ); assert( Vec_PtrSize(p->vRings) > 0 ); @@ -428,7 +428,7 @@ int Llb_NonlinCompPerms( DdManager * dd, int * pVar2Lev ) int Llb_NonlinReachability( Llb_Mnn_t * p ) { DdNode * bTemp, * bNext; - int nIters, nBddSize0, nBddSize, NumCmp, Limit = p->pPars->nBddMax; + int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax; int clk2, clk3, clk = clock(); assert( Aig_ManRegNum(p->pAig) > 0 ); diff --git a/src/proof/llb/llb4Cex.c b/src/proof/llb/llb4Cex.c index a68be711..3a1c96e5 100644 --- a/src/proof/llb/llb4Cex.c +++ b/src/proof/llb/llb4Cex.c @@ -52,7 +52,7 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int sat_solver * pSat; Aig_Obj_t * pObj; unsigned * pNext, * pThis; - int i, k, iBit, status, nRegs, clk = clock(); + int i, k, iBit, status, nRegs;//, clk = clock(); /* Vec_PtrForEachEntry( unsigned *, vStates, pNext, i ) { diff --git a/src/proof/llb/llb4Image.c b/src/proof/llb/llb4Image.c index 91eb62f8..039be164 100644 --- a/src/proof/llb/llb4Image.c +++ b/src/proof/llb/llb4Image.c @@ -323,8 +323,8 @@ int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 Vec_Ptr_t * vSingles; DdNode * bCube, * bFunc; int i, RetValue, nSuppSize; - int iPart1 = pPart1->iPart; - int iPart2 = pPart2->iPart; +// int iPart1 = pPart1->iPart; +// int iPart2 = pPart2->iPart; int liveBeg, liveEnd; // create cube to be quantified @@ -806,7 +806,7 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV Vec_Ptr_t * vGroups; Llb_Prt_t * pPart, * pPart1, * pPart2; Llb_Mgr_t * p; - int i, nReorders, clk = clock(); + int i, nReorders;//, clk = clock(); // start the manager p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax ); // remove singles diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c index b7ea79b8..6442d62e 100644 --- a/src/proof/llb/llb4Nonlin.c +++ b/src/proof/llb/llb4Nonlin.c @@ -576,8 +576,8 @@ Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose ) Vec_Int_t * vVars2Q; Vec_Ptr_t * vStates, * vRootsNew; Aig_Obj_t * pObj; - DdNode * bState, * bImage, * bOneCube, * bRing; - int i, v, RetValue, clk = clock(); + DdNode * bState = NULL, * bImage, * bOneCube, * bRing; + int i, v, RetValue;//, clk = clock(); char * pValues; assert( Vec_PtrSize(p->vRings) > 0 ); // disable the timeout @@ -666,7 +666,7 @@ Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose ) int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) { DdNode * bAux; - int nIters, nBddSizeFr, nBddSizeTo, nBddSizeTo2; + int nIters, nBddSizeFr = 0, nBddSizeTo = 0, nBddSizeTo2 = 0; int clkTemp, clkIter, clk = clock(); assert( Aig_ManRegNum(p->pAig) > 0 ); |